Logiweb codex of ijcar base in pyk

Up Help

ref-0-id-0	ijcar base
ref-0-id-1	proclaim * as * end proclaim
ref-0-id-2	unicode start of text * end unicode text
ref-0-id-3	unicode end of text
ref-0-id-4	* then *
ref-0-id-5	* begin * end *
ref-0-id-6	preassociative * greater than *
ref-0-id-7	postassociative * greater than *
ref-0-id-8	priority * equal *
ref-0-id-9	priority * end priority
ref-0-id-10	unicode newline *
ref-0-id-11	x
ref-0-id-12	text * end text
ref-0-id-13	text * plus *
ref-0-id-14	text * plus indent *
ref-0-id-15	bracket * end bracket
ref-0-id-16	big bracket * end bracket
ref-0-id-17	math * end math
ref-0-id-18	flush left * end left
ref-0-id-19	var x
ref-0-id-20	var y
ref-0-id-21	var z
ref-0-id-22	define * of * as * end define
ref-0-id-23	pyk
ref-0-id-24	tex
ref-0-id-25	tex name
ref-0-id-26	priority
ref-0-id-27	true
ref-0-id-28	if * then * else * end if
ref-0-id-29	introduce * of * as * end introduce
ref-0-id-30	value
ref-0-id-31	claim
ref-0-id-32	unicode space *
ref-0-id-33	unicode exclamation mark *
ref-0-id-34	unicode quotation mark *
ref-0-id-35	unicode number sign *
ref-0-id-36	unicode dollar sign *
ref-0-id-37	unicode percent *
ref-0-id-38	unicode ampersand *
ref-0-id-39	unicode apostrophe *
ref-0-id-40	unicode left parenthesis *
ref-0-id-41	unicode right parenthesis *
ref-0-id-42	unicode asterisk *
ref-0-id-43	unicode plus sign *
ref-0-id-44	unicode comma *
ref-0-id-45	unicode hyphen *
ref-0-id-46	unicode period *
ref-0-id-47	unicode slash *
ref-0-id-48	unicode zero *
ref-0-id-49	unicode one *
ref-0-id-50	unicode two *
ref-0-id-51	unicode three *
ref-0-id-52	unicode four *
ref-0-id-53	unicode five *
ref-0-id-54	unicode six *
ref-0-id-55	unicode seven *
ref-0-id-56	unicode eight *
ref-0-id-57	unicode nine *
ref-0-id-58	unicode colon *
ref-0-id-59	unicode semicolon *
ref-0-id-60	unicode less than *
ref-0-id-61	unicode equal sign *
ref-0-id-62	unicode greater than *
ref-0-id-63	unicode question mark *
ref-0-id-64	unicode commercial at *
ref-0-id-65	unicode capital a *
ref-0-id-66	unicode capital b *
ref-0-id-67	unicode capital c *
ref-0-id-68	unicode capital d *
ref-0-id-69	unicode capital e *
ref-0-id-70	unicode capital f *
ref-0-id-71	unicode capital g *
ref-0-id-72	unicode capital h *
ref-0-id-73	unicode capital i *
ref-0-id-74	unicode capital j *
ref-0-id-75	unicode capital k *
ref-0-id-76	unicode capital l *
ref-0-id-77	unicode capital m *
ref-0-id-78	unicode capital n *
ref-0-id-79	unicode capital o *
ref-0-id-80	unicode capital p *
ref-0-id-81	unicode capital q *
ref-0-id-82	unicode capital r *
ref-0-id-83	unicode capital s *
ref-0-id-84	unicode capital t *
ref-0-id-85	unicode capital u *
ref-0-id-86	unicode capital v *
ref-0-id-87	unicode capital w *
ref-0-id-88	unicode capital x *
ref-0-id-89	unicode capital y *
ref-0-id-90	unicode capital z *
ref-0-id-91	unicode left bracket *
ref-0-id-92	unicode backslash *
ref-0-id-93	unicode right bracket *
ref-0-id-94	unicode circumflex *
ref-0-id-95	unicode underscore *
ref-0-id-96	unicode grave accent *
ref-0-id-97	unicode small a *
ref-0-id-98	unicode small b *
ref-0-id-99	unicode small c *
ref-0-id-100	unicode small d *
ref-0-id-101	unicode small e *
ref-0-id-102	unicode small f *
ref-0-id-103	unicode small g *
ref-0-id-104	unicode small h *
ref-0-id-105	unicode small i *
ref-0-id-106	unicode small j *
ref-0-id-107	unicode small k *
ref-0-id-108	unicode small l *
ref-0-id-109	unicode small m *
ref-0-id-110	unicode small n *
ref-0-id-111	unicode small o *
ref-0-id-112	unicode small p *
ref-0-id-113	unicode small q *
ref-0-id-114	unicode small r *
ref-0-id-115	unicode small s *
ref-0-id-116	unicode small t *
ref-0-id-117	unicode small u *
ref-0-id-118	unicode small v *
ref-0-id-119	unicode small w *
ref-0-id-120	unicode small x *
ref-0-id-121	unicode small y *
ref-0-id-122	unicode small z *
ref-0-id-123	unicode left brace *
ref-0-id-124	unicode vertical line *
ref-0-id-125	unicode right brace *
ref-0-id-126	unicode tilde *
ref-0-id-127	bottom
ref-0-id-128	function f of * end function
ref-0-id-129	identity * end identity
ref-0-id-130	false
ref-0-id-131	untagged zero
ref-0-id-132	untagged one
ref-0-id-133	untagged two
ref-0-id-134	untagged three
ref-0-id-135	untagged four
ref-0-id-136	untagged five
ref-0-id-137	untagged six
ref-0-id-138	untagged seven
ref-0-id-139	untagged eight
ref-0-id-140	untagged nine
ref-0-id-141	zero
ref-0-id-142	one
ref-0-id-143	two
ref-0-id-144	three
ref-0-id-145	four
ref-0-id-146	five
ref-0-id-147	six
ref-0-id-148	seven
ref-0-id-149	eight
ref-0-id-150	nine
ref-0-id-151	var a
ref-0-id-152	var b
ref-0-id-153	var c
ref-0-id-154	var d
ref-0-id-155	var e
ref-0-id-156	var f
ref-0-id-157	var g
ref-0-id-158	var h
ref-0-id-159	var i
ref-0-id-160	var j
ref-0-id-161	var k
ref-0-id-162	var l
ref-0-id-163	var m
ref-0-id-164	var n
ref-0-id-165	var o
ref-0-id-166	var p
ref-0-id-167	var q
ref-0-id-168	var r
ref-0-id-169	var s
ref-0-id-170	var t
ref-0-id-171	var u
ref-0-id-172	var v
ref-0-id-173	var w
ref-0-id-174	tagged parenthesis * end tagged
ref-0-id-175	tagged if * then * else * end if
ref-0-id-176	array * is * end array
ref-0-id-177	left
ref-0-id-178	center
ref-0-id-179	right
ref-0-id-180	empty
ref-0-id-181	substitute * set * to * end substitute
ref-0-id-182	map tag * end tag
ref-0-id-183	raw map untag * end untag
ref-0-id-184	map untag * end untag
ref-0-id-185	normalizing untag * end untag
ref-0-id-186	apply * to * end apply
ref-0-id-187	apply one * to * end apply
ref-0-id-188	identifier * end identifier
ref-0-id-189	identifier one * plus id * end identifier
ref-0-id-190	array plus * and * end plus
ref-0-id-191	array remove * array * level * end remove
ref-0-id-192	array put * value * array * level * end put
ref-0-id-193	array add * value * index * value * level * end add
ref-0-id-194	bit * of * end bit
ref-0-id-195	bit one * of * end bit
ref-0-id-196	example rack
ref-0-id-197	vector hook
ref-0-id-198	bibliography hook
ref-0-id-199	dictionary hook
ref-0-id-200	body hook
ref-0-id-201	codex hook
ref-0-id-202	expansion hook
ref-0-id-203	code hook
ref-0-id-204	cache hook
ref-0-id-205	diagnose hook
ref-0-id-206	pyk aspect
ref-0-id-207	tex aspect
ref-0-id-208	texname aspect
ref-0-id-209	value aspect
ref-0-id-210	message aspect
ref-0-id-211	macro aspect
ref-0-id-212	definition aspect
ref-0-id-213	unpack aspect
ref-0-id-214	claim aspect
ref-0-id-215	priority aspect
ref-0-id-216	lambda identifier
ref-0-id-217	apply identifier
ref-0-id-218	true identifier
ref-0-id-219	if identifier
ref-0-id-220	quote identifier
ref-0-id-221	proclaim identifier
ref-0-id-222	define identifier
ref-0-id-223	introduce identifier
ref-0-id-224	hide identifier
ref-0-id-225	pre identifier
ref-0-id-226	post identifier
ref-0-id-227	eval * stack * cache * end eval
ref-0-id-228	eval two * ref * id * stack * cache * end eval
ref-0-id-229	eval three * function * stack * cache * end eval
ref-0-id-230	eval four * arguments * stack * cache * end eval
ref-0-id-231	lookup * stack * default * end lookup
ref-0-id-232	abstract * term * stack * cache * end abstract
ref-0-id-233	quote * end quote
ref-0-id-234	expand * state * cache * end expand
ref-0-id-235	expand two * definition * state * cache * end expand
ref-0-id-236	expand list * state * cache * end expand
ref-0-id-237	macro
ref-0-id-238	macro state
ref-0-id-239	zip * with * end zip
ref-0-id-240	assoc one * address * index * end assoc
ref-0-id-241	protect * end protect
ref-0-id-242	self
ref-0-id-243	macro define * as * end define
ref-0-id-244	value define * as * end define
ref-0-id-245	intro define * as * end define
ref-0-id-246	pyk define * as * end define
ref-0-id-247	tex define * as * end define
ref-0-id-248	tex name define * as * end define
ref-0-id-249	priority table * end table
ref-0-id-250	macro define one
ref-0-id-251	macro define two * end define
ref-0-id-252	macro define three * end define
ref-0-id-253	macro define four * state * cache * definition * end define
ref-0-id-254	state expand * state * cache * end expand
ref-0-id-255	quote expand * term * stack * end expand
ref-0-id-256	quote expand two * term * stack * end expand
ref-0-id-257	quote expand three * term * stack * value * end expand
ref-0-id-258	quote expand star * term * stack * end expand
ref-0-id-259	parenthesis * end parenthesis
ref-0-id-260	big parenthesis * end parenthesis
ref-0-id-261	display * end display
ref-0-id-262	statement * end statement
ref-0-id-263	spying test * end test
ref-0-id-264	false spying test * end test
ref-0-id-265	aspect * subcodex * end aspect
ref-0-id-266	aspect * term * cache * end aspect
ref-0-id-267	tuple * end tuple
ref-0-id-268	tuple one * end tuple
ref-0-id-269	tuple two * end tuple
ref-0-id-270	let two * apply * end let
ref-0-id-271	let one * apply * end let
ref-0-id-272	claim define * as * end define
ref-0-id-273	checker
ref-0-id-274	check * cache * end check
ref-0-id-275	check two * cache * def * end check
ref-0-id-276	check three * cache * def * end check
ref-0-id-277	check list * cache * end check
ref-0-id-278	check list two * cache * value * end check
ref-0-id-279	test * end test
ref-0-id-280	false test * end test
ref-0-id-281	raw test * end test
ref-0-id-282	message
ref-0-id-283	message define * as * end define
ref-0-id-284	the statement aspect
ref-0-id-285	statement
ref-0-id-286	statement define * as * end define
ref-0-id-287	example axiom
ref-0-id-288	example scheme
ref-0-id-289	example rule
ref-0-id-290	absurdity
ref-0-id-291	contraexample
ref-0-id-292	example theory primed
ref-0-id-293	example lemma
ref-0-id-294	metavar * end metavar
ref-0-id-295	meta a
ref-0-id-296	meta b
ref-0-id-297	meta c
ref-0-id-298	meta d
ref-0-id-299	meta e
ref-0-id-300	meta f
ref-0-id-301	meta g
ref-0-id-302	meta h
ref-0-id-303	meta i
ref-0-id-304	meta j
ref-0-id-305	meta k
ref-0-id-306	meta l
ref-0-id-307	meta m
ref-0-id-308	meta n
ref-0-id-309	meta o
ref-0-id-310	meta p
ref-0-id-311	meta q
ref-0-id-312	meta r
ref-0-id-313	meta s
ref-0-id-314	meta t
ref-0-id-315	meta u
ref-0-id-316	meta v
ref-0-id-317	meta w
ref-0-id-318	meta x
ref-0-id-319	meta y
ref-0-id-320	meta z
ref-0-id-321	sub * set * to * end sub
ref-0-id-322	sub star * set * to * end sub
ref-0-id-323	the empty set
ref-0-id-324	example remainder
ref-0-id-325	make visible * end visible
ref-0-id-326	intro * index * pyk * tex * end intro
ref-0-id-327	intro * pyk * tex * end intro
ref-0-id-328	error * term * end error
ref-0-id-329	error two * term * end error
ref-0-id-330	proof * term * cache * end proof
ref-0-id-331	proof two * term * end proof
ref-0-id-332	sequent eval * term * end eval
ref-0-id-333	seqeval init * term * end eval
ref-0-id-334	seqeval modus * term * end eval
ref-0-id-335	seqeval modus one * term * sequent * end eval
ref-0-id-336	seqeval verify * term * end eval
ref-0-id-337	seqeval verify one * term * sequent * end eval
ref-0-id-338	sequent eval plus * term * end eval
ref-0-id-339	seqeval plus one * term * sequent * end eval
ref-0-id-340	seqeval minus * term * end eval
ref-0-id-341	seqeval minus one * term * sequent * end eval
ref-0-id-342	seqeval deref * term * end eval
ref-0-id-343	seqeval deref one * term * sequent * end eval
ref-0-id-344	seqeval deref two * term * sequent * def * end eval
ref-0-id-345	seqeval at * term * end eval
ref-0-id-346	seqeval at one * term * sequent * end eval
ref-0-id-347	seqeval infer * term * end eval
ref-0-id-348	seqeval infer one * term * premise * sequent * end eval
ref-0-id-349	seqeval endorse * term * end eval
ref-0-id-350	seqeval endorse one * term * side * sequent * end eval
ref-0-id-351	seqeval est * term * end eval
ref-0-id-352	seqeval est one * term * name * sequent * end eval
ref-0-id-353	seqeval est two * term * name * sequent * def * end eval
ref-0-id-354	seqeval all * term * end eval
ref-0-id-355	seqeval all one * term * variable * sequent * end eval
ref-0-id-356	seqeval cut * term * end eval
ref-0-id-357	seqeval cut one * term * forerunner * end eval
ref-0-id-358	seqeval cut two * term * forerunner * sequent * end eval
ref-0-id-359	computably true * end true
ref-0-id-360	claims * cache * ref * end claims
ref-0-id-361	claims two * cache * ref * end claims
ref-0-id-362	the proof aspect
ref-0-id-363	proof
ref-0-id-364	lemma * says * end lemma
ref-0-id-365	proof of * reads * end proof
ref-0-id-366	in theory * lemma * says * end lemma
ref-0-id-367	in theory * antilemma * says * end antilemma
ref-0-id-368	in theory * rule * says * end rule
ref-0-id-369	in theory * antirule * says * end antirule
ref-0-id-370	verifier
ref-0-id-371	verify one * end verify
ref-0-id-372	verify two * proofs * end verify
ref-0-id-373	verify three * ref * sequents * diagnose * end verify
ref-0-id-374	verify four * premises * end verify
ref-0-id-375	verify five * ref * array * sequents * end verify
ref-0-id-376	verify six * ref * list * sequents * end verify
ref-0-id-377	verify seven * ref * id * sequents * end verify
ref-0-id-378	cut * and * end cut
ref-0-id-379	head * end head
ref-0-id-380	tail * end tail
ref-0-id-381	rule one * theory * end rule
ref-0-id-382	rule * subcodex * end rule
ref-0-id-383	rule tactic
ref-0-id-384	plus * and * end plus
ref-0-id-385	theory * end theory
ref-0-id-386	theory two * cache * end theory
ref-0-id-387	theory three * name * end theory
ref-0-id-388	theory four * name * sum * end theory
ref-0-id-389	example axiom lemma primed
ref-0-id-390	example scheme lemma primed
ref-0-id-391	example rule lemma primed
ref-0-id-392	contraexample lemma primed
ref-0-id-393	example axiom lemma
ref-0-id-394	example scheme lemma
ref-0-id-395	example rule lemma
ref-0-id-396	contraexample lemma
ref-0-id-397	example theory
ref-0-id-398	ragged right
ref-0-id-399	ragged right expansion
ref-0-id-400	parameter term * stack * seed * end parameter
ref-0-id-401	parameter term star * stack * seed * end parameter
ref-0-id-402	instantiate * with * end instantiate
ref-0-id-403	instantiate star * with * end instantiate
ref-0-id-404	occur * in * substitution * end occur
ref-0-id-405	occur star * in * substitution * end occur
ref-0-id-406	unify * with * substitution * end unify
ref-0-id-407	unify star * with * substitution * end unify
ref-0-id-408	unify two * with * substitution * end unify
ref-0-id-409	ell a
ref-0-id-410	ell b
ref-0-id-411	ell c
ref-0-id-412	ell d
ref-0-id-413	ell e
ref-0-id-414	ell f
ref-0-id-415	ell g
ref-0-id-416	ell h
ref-0-id-417	ell i
ref-0-id-418	ell j
ref-0-id-419	ell k
ref-0-id-420	ell l
ref-0-id-421	ell m
ref-0-id-422	ell n
ref-0-id-423	ell o
ref-0-id-424	ell p
ref-0-id-425	ell q
ref-0-id-426	ell r
ref-0-id-427	ell s
ref-0-id-428	ell t
ref-0-id-429	ell u
ref-0-id-430	ell v
ref-0-id-431	ell w
ref-0-id-432	ell x
ref-0-id-433	ell y
ref-0-id-434	ell z
ref-0-id-435	ell big a
ref-0-id-436	ell big b
ref-0-id-437	ell big c
ref-0-id-438	ell big d
ref-0-id-439	ell big e
ref-0-id-440	ell big f
ref-0-id-441	ell big g
ref-0-id-442	ell big h
ref-0-id-443	ell big i
ref-0-id-444	ell big j
ref-0-id-445	ell big k
ref-0-id-446	ell big l
ref-0-id-447	ell big m
ref-0-id-448	ell big n
ref-0-id-449	ell big o
ref-0-id-450	ell big p
ref-0-id-451	ell big q
ref-0-id-452	ell big r
ref-0-id-453	ell big s
ref-0-id-454	ell big t
ref-0-id-455	ell big u
ref-0-id-456	ell big v
ref-0-id-457	ell big w
ref-0-id-458	ell big x
ref-0-id-459	ell big y
ref-0-id-460	ell big z
ref-0-id-461	ell dummy
ref-0-id-462	sequent reflexivity
ref-0-id-463	tactic reflexivity
ref-0-id-464	sequent commutativity
ref-0-id-465	tactic commutativity
ref-0-id-466	the tactic aspect
ref-0-id-467	tactic
ref-0-id-468	tactic define * as * end define
ref-0-id-469	proof expand * state * cache * end expand
ref-0-id-470	proof expand list * state * cache * end expand
ref-0-id-471	proof state
ref-0-id-472	conclude one * cache * end conclude
ref-0-id-473	conclude two * proves * cache * end conclude
ref-0-id-474	conclude three * proves * lemma * substitution * end conclude
ref-0-id-475	conclude four * lemma * end conclude
ref-0-id-476	* sub * end sub
ref-0-id-477	* intro * index * pyk * tex * end intro
ref-0-id-478	* intro * pyk * tex * end intro
ref-0-id-479	* intro * index * pyk * tex * name * end intro
ref-0-id-480	* intro * pyk * tex * name * end intro
ref-0-id-481	* prime
ref-0-id-482	* assoc * end assoc
ref-0-id-483	* set * to * end set
ref-0-id-484	* set multi * to * end set
ref-0-id-485	* bit nil
ref-0-id-486	* bit one
ref-0-id-487	binary
ref-0-id-488	* color * end color
ref-0-id-489	* color star * end color
ref-0-id-490	* raw head
ref-0-id-491	* raw tail
ref-0-id-492	* cardinal untag
ref-0-id-493	* head
ref-0-id-494	* tail
ref-0-id-495	* is singular
ref-0-id-496	* is cardinal
ref-0-id-497	* is data
ref-0-id-498	* is atomic
ref-0-id-499	* cardinal retract
ref-0-id-500	* tagged retract
ref-0-id-501	* boolean retract
ref-0-id-502	* ref
ref-0-id-503	* id
ref-0-id-504	* debug
ref-0-id-505	* root
ref-0-id-506	* zeroth
ref-0-id-507	* first
ref-0-id-508	* second
ref-0-id-509	* third
ref-0-id-510	* fourth
ref-0-id-511	* fifth
ref-0-id-512	* sixth
ref-0-id-513	* seventh
ref-0-id-514	* eighth
ref-0-id-515	* ninth
ref-0-id-516	* is error
ref-0-id-517	* is metavar
ref-0-id-518	* is metaclosed
ref-0-id-519	* is metaclosed star
ref-0-id-520	newline *
ref-0-id-521	macro newline *
ref-0-id-522	* apply *
ref-0-id-523	* tagged apply *
ref-0-id-524	* times *
ref-0-id-525	* times zero *
ref-0-id-526	* plus *
ref-0-id-527	* plus zero *
ref-0-id-528	* plus one *
ref-0-id-529	* minus *
ref-0-id-530	* minus zero *
ref-0-id-531	* minus one *
ref-0-id-532	* term plus * end plus
ref-0-id-533	* term union *
ref-0-id-534	* term minus * end minus
ref-0-id-535	* raw pair *
ref-0-id-536	* eager pair *
ref-0-id-537	* tagged pair *
ref-0-id-538	* untagged double *
ref-0-id-539	* pair *
ref-0-id-540	* double *
ref-0-id-541	* comma *
ref-0-id-542	* boolean equal *
ref-0-id-543	* data equal *
ref-0-id-544	* cardinal equal *
ref-0-id-545	* peano equal *
ref-0-id-546	* tagged equal *
ref-0-id-547	* math equal *
ref-0-id-548	* reduce to *
ref-0-id-549	* term equal *
ref-0-id-550	* term list equal *
ref-0-id-551	* term root equal *
ref-0-id-552	* term in *
ref-0-id-553	* term subset *
ref-0-id-554	* term set equal *
ref-0-id-555	* sequent equal *
ref-0-id-556	* free in *
ref-0-id-557	* free in star *
ref-0-id-558	* free for * in *
ref-0-id-559	* free for star * in *
ref-0-id-560	* claim in *
ref-0-id-561	* less *
ref-0-id-562	* less zero *
ref-0-id-563	* less one *
ref-0-id-564	not *
ref-0-id-565	* and *
ref-0-id-566	* macro and *
ref-0-id-567	* simple and *
ref-0-id-568	* claim and *
ref-0-id-569	* or *
ref-0-id-570	* parallel *
ref-0-id-571	* macro or *
ref-0-id-572	* macro imply *
ref-0-id-573	* guard *
ref-0-id-574	* spy *
ref-0-id-575	* tagged guard *
ref-0-id-576	* select * else * end select
ref-0-id-577	lambda * dot *
ref-0-id-578	tagged lambda * dot *
ref-0-id-579	tagging *
ref-0-id-580	open if * then * else *
ref-0-id-581	let * be * in *
ref-0-id-582	let * abbreviate * in *
ref-0-id-583	* init
ref-0-id-584	* modus
ref-0-id-585	* verify
ref-0-id-586	* curry plus
ref-0-id-587	* curry minus
ref-0-id-588	* dereference
ref-0-id-589	* at *
ref-0-id-590	* modus ponens *
ref-0-id-591	* modus probans *
ref-0-id-592	* conclude *
ref-0-id-593	* infer *
ref-0-id-594	* endorse *
ref-0-id-595	* id est *
ref-0-id-596	all * indeed *
ref-0-id-597	* rule plus *
ref-0-id-598	* cut *
ref-0-id-599	* proves *
ref-0-id-600	* proof of * reads *
ref-0-id-601	line * because * indeed * end line *
ref-0-id-602	because * indeed * qed
ref-0-id-603	line * premise * end line *
ref-0-id-604	line * side condition * end line *
ref-0-id-605	arbitrary * end line *
ref-0-id-606	locally define * as * end line *
ref-0-id-607	* tab *
ref-0-id-608	* row *