ref-2-id-53
|
system s
|
ref-2-id-54
|
double negation
|
ref-2-id-55
|
rule mp
|
ref-2-id-56
|
rule gen
|
ref-2-id-57
|
deduction
|
ref-2-id-58
|
axiom s one
|
ref-2-id-59
|
axiom s two
|
ref-2-id-60
|
axiom s three
|
ref-2-id-61
|
axiom s four
|
ref-2-id-62
|
axiom s five
|
ref-2-id-63
|
axiom s six
|
ref-2-id-64
|
axiom s seven
|
ref-2-id-65
|
axiom s eight
|
ref-2-id-66
|
axiom s nine
|
ref-2-id-72
|
prop three two a
|
ref-2-id-73
|
prop three two b
|
ref-2-id-74
|
prop three two c
|
ref-2-id-75
|
prop three two d
|
ref-2-id-78
|
prop three two e
|
ref-2-id-81
|
prop three two f
|
ref-2-id-84
|
prop three two g
|
ref-2-id-87
|
prop three two h
|
ref-0-id-0
|
frozen
|
ref-0-id-1
|
numeral zero
|
ref-0-id-2
|
numeral one
|
ref-0-id-3
|
numeral two
|
ref-0-id-4
|
numeral three
|
ref-0-id-5
|
numeral four
|
ref-0-id-6
|
numeral five
|
ref-0-id-7
|
numeral six
|
ref-0-id-8
|
numeral seven
|
ref-0-id-9
|
numeral eight
|
ref-0-id-10
|
numeral nine
|
ref-0-id-11
|
rule div
|
ref-0-id-12
|
rule r
|
ref-0-id-13
|
rule r one
|
ref-0-id-14
|
rule r two
|
ref-0-id-15
|
rule r three
|
ref-0-id-16
|
rule r four
|
ref-0-id-17
|
rule r five
|
ref-0-id-18
|
rule r six
|
ref-0-id-19
|
conjel1
|
ref-0-id-20
|
conjel2
|
ref-0-id-21
|
conjin
|
ref-0-id-22
|
disjin1
|
ref-0-id-23
|
disjin2
|
ref-0-id-24
|
t one
|
ref-0-id-25
|
t zero
|
ref-0-id-26
|
h zero a
|
ref-0-id-27
|
h zero b
|
ref-0-id-28
|
h one
|
ref-0-id-29
|
h two
|
ref-0-id-30
|
axiom s ten
|
ref-0-id-31
|
prop three two
|
ref-0-id-32
|
prop three two i
|
ref-0-id-33
|
prop three two j one
|
ref-0-id-34
|
prop three two j two
|
ref-0-id-35
|
prop three two j
|
ref-0-id-36
|
prop three two k one
|
ref-0-id-37
|
prop three two k two
|
ref-0-id-38
|
prop three two k
|
ref-0-id-39
|
prop three two l one
|
ref-0-id-40
|
prop three two l two
|
ref-0-id-41
|
prop three two l
|
ref-0-id-42
|
prop three two m one
|
ref-0-id-43
|
prop three two m two
|
ref-0-id-44
|
prop three two m
|
ref-0-id-45
|
prop three two n one
|
ref-0-id-46
|
prop three two n two
|
ref-0-id-47
|
prop three two n
|
ref-0-id-48
|
prop three two o
|
ref-0-id-49
|
prop three four
|
ref-0-id-50
|
prop three four a one
|
ref-0-id-51
|
prop three four a two
|
ref-0-id-52
|
prop three four a
|
ref-0-id-53
|
prop three four b
|
ref-0-id-54
|
prop three four c one
|
ref-0-id-55
|
prop three four c two
|
ref-0-id-56
|
prop three four c
|
ref-0-id-57
|
prop three four d one
|
ref-0-id-58
|
prop three four d two
|
ref-0-id-59
|
prop three four d
|
ref-0-id-60
|
prop three five
|
ref-0-id-61
|
prop three five a
|
ref-0-id-62
|
prop three five b
|
ref-0-id-63
|
prop three five c
|
ref-0-id-64
|
prop three five d one
|
ref-0-id-65
|
prop three five d two
|
ref-0-id-66
|
prop three five d
|
ref-0-id-67
|
prop three five e one
|
ref-0-id-68
|
prop three five e two
|
ref-0-id-69
|
prop three five e
|
ref-0-id-70
|
prop three five f one
|
ref-0-id-71
|
prop three five f two
|
ref-0-id-72
|
prop three five f
|
ref-0-id-73
|
prop three five g one
|
ref-0-id-74
|
prop three five g two
|
ref-0-id-75
|
prop three five g
|
ref-0-id-76
|
prop three five h one
|
ref-0-id-77
|
prop three five h two
|
ref-0-id-78
|
prop three five h
|
ref-0-id-79
|
prop three five i one
|
ref-0-id-80
|
prop three five i two
|
ref-0-id-81
|
prop three five i
|
ref-0-id-82
|
prop three five j one
|
ref-0-id-83
|
prop three five j two
|
ref-0-id-84
|
prop three five j
|
ref-0-id-85
|
prop three seven
|
ref-0-id-86
|
prop three seven a
|
ref-0-id-87
|
prop three seven b
|
ref-0-id-88
|
prop three seven c
|
ref-0-id-89
|
prop three seven d
|
ref-0-id-90
|
prop three seven e
|
ref-0-id-91
|
prop three seven f
|
ref-0-id-92
|
prop three seven g
|
ref-0-id-93
|
prop three seven g mark
|
ref-0-id-94
|
prop three seven h
|
ref-0-id-95
|
prop three seven i
|
ref-0-id-96
|
prop three seven j
|
ref-0-id-97
|
prop three seven k
|
ref-0-id-98
|
prop three seven k mark
|
ref-0-id-99
|
prop three seven l
|
ref-0-id-100
|
prop three seven l mark
|
ref-0-id-101
|
prop three seven m
|
ref-0-id-102
|
prop three seven n
|
ref-0-id-103
|
prop three seven o
|
ref-0-id-104
|
prop three seven p
|
ref-0-id-105
|
prop three seven q
|
ref-0-id-106
|
prop three seven r
|
ref-0-id-107
|
prop three seven s
|
ref-0-id-108
|
prop three seven t
|
ref-0-id-109
|
prop three seven u
|
ref-0-id-110
|
prop three seven u mark
|
ref-0-id-111
|
prop three seven v
|
ref-0-id-112
|
prop three seven w
|
ref-0-id-113
|
prop three seven x
|
ref-0-id-114
|
prop three seven x mark
|
ref-0-id-115
|
prop three seven y
|
ref-0-id-116
|
prop three seven y mark
|
ref-0-id-117
|
prop three seven z
|
ref-0-id-118
|
prop three seven z mark
|
ref-0-id-119
|
prop three ten
|
ref-0-id-120
|
prop three ten a
|
ref-0-id-121
|
prop three ten b
|
ref-0-id-122
|
prop three ten c
|
ref-0-id-123
|
prop three ten d
|
ref-0-id-124
|
prop three ten e
|
ref-0-id-125
|
prop three ten f
|
ref-0-id-126
|
prop three ten g
|
ref-0-id-127
|
prop three ten h
|
ref-0-id-128
|
prop three eleven
|
ref-0-id-129
|
{MissingArg} ist {MissingArg}
|
ref-0-id-130
|
{MissingArg} istq {MissingArg}
|
ref-0-id-131
|
{MissingArg} inst {MissingArg}
|
ref-0-id-132
|
{MissingArg} igt {MissingArg}
|
ref-0-id-133
|
{MissingArg} igtq {MissingArg}
|
ref-0-id-134
|
{MissingArg} ingt {MissingArg}
|
ref-0-id-135
|
{MissingArg} neq {MissingArg}
|
ref-0-id-136
|
{MissingArg} and1 {MissingArg}
|
ref-0-id-137
|
{MissingArg} or1 {MissingArg}
|
ref-0-id-138
|
exists {MissingArg} indeed {MissingArg}
|
ref-0-id-139
|
{MissingArg} divides {MissingArg}
|
ref-0-id-140
|
{MissingArg} ldots
|