Logiweb codex of ijcar in pyk

Up Help

ref-1-id-318	meta x
ref-0-id-0	ijcar
ref-0-id-1	general macro define * as * end define
ref-0-id-2	make root visible * end visible
ref-0-id-3	ijcar example axiom
ref-0-id-4	ijcar example rule
ref-0-id-5	ijcar example contradiction
ref-0-id-6	ijcar example theory
ref-0-id-7	ijcar example lemma
ref-0-id-8	set * end set
ref-0-id-9	object var * end var
ref-0-id-10	object a
ref-0-id-11	object b
ref-0-id-12	object c
ref-0-id-13	object d
ref-0-id-14	object e
ref-0-id-15	object f
ref-0-id-16	object g
ref-0-id-17	object h
ref-0-id-18	object i
ref-0-id-19	object j
ref-0-id-20	object k
ref-0-id-21	object l
ref-0-id-22	object m
ref-0-id-23	object n
ref-0-id-24	object o
ref-0-id-25	object p
ref-0-id-26	object q
ref-0-id-27	object r
ref-0-id-28	object s
ref-0-id-29	object t
ref-0-id-30	object u
ref-0-id-31	object v
ref-0-id-32	object w
ref-0-id-33	object x
ref-0-id-34	object y
ref-0-id-35	object z
ref-0-id-36	sub * is * where * is * end sub
ref-0-id-37	sub zero * is * where * is * end sub
ref-0-id-38	sub one * is * where * is * end sub
ref-0-id-39	sub star * is * where * is * end sub
ref-0-id-40	deduction * conclude * end deduction
ref-0-id-41	deduction zero * conclude * end deduction
ref-0-id-42	deduction one * conclude * condition * end deduction
ref-0-id-43	deduction two * conclude * condition * end deduction
ref-0-id-44	deduction three * conclude * condition * bound * end deduction
ref-0-id-45	deduction four * conclude * condition * bound * end deduction
ref-0-id-46	deduction four star * conclude * condition * bound * end deduction
ref-0-id-47	deduction five * condition * bound * end deduction
ref-0-id-48	deduction six * conclude * exception * bound * end deduction
ref-0-id-49	deduction six star * conclude * exception * bound * end deduction
ref-0-id-50	deduction seven * end deduction
ref-0-id-51	deduction eight * bound * end deduction
ref-0-id-52	deduction eight * bound * end deduction
ref-0-id-53	system s
ref-0-id-54	double negation
ref-0-id-55	rule mp
ref-0-id-56	rule gen
ref-0-id-57	deduction
ref-0-id-58	axiom s one
ref-0-id-59	axiom s two
ref-0-id-60	axiom s three
ref-0-id-61	axiom s four
ref-0-id-62	axiom s five
ref-0-id-63	axiom s six
ref-0-id-64	axiom s seven
ref-0-id-65	axiom s eight
ref-0-id-66	axiom s nine
ref-0-id-67	repetition
ref-0-id-68	lemma a one
ref-0-id-69	lemma a two
ref-0-id-70	lemma a four
ref-0-id-71	lemma a five
ref-0-id-72	prop three two a
ref-0-id-73	prop three two b
ref-0-id-74	prop three two c
ref-0-id-75	prop three two d
ref-0-id-76	prop three two e one
ref-0-id-77	prop three two e two
ref-0-id-78	prop three two e
ref-0-id-79	prop three two f one
ref-0-id-80	prop three two f two
ref-0-id-81	prop three two f
ref-0-id-82	prop three two g one
ref-0-id-83	prop three two g two
ref-0-id-84	prop three two g
ref-0-id-85	prop three two h one
ref-0-id-86	prop three two h two
ref-0-id-87	prop three two h
ref-0-id-88	block one * state * cache * end block
ref-0-id-89	block two * end block
ref-0-id-90	* hide
ref-0-id-91	macro indent *
ref-0-id-92	* suc
ref-0-id-93	* equal *
ref-0-id-94	* unequal *
ref-0-id-95	* is object var
ref-0-id-96	* avoid zero *
ref-0-id-97	* avoid one *
ref-0-id-98	* avoid star *
ref-0-id-99	exist * indeed *
ref-0-id-100	for all * indeed *
ref-0-id-101	for all objects * indeed *
ref-0-id-102	* imply *
ref-0-id-103	* if and only if *
ref-0-id-104	* avoid *
ref-0-id-105	* object modus ponens *
ref-0-id-106	for all terms * indeed *
ref-0-id-107	block * line * end block *
ref-0-id-108	because * indeed * end line
ref-0-id-109	any term * end line *
ref-0-id-110	* alternative *
ref-0-id-111	evaluates to
ref-0-id-112	* safe row *