Logiweb codex of peano in pyk

Up Help

ref-0-id-0	peano
ref-0-id-1	intro * index * pyk * tex * end intro
ref-0-id-2	intro * pyk * tex * end intro
ref-0-id-3	peano zero
ref-0-id-4	peano one
ref-0-id-5	peano two
ref-0-id-6	peano a
ref-0-id-7	peano b
ref-0-id-8	peano c
ref-0-id-9	peano d
ref-0-id-10	peano e
ref-0-id-11	peano f
ref-0-id-12	peano g
ref-0-id-13	peano h
ref-0-id-14	peano i
ref-0-id-15	peano j
ref-0-id-16	peano k
ref-0-id-17	peano l
ref-0-id-18	peano m
ref-0-id-19	peano n
ref-0-id-20	peano o
ref-0-id-21	peano p
ref-0-id-22	peano q
ref-0-id-23	peano r
ref-0-id-24	peano s
ref-0-id-25	peano t
ref-0-id-26	peano u
ref-0-id-27	peano v
ref-0-id-28	peano w
ref-0-id-29	peano x
ref-0-id-30	peano y
ref-0-id-31	peano z
ref-0-id-32	peano nonfree * in * end nonfree
ref-0-id-33	peano nonfree star * in * end nonfree
ref-0-id-34	peano free * set * to * end free
ref-0-id-35	peano free star * set * to * end free
ref-0-id-36	peano sub * is * where * is * end sub
ref-0-id-37	peano sub star * is * where * is * end sub
ref-0-id-38	system s
ref-0-id-39	axiom a one
ref-0-id-40	axiom a two
ref-0-id-41	axiom a three
ref-0-id-42	axiom a four
ref-0-id-43	axiom a five
ref-0-id-44	axiom s one
ref-0-id-45	axiom s two
ref-0-id-46	axiom s three
ref-0-id-47	axiom s four
ref-0-id-48	axiom s five
ref-0-id-49	axiom s six
ref-0-id-50	axiom s seven
ref-0-id-51	axiom s eight
ref-0-id-52	axiom s nine
ref-0-id-53	rule mp
ref-0-id-54	rule gen
ref-0-id-55	lemma l three two a
ref-0-id-56	* peano var
ref-0-id-57	* peano succ
ref-0-id-58	* peano times *
ref-0-id-59	* peano plus *
ref-0-id-60	* peano is *
ref-0-id-61	* is peano var
ref-0-id-62	peano not *
ref-0-id-63	* peano and *
ref-0-id-64	* peano or *
ref-0-id-65	peano all * indeed *
ref-0-id-66	peano exist * indeed *
ref-0-id-67	* peano imply *
ref-0-id-68	* peano iff *