Logiweb codex of ijcar in pyk
Up
Help
ref-1-id-318
meta x
ref-0-id-0
ijcar
ref-0-id-1
general macro define * as * end define
ref-0-id-2
make root visible * end visible
ref-0-id-3
ijcar example axiom
ref-0-id-4
ijcar example rule
ref-0-id-5
ijcar example contradiction
ref-0-id-6
ijcar example theory
ref-0-id-7
ijcar example lemma
ref-0-id-8
set * end set
ref-0-id-9
object var * 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 * is * where * is * end sub
ref-0-id-37
sub zero * is * where * is * end sub
ref-0-id-38
sub one * is * where * is * end sub
ref-0-id-39
sub star * is * where * is * end sub
ref-0-id-40
deduction * conclude * end deduction
ref-0-id-41
deduction zero * conclude * end deduction
ref-0-id-42
deduction one * conclude * condition * end deduction
ref-0-id-43
deduction two * conclude * condition * end deduction
ref-0-id-44
deduction three * conclude * condition * bound * end deduction
ref-0-id-45
deduction four * conclude * condition * bound * end deduction
ref-0-id-46
deduction four star * conclude * condition * bound * end deduction
ref-0-id-47
deduction five * condition * bound * end deduction
ref-0-id-48
deduction six * conclude * exception * bound * end deduction
ref-0-id-49
deduction six star * conclude * exception * bound * end deduction
ref-0-id-50
deduction seven * end deduction
ref-0-id-51
deduction eight * bound * end deduction
ref-0-id-52
deduction eight * bound * 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
deduction
ref-0-id-58
axiom s one
ref-0-id-59
axiom s two
ref-0-id-60
axiom s three
ref-0-id-61
axiom s four
ref-0-id-62
axiom s five
ref-0-id-63
axiom s six
ref-0-id-64
axiom s seven
ref-0-id-65
axiom s eight
ref-0-id-66
axiom s nine
ref-0-id-67
repetition
ref-0-id-68
lemma a one
ref-0-id-69
lemma a two
ref-0-id-70
lemma a four
ref-0-id-71
lemma a five
ref-0-id-72
prop three two a
ref-0-id-73
prop three two b
ref-0-id-74
prop three two c
ref-0-id-75
prop three two d
ref-0-id-76
prop three two e one
ref-0-id-77
prop three two e two
ref-0-id-78
prop three two e
ref-0-id-79
prop three two f one
ref-0-id-80
prop three two f two
ref-0-id-81
prop three two f
ref-0-id-82
prop three two g one
ref-0-id-83
prop three two g two
ref-0-id-84
prop three two g
ref-0-id-85
prop three two h one
ref-0-id-86
prop three two h two
ref-0-id-87
prop three two h
ref-0-id-88
block one * state * cache * end block
ref-0-id-89
block two * end block
ref-0-id-90
* hide
ref-0-id-91
macro indent *
ref-0-id-92
* suc
ref-0-id-93
* equal *
ref-0-id-94
* unequal *
ref-0-id-95
* is object var
ref-0-id-96
* avoid zero *
ref-0-id-97
* avoid one *
ref-0-id-98
* avoid star *
ref-0-id-99
exist * indeed *
ref-0-id-100
for all * indeed *
ref-0-id-101
for all objects * indeed *
ref-0-id-102
* imply *
ref-0-id-103
* if and only if *
ref-0-id-104
* avoid *
ref-0-id-105
* object modus ponens *
ref-0-id-106
for all terms * indeed *
ref-0-id-107
block * line * end block *
ref-0-id-108
because * indeed * end line
ref-0-id-109
any term * end line *
ref-0-id-110
* alternative *
ref-0-id-111
evaluates to
ref-0-id-112
* safe row *
The pyk compiler
, version 0.grue.20060417 by
Klaus Grue
,
GRD-2006-03-06.UTC:13:37:57.803308
=
MJD-53800.TAI:13:38:30.803308
=
LGT-4648369110803308e-6