Logiweb codex of peano in pyk

Up Help

ref-0-id-0	peano
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 s
ref-0-id-37	axiom a one
ref-0-id-38	axiom a two
ref-0-id-39	axiom a three
ref-0-id-40	axiom a four
ref-0-id-41	axiom a five
ref-0-id-42	axiom s one
ref-0-id-43	axiom s two
ref-0-id-44	axiom s three
ref-0-id-45	axiom s four
ref-0-id-46	axiom s five
ref-0-id-47	axiom s six
ref-0-id-48	axiom s seven
ref-0-id-49	axiom s eight
ref-0-id-50	axiom s nine
ref-0-id-51	rule mp
ref-0-id-52	rule gen
ref-0-id-53	lemma l three two a
ref-0-id-54	system prime s
ref-0-id-55	axiom prime a one
ref-0-id-56	axiom prime a two
ref-0-id-57	axiom prime a three
ref-0-id-58	axiom prime a four
ref-0-id-59	axiom prime a five
ref-0-id-60	axiom prime s one
ref-0-id-61	axiom prime s two
ref-0-id-62	axiom prime s three
ref-0-id-63	axiom prime s four
ref-0-id-64	axiom prime s five
ref-0-id-65	axiom prime s six
ref-0-id-66	axiom prime s seven
ref-0-id-67	axiom prime s eight
ref-0-id-68	axiom prime s nine
ref-0-id-69	rule prime mp
ref-0-id-70	rule prime gen
ref-0-id-71	lemma prime l three two a
ref-0-id-72	mendelson one seven
ref-0-id-73	hypothetical rule prime mp
ref-0-id-74	hypothesize
ref-0-id-75	hypothetical rule prime gen
ref-0-id-76	mendelson three two a
ref-0-id-77	hypothetical three two a
ref-0-id-78	hypothetical three two b
ref-0-id-79	hypothetical three one s one
ref-0-id-80	hypothetical three two c
ref-0-id-81	hypothetical three one s two
ref-0-id-82	hypothetical three one s five
ref-0-id-83	hypothetical three one s six
ref-0-id-84	mendelson three two f
ref-0-id-85	* peano var
ref-0-id-86	* peano succ
ref-0-id-87	* peano times *
ref-0-id-88	* peano plus *
ref-0-id-89	* peano is *
ref-0-id-90	* is peano var
ref-0-id-91	peano not *
ref-0-id-92	* peano and *
ref-0-id-93	* peano or *
ref-0-id-94	peano all * indeed *
ref-0-id-95	peano exist * indeed *
ref-0-id-96	* peano imply *
ref-0-id-97	* peano iff *
ref-0-id-98	* macro modus ponens *
ref-0-id-99	* hypothetical modus ponens *