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
The pyk compiler
, version 0.grue.20050603 by
Klaus Grue
,
GRD-2005-07-04.UTC:21:57:57.981341
=
MJD-53555.TAI:21:58:29.981341
=
LGT-4627231109981341e-6