Logiweb codex of proofreport in pyk

Up Help

ref-0-id-0	proofreport
ref-0-id-1	peano zero
ref-0-id-2	peano one
ref-0-id-3	peano two
ref-0-id-4	peano a
ref-0-id-5	peano b
ref-0-id-6	peano c
ref-0-id-7	peano d
ref-0-id-8	peano e
ref-0-id-9	peano f
ref-0-id-10	peano g
ref-0-id-11	peano h
ref-0-id-12	peano i
ref-0-id-13	peano j
ref-0-id-14	peano k
ref-0-id-15	peano l
ref-0-id-16	peano m
ref-0-id-17	peano n
ref-0-id-18	peano o
ref-0-id-19	peano p
ref-0-id-20	peano q
ref-0-id-21	peano r
ref-0-id-22	peano s
ref-0-id-23	peano t
ref-0-id-24	peano u
ref-0-id-25	peano v
ref-0-id-26	peano w
ref-0-id-27	peano x
ref-0-id-28	peano y
ref-0-id-29	peano z
ref-0-id-30	peano nonfree * in * end nonfree
ref-0-id-31	peano nonfree star * in * end nonfree
ref-0-id-32	peano free * set * to * end free
ref-0-id-33	peano free star * set * to * end free
ref-0-id-34	peano sub * is * where * is * end sub
ref-0-id-35	peano sub star * is * where * is * end sub
ref-0-id-36	system prime s
ref-0-id-37	axiom prime a one
ref-0-id-38	axiom prime a two
ref-0-id-39	axiom prime a three
ref-0-id-40	axiom prime a four
ref-0-id-41	axiom prime a five
ref-0-id-42	axiom prime s one
ref-0-id-43	axiom prime s two
ref-0-id-44	axiom prime s three
ref-0-id-45	axiom prime s four
ref-0-id-46	axiom prime s five
ref-0-id-47	axiom prime s six
ref-0-id-48	axiom prime s seven
ref-0-id-49	axiom prime s eight
ref-0-id-50	axiom prime s nine
ref-0-id-51	rule prime mp
ref-0-id-52	rule prime gen
ref-0-id-53	lemma prime l three two a
ref-0-id-57	lemma prime l three two b
ref-0-id-58	lemma prime l three two c
ref-0-id-59	lemma prime l three two d one
ref-0-id-60	lemma prime l three two d two
ref-0-id-61	lemma prime l three two f
ref-0-id-62	lemma prime l three two g
ref-0-id-63	lemma prime l three two h one
ref-0-id-64	lemma prime l three two h two
ref-0-id-65	lemma prime l three two h
ref-0-id-67	hypothetical three two d
ref-0-id-68	mendelson corollary one ten a
ref-0-id-69	mendelson corollary one ten b
ref-0-id-70	mendelson corollary one ten pre b
ref-0-id-71	mendelson corollary one ten b plus plus
ref-0-id-72	hypothetical rule prime mp plus plus
ref-0-id-73	hypothesize plus plus
ref-0-id-74	mendelson one seven plus plus
ref-0-id-75	mendelson one seven
ref-0-id-76	hypothetical rule prime mp
ref-0-id-77	hypothesize
ref-0-id-78	hypothetical rule prime gen
ref-0-id-79	mendelson three two a
ref-0-id-80	hypothetical three two a
ref-0-id-81	hypothetical three two b
ref-0-id-82	hypothetical three one s one
ref-0-id-83	hypothetical three two c
ref-0-id-84	hypothetical three one s two
ref-0-id-85	hypothetical three one s five
ref-0-id-86	hypothetical three one s six
ref-0-id-87	mendelson three two f
ref-0-id-88	* peano var
ref-0-id-89	* peano succ
ref-0-id-90	* peano times *
ref-0-id-91	* peano plus *
ref-0-id-92	* peano is *
ref-0-id-93	* is peano var
ref-0-id-94	peano not *
ref-0-id-95	* peano and *
ref-0-id-96	* peano or *
ref-0-id-97	peano all * indeed *
ref-0-id-98	peano exist * indeed *
ref-0-id-99	* peano imply *
ref-0-id-100	* peano iff *
ref-0-id-101	* macro modus ponens *
ref-0-id-102	* hypothetical modus ponens *