|
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
|
