ref-0-id-0
|
opgave
|
ref-0-id-1
|
general macro define {MissingArg} as {MissingArg} end define
|
ref-0-id-2
|
make root visible {MissingArg} end visible
|
ref-0-id-3
|
sequent example axiom
|
ref-0-id-4
|
sequent example rule
|
ref-0-id-5
|
sequent example contradiction
|
ref-0-id-6
|
sequent example theory
|
ref-0-id-7
|
sequent example lemma
|
ref-0-id-8
|
set {MissingArg} end set
|
ref-0-id-9
|
object var {MissingArg} end var
|
ref-0-id-10
|
object a
|
ref-0-id-11
|
object b
|
ref-0-id-12
|
object c
|
ref-0-id-13
|
object d
|
ref-0-id-14
|
object e
|
ref-0-id-15
|
object f
|
ref-0-id-16
|
object g
|
ref-0-id-17
|
object h
|
ref-0-id-18
|
object i
|
ref-0-id-19
|
object j
|
ref-0-id-20
|
object k
|
ref-0-id-21
|
object l
|
ref-0-id-22
|
object m
|
ref-0-id-23
|
object n
|
ref-0-id-24
|
object o
|
ref-0-id-25
|
object p
|
ref-0-id-26
|
object q
|
ref-0-id-27
|
object r
|
ref-0-id-28
|
object s
|
ref-0-id-29
|
object t
|
ref-0-id-30
|
object u
|
ref-0-id-31
|
object v
|
ref-0-id-32
|
object w
|
ref-0-id-33
|
object x
|
ref-0-id-34
|
object y
|
ref-0-id-35
|
object z
|
ref-0-id-36
|
sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-37
|
sub zero {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-38
|
sub one {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-39
|
sub star {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
|
ref-0-id-40
|
deduction {MissingArg} conclude {MissingArg} end deduction
|
ref-0-id-41
|
deduction zero {MissingArg} conclude {MissingArg} end deduction
|
ref-0-id-42
|
deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end deduction
|
ref-0-id-43
|
deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end deduction
|
ref-0-id-44
|
deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-45
|
deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-46
|
deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-47
|
deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-48
|
deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-49
|
deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-50
|
deduction seven {MissingArg} end deduction
|
ref-0-id-51
|
deduction eight {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-52
|
deduction eight star {MissingArg} bound {MissingArg} end deduction
|
ref-0-id-53
|
system s
|
ref-0-id-54
|
double negation
|
ref-0-id-55
|
rule mp
|
ref-0-id-56
|
rule gen
|
ref-0-id-57
|
rule div
|
ref-0-id-58
|
deduction
|
ref-0-id-59
|
axiom s one
|
ref-0-id-60
|
axiom s two
|
ref-0-id-61
|
axiom s three
|
ref-0-id-62
|
axiom s four
|
ref-0-id-63
|
axiom s five
|
ref-0-id-64
|
axiom s six
|
ref-0-id-65
|
axiom s seven
|
ref-0-id-66
|
axiom s eight
|
ref-0-id-67
|
axiom s nine
|
ref-0-id-68
|
axiom s ten
|
ref-0-id-69
|
repetition
|
ref-0-id-70
|
lemma a one
|
ref-0-id-71
|
lemma a two
|
ref-0-id-72
|
lemma a four
|
ref-0-id-73
|
lemma a five
|
ref-0-id-74
|
prop three two a
|
ref-0-id-75
|
prop three two b
|
ref-0-id-76
|
prop three two c
|
ref-0-id-77
|
prop three two d
|
ref-0-id-78
|
prop three two e one
|
ref-0-id-79
|
prop three two e two
|
ref-0-id-80
|
prop three two e
|
ref-0-id-81
|
prop three two f one
|
ref-0-id-82
|
prop three two f two
|
ref-0-id-83
|
prop three two f
|
ref-0-id-84
|
prop three two g one
|
ref-0-id-85
|
prop three two g two
|
ref-0-id-86
|
prop three two g
|
ref-0-id-87
|
prop three two h one
|
ref-0-id-88
|
prop three two h two
|
ref-0-id-89
|
prop three two h
|
ref-0-id-90
|
prop three two i
|
ref-0-id-91
|
prop three two j one
|
ref-0-id-92
|
prop three two j two
|
ref-0-id-93
|
prop three two j
|
ref-0-id-94
|
prop three two k one
|
ref-0-id-95
|
prop three two k two
|
ref-0-id-96
|
prop three two k
|
ref-0-id-97
|
prop three two l one
|
ref-0-id-98
|
prop three two l two
|
ref-0-id-99
|
prop three two l
|
ref-0-id-100
|
prop three two m one
|
ref-0-id-101
|
prop three two m two
|
ref-0-id-102
|
prop three two m
|
ref-0-id-103
|
prop three two n one
|
ref-0-id-104
|
prop three two n two
|
ref-0-id-105
|
prop three two n
|
ref-0-id-106
|
prop three two o
|
ref-0-id-107
|
prop three four a one
|
ref-0-id-108
|
prop three four a two
|
ref-0-id-109
|
prop three four a
|
ref-0-id-110
|
prop three four b
|
ref-0-id-111
|
prop three four c one
|
ref-0-id-112
|
prop three four c two
|
ref-0-id-113
|
prop three four c
|
ref-0-id-114
|
prop three four d one
|
ref-0-id-115
|
prop three four d two
|
ref-0-id-116
|
prop three four d
|
ref-0-id-117
|
block one {MissingArg} state {MissingArg} cache {MissingArg} end block
|
ref-0-id-118
|
block two {MissingArg} end block
|
ref-0-id-119
|
{MissingArg} hide
|
ref-0-id-120
|
macro indent {MissingArg}
|
ref-0-id-121
|
{MissingArg} suc
|
ref-0-id-122
|
{MissingArg} equal {MissingArg}
|
ref-0-id-123
|
{MissingArg} unequal {MissingArg}
|
ref-0-id-124
|
{MissingArg} is object var
|
ref-0-id-125
|
{MissingArg} avoid zero {MissingArg}
|
ref-0-id-126
|
{MissingArg} avoid one {MissingArg}
|
ref-0-id-127
|
{MissingArg} avoid star {MissingArg}
|
ref-0-id-128
|
exist {MissingArg} indeed {MissingArg}
|
ref-0-id-129
|
for all {MissingArg} indeed {MissingArg}
|
ref-0-id-130
|
for all objects {MissingArg} indeed {MissingArg}
|
ref-0-id-131
|
{MissingArg} imply {MissingArg}
|
ref-0-id-132
|
{MissingArg} if and only if {MissingArg}
|
ref-0-id-133
|
{MissingArg} avoid {MissingArg}
|
ref-0-id-134
|
{MissingArg} object modus ponens {MissingArg}
|
ref-0-id-135
|
for all terms {MissingArg} indeed {MissingArg}
|
ref-0-id-136
|
block {MissingArg} line {MissingArg} end block {MissingArg}
|
ref-0-id-137
|
because {MissingArg} indeed {MissingArg} end line
|
ref-0-id-138
|
any term {MissingArg} end line {MissingArg}
|
ref-0-id-139
|
{MissingArg} alternative {MissingArg}
|
ref-0-id-140
|
evaluates to
|
ref-0-id-141
|
{MissingArg} safe row {MissingArg}
|
ref-0-id-142
|
{MissingArg} divides {MissingArg}
|