Logiweb codex of pok in pyk
Up
Help
ref-0-id-0
pok
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}
The pyk compiler
, version 0.grue.20060417+ by
Klaus Grue
,
GRD-2006-06-21.UTC:11:30:14.300977
=
MJD-53907.TAI:11:30:47.300977
=
LGT-4657606247300977e-6