Logiweb codex of hmpeano in pyk

Up Help

ref-2-id-54	system prime s
ref-2-id-55	axiom prime a one
ref-2-id-56	axiom prime a two
ref-2-id-57	axiom prime a three
ref-2-id-58	axiom prime a four
ref-2-id-59	axiom prime a five
ref-2-id-60	axiom prime s one
ref-2-id-61	axiom prime s two
ref-2-id-62	axiom prime s three
ref-2-id-63	axiom prime s four
ref-2-id-64	axiom prime s five
ref-2-id-65	axiom prime s six
ref-2-id-66	axiom prime s seven
ref-2-id-67	axiom prime s eight
ref-2-id-68	axiom prime s nine
ref-2-id-69	rule prime mp
ref-2-id-70	rule prime gen
ref-2-id-73	hypothetical rule prime mp
ref-2-id-74	hypothesize
ref-2-id-98	* macro modus ponens *
ref-2-id-99	* hypothetical modus ponens *
ref-0-id-0	hmpeano
ref-0-id-1	prop three two a
ref-0-id-2	prop three two b
ref-0-id-3	prop three two b rule
ref-0-id-4	prop three two c
ref-0-id-5	prop three two c rule
ref-0-id-6	prop three two c hyp rule
ref-0-id-7	prop three two d
ref-0-id-8	prop three two d rule
ref-0-id-9	prop three two d hyp rule
ref-0-id-10	prop three two f
ref-0-id-11	prop three two f base
ref-0-id-12	prop three two f ind
ref-0-id-13	prop three two f t
ref-0-id-14	prop three two g
ref-0-id-15	prop three two g base
ref-0-id-16	prop three two g ind
ref-0-id-17	prop three two g rt hyp
ref-0-id-18	prop three two h
ref-0-id-19	prop three two h base
ref-0-id-20	prop three two h ind
ref-0-id-21	axiom prime s six hyp
ref-0-id-22	permute premises
ref-0-id-23	no middle man