Logiweb codex of peanorapport in pyk

Up Help

ref-0-id-0	peanorapport
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 three two a
ref-0-id-54	lemma prime three two b
ref-0-id-55	lemma prime three two c
ref-0-id-56	lemma prime three two d
ref-0-id-57	lemma prime three two f
ref-0-id-58	lemma prime three two g
ref-0-id-59	lemma prime three two g rev
ref-0-id-60	lemma prime three two h base
ref-0-id-61	lemma prime three two h
ref-0-id-62	lemma tautology one
ref-0-id-63	lemma tautology two
ref-0-id-64	lemma tautology three
ref-0-id-65	lemma tautology four
ref-0-id-66	lemma weaken
ref-0-id-67	mendelson one seven
ref-0-id-68	lemma mp twice
ref-0-id-71	* peano var
ref-0-id-72	* peano succ
ref-0-id-73	* peano times *
ref-0-id-74	* peano plus *
ref-0-id-75	* peano is *
ref-0-id-76	* is peano var
ref-0-id-77	peano not *
ref-0-id-80	peano all * indeed *
ref-0-id-82	* peano imply *