Logiweb codex of base in pyk
Up
Help
ref-0-id-0
base
ref-0-id-1
proclaim {MissingArg} as {MissingArg} end proclaim
ref-0-id-2
unicode start of text {MissingArg} end unicode text
ref-0-id-3
unicode end of text
ref-0-id-4
{MissingArg} , {MissingArg}
ref-0-id-5
{MissingArg} [ {MissingArg} ] {MissingArg}
ref-0-id-6
preassociative {MissingArg} greater than {MissingArg}
ref-0-id-7
postassociative {MissingArg} greater than {MissingArg}
ref-0-id-8
priority {MissingArg} equal {MissingArg}
ref-0-id-9
priority {MissingArg} end priority
ref-0-id-10
unicode newline {MissingArg}
ref-0-id-11
x
ref-0-id-12
text {MissingArg} end text
ref-0-id-13
text {MissingArg} plus {MissingArg}
ref-0-id-14
text {MissingArg} plus indent {MissingArg}
ref-0-id-15
pyk
ref-0-id-16
define {MissingArg} of {MissingArg} as {MissingArg} end define
ref-0-id-17
{MissingArg} linebreak {MissingArg}
ref-0-id-18
bracket {MissingArg} end bracket
ref-0-id-19
big bracket {MissingArg} end bracket
ref-0-id-20
math {MissingArg} end math
ref-0-id-21
flush left {MissingArg} end left
ref-0-id-22
var x
ref-0-id-23
var y
ref-0-id-24
var z
ref-0-id-25
tex
ref-0-id-26
tex name
ref-0-id-27
priority
ref-0-id-28
true
ref-0-id-29
if {MissingArg} then {MissingArg} else {MissingArg} end if
ref-0-id-30
introduce {MissingArg} of {MissingArg} as {MissingArg} end introduce
ref-0-id-31
value
ref-0-id-32
unicode space {MissingArg}
ref-0-id-33
unicode exclamation mark {MissingArg}
ref-0-id-34
unicode quotation mark {MissingArg}
ref-0-id-35
unicode number sign {MissingArg}
ref-0-id-36
unicode dollar sign {MissingArg}
ref-0-id-37
unicode percent {MissingArg}
ref-0-id-38
unicode ampersand {MissingArg}
ref-0-id-39
unicode apostrophe {MissingArg}
ref-0-id-40
unicode left parenthesis {MissingArg}
ref-0-id-41
unicode right parenthesis {MissingArg}
ref-0-id-42
unicode asterisk {MissingArg}
ref-0-id-43
unicode plus sign {MissingArg}
ref-0-id-44
unicode comma {MissingArg}
ref-0-id-45
unicode hyphen {MissingArg}
ref-0-id-46
unicode period {MissingArg}
ref-0-id-47
unicode slash {MissingArg}
ref-0-id-48
unicode zero {MissingArg}
ref-0-id-49
unicode one {MissingArg}
ref-0-id-50
unicode two {MissingArg}
ref-0-id-51
unicode three {MissingArg}
ref-0-id-52
unicode four {MissingArg}
ref-0-id-53
unicode five {MissingArg}
ref-0-id-54
unicode six {MissingArg}
ref-0-id-55
unicode seven {MissingArg}
ref-0-id-56
unicode eight {MissingArg}
ref-0-id-57
unicode nine {MissingArg}
ref-0-id-58
unicode colon {MissingArg}
ref-0-id-59
unicode semicolon {MissingArg}
ref-0-id-60
unicode less than {MissingArg}
ref-0-id-61
unicode equal sign {MissingArg}
ref-0-id-62
unicode greater than {MissingArg}
ref-0-id-63
unicode question mark {MissingArg}
ref-0-id-64
unicode commercial at {MissingArg}
ref-0-id-65
unicode capital a {MissingArg}
ref-0-id-66
unicode capital b {MissingArg}
ref-0-id-67
unicode capital c {MissingArg}
ref-0-id-68
unicode capital d {MissingArg}
ref-0-id-69
unicode capital e {MissingArg}
ref-0-id-70
unicode capital f {MissingArg}
ref-0-id-71
unicode capital g {MissingArg}
ref-0-id-72
unicode capital h {MissingArg}
ref-0-id-73
unicode capital i {MissingArg}
ref-0-id-74
unicode capital j {MissingArg}
ref-0-id-75
unicode capital k {MissingArg}
ref-0-id-76
unicode capital l {MissingArg}
ref-0-id-77
unicode capital m {MissingArg}
ref-0-id-78
unicode capital n {MissingArg}
ref-0-id-79
unicode capital o {MissingArg}
ref-0-id-80
unicode capital p {MissingArg}
ref-0-id-81
unicode capital q {MissingArg}
ref-0-id-82
unicode capital r {MissingArg}
ref-0-id-83
unicode capital s {MissingArg}
ref-0-id-84
unicode capital t {MissingArg}
ref-0-id-85
unicode capital u {MissingArg}
ref-0-id-86
unicode capital v {MissingArg}
ref-0-id-87
unicode capital w {MissingArg}
ref-0-id-88
unicode capital x {MissingArg}
ref-0-id-89
unicode capital y {MissingArg}
ref-0-id-90
unicode capital z {MissingArg}
ref-0-id-91
unicode left bracket {MissingArg}
ref-0-id-92
unicode backslash {MissingArg}
ref-0-id-93
unicode right bracket {MissingArg}
ref-0-id-94
unicode circumflex {MissingArg}
ref-0-id-95
unicode underscore {MissingArg}
ref-0-id-96
unicode grave accent {MissingArg}
ref-0-id-97
unicode small a {MissingArg}
ref-0-id-98
unicode small b {MissingArg}
ref-0-id-99
unicode small c {MissingArg}
ref-0-id-100
unicode small d {MissingArg}
ref-0-id-101
unicode small e {MissingArg}
ref-0-id-102
unicode small f {MissingArg}
ref-0-id-103
unicode small g {MissingArg}
ref-0-id-104
unicode small h {MissingArg}
ref-0-id-105
unicode small i {MissingArg}
ref-0-id-106
unicode small j {MissingArg}
ref-0-id-107
unicode small k {MissingArg}
ref-0-id-108
unicode small l {MissingArg}
ref-0-id-109
unicode small m {MissingArg}
ref-0-id-110
unicode small n {MissingArg}
ref-0-id-111
unicode small o {MissingArg}
ref-0-id-112
unicode small p {MissingArg}
ref-0-id-113
unicode small q {MissingArg}
ref-0-id-114
unicode small r {MissingArg}
ref-0-id-115
unicode small s {MissingArg}
ref-0-id-116
unicode small t {MissingArg}
ref-0-id-117
unicode small u {MissingArg}
ref-0-id-118
unicode small v {MissingArg}
ref-0-id-119
unicode small w {MissingArg}
ref-0-id-120
unicode small x {MissingArg}
ref-0-id-121
unicode small y {MissingArg}
ref-0-id-122
unicode small z {MissingArg}
ref-0-id-123
unicode left brace {MissingArg}
ref-0-id-124
unicode vertical line {MissingArg}
ref-0-id-125
unicode right brace {MissingArg}
ref-0-id-126
unicode tilde {MissingArg}
ref-0-id-127
claim
ref-0-id-128
bottom
ref-0-id-129
function f of {MissingArg} end function
ref-0-id-130
identity {MissingArg} end identity
ref-0-id-131
false
ref-0-id-132
untagged zero
ref-0-id-133
untagged one
ref-0-id-134
untagged two
ref-0-id-135
untagged three
ref-0-id-136
untagged four
ref-0-id-137
untagged five
ref-0-id-138
untagged six
ref-0-id-139
untagged seven
ref-0-id-140
untagged eight
ref-0-id-141
untagged nine
ref-0-id-142
zero
ref-0-id-143
one
ref-0-id-144
two
ref-0-id-145
three
ref-0-id-146
four
ref-0-id-147
five
ref-0-id-148
six
ref-0-id-149
seven
ref-0-id-150
eight
ref-0-id-151
nine
ref-0-id-152
var a
ref-0-id-153
var b
ref-0-id-154
var c
ref-0-id-155
var d
ref-0-id-156
var e
ref-0-id-157
var f
ref-0-id-158
var g
ref-0-id-159
var h
ref-0-id-160
var i
ref-0-id-161
var j
ref-0-id-162
var k
ref-0-id-163
var l
ref-0-id-164
var m
ref-0-id-165
var n
ref-0-id-166
var o
ref-0-id-167
var p
ref-0-id-168
var q
ref-0-id-169
var r
ref-0-id-170
var s
ref-0-id-171
var t
ref-0-id-172
var u
ref-0-id-173
var v
ref-0-id-174
var w
ref-0-id-175
tagged parenthesis {MissingArg} end tagged
ref-0-id-176
tagged if {MissingArg} then {MissingArg} else {MissingArg} end if
ref-0-id-177
array {MissingArg} is {MissingArg} end array
ref-0-id-178
left
ref-0-id-179
center
ref-0-id-180
right
ref-0-id-181
empty
ref-0-id-182
substitute {MissingArg} set {MissingArg} to {MissingArg} end substitute
ref-0-id-183
map tag {MissingArg} end tag
ref-0-id-184
raw map untag {MissingArg} end untag
ref-0-id-185
map untag {MissingArg} end untag
ref-0-id-186
normalizing untag {MissingArg} end untag
ref-0-id-187
apply {MissingArg} to {MissingArg} end apply
ref-0-id-188
apply one {MissingArg} to {MissingArg} end apply
ref-0-id-189
identifier {MissingArg} end identifier
ref-0-id-190
identifier one {MissingArg} plus id {MissingArg} end identifier
ref-0-id-191
array plus {MissingArg} and {MissingArg} end plus
ref-0-id-192
array remove {MissingArg} array {MissingArg} level {MissingArg} end remove
ref-0-id-193
array put {MissingArg} value {MissingArg} array {MissingArg} level {MissingArg} end put
ref-0-id-194
array add {MissingArg} value {MissingArg} index {MissingArg} value {MissingArg} level {MissingArg} end add
ref-0-id-195
bit {MissingArg} of {MissingArg} end bit
ref-0-id-196
bit one {MissingArg} of {MissingArg} end bit
ref-0-id-197
example rack
ref-0-id-198
vector hook
ref-0-id-199
bibliography hook
ref-0-id-200
dictionary hook
ref-0-id-201
body hook
ref-0-id-202
codex hook
ref-0-id-203
expansion hook
ref-0-id-204
code hook
ref-0-id-205
cache hook
ref-0-id-206
diagnose hook
ref-0-id-207
pyk aspect
ref-0-id-208
tex aspect
ref-0-id-209
texname aspect
ref-0-id-210
value aspect
ref-0-id-211
message aspect
ref-0-id-212
macro aspect
ref-0-id-213
definition aspect
ref-0-id-214
unpack aspect
ref-0-id-215
claim aspect
ref-0-id-216
priority aspect
ref-0-id-217
lambda identifier
ref-0-id-218
apply identifier
ref-0-id-219
true identifier
ref-0-id-220
if identifier
ref-0-id-221
quote identifier
ref-0-id-222
proclaim identifier
ref-0-id-223
define identifier
ref-0-id-224
introduce identifier
ref-0-id-225
hide identifier
ref-0-id-226
pre identifier
ref-0-id-227
post identifier
ref-0-id-228
eval {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-229
eval two {MissingArg} ref {MissingArg} id {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-230
eval three {MissingArg} function {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-231
eval four {MissingArg} arguments {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-232
lookup {MissingArg} stack {MissingArg} default {MissingArg} end lookup
ref-0-id-233
abstract {MissingArg} term {MissingArg} stack {MissingArg} cache {MissingArg} end abstract
ref-0-id-234
quote {MissingArg} end quote
ref-0-id-235
expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-236
expand two {MissingArg} definition {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-237
expand list {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-238
macro
ref-0-id-239
macro state
ref-0-id-240
zip {MissingArg} with {MissingArg} end zip
ref-0-id-241
assoc one {MissingArg} address {MissingArg} index {MissingArg} end assoc
ref-0-id-242
protect {MissingArg} end protect
ref-0-id-243
self
ref-0-id-244
macro define {MissingArg} as {MissingArg} end define
ref-0-id-245
value define {MissingArg} as {MissingArg} end define
ref-0-id-246
intro define {MissingArg} as {MissingArg} end define
ref-0-id-247
pyk define {MissingArg} as {MissingArg} end define
ref-0-id-248
tex define {MissingArg} as {MissingArg} end define
ref-0-id-249
tex name define {MissingArg} as {MissingArg} end define
ref-0-id-250
priority table {MissingArg} end table
ref-0-id-251
macro define one
ref-0-id-252
macro define two {MissingArg} end define
ref-0-id-253
macro define three {MissingArg} end define
ref-0-id-254
macro define four {MissingArg} state {MissingArg} cache {MissingArg} definition {MissingArg} end define
ref-0-id-255
state expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-256
quote expand {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-257
quote expand two {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-258
quote expand three {MissingArg} term {MissingArg} stack {MissingArg} value {MissingArg} end expand
ref-0-id-259
quote expand star {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-260
parenthesis {MissingArg} end parenthesis
ref-0-id-261
big parenthesis {MissingArg} end parenthesis
ref-0-id-262
display {MissingArg} end display
ref-0-id-263
statement {MissingArg} end statement
ref-0-id-264
spying test {MissingArg} end test
ref-0-id-265
false spying test {MissingArg} end test
ref-0-id-266
aspect {MissingArg} subcodex {MissingArg} end aspect
ref-0-id-267
aspect {MissingArg} term {MissingArg} cache {MissingArg} end aspect
ref-0-id-268
tuple {MissingArg} end tuple
ref-0-id-269
tuple one {MissingArg} end tuple
ref-0-id-270
tuple two {MissingArg} end tuple
ref-0-id-271
let two {MissingArg} apply {MissingArg} end let
ref-0-id-272
let one {MissingArg} apply {MissingArg} end let
ref-0-id-273
claim define {MissingArg} as {MissingArg} end define
ref-0-id-274
checker
ref-0-id-275
check {MissingArg} cache {MissingArg} end check
ref-0-id-276
check two {MissingArg} cache {MissingArg} def {MissingArg} end check
ref-0-id-277
check three {MissingArg} cache {MissingArg} def {MissingArg} end check
ref-0-id-278
check list {MissingArg} cache {MissingArg} end check
ref-0-id-279
check list two {MissingArg} cache {MissingArg} value {MissingArg} end check
ref-0-id-280
test {MissingArg} end test
ref-0-id-281
false test {MissingArg} end test
ref-0-id-282
raw test {MissingArg} end test
ref-0-id-283
message
ref-0-id-284
message define {MissingArg} as {MissingArg} end define
ref-0-id-285
the statement aspect
ref-0-id-286
statement
ref-0-id-287
statement define {MissingArg} as {MissingArg} end define
ref-0-id-288
example axiom
ref-0-id-289
example scheme
ref-0-id-290
example rule
ref-0-id-291
absurdity
ref-0-id-292
contraexample
ref-0-id-293
example theory primed
ref-0-id-294
example lemma
ref-0-id-295
metavar {MissingArg} end metavar
ref-0-id-296
meta a
ref-0-id-297
meta b
ref-0-id-298
meta c
ref-0-id-299
meta d
ref-0-id-300
meta e
ref-0-id-301
meta f
ref-0-id-302
meta g
ref-0-id-303
meta h
ref-0-id-304
meta i
ref-0-id-305
meta j
ref-0-id-306
meta k
ref-0-id-307
meta l
ref-0-id-308
meta m
ref-0-id-309
meta n
ref-0-id-310
meta o
ref-0-id-311
meta p
ref-0-id-312
meta q
ref-0-id-313
meta r
ref-0-id-314
meta s
ref-0-id-315
meta t
ref-0-id-316
meta u
ref-0-id-317
meta v
ref-0-id-318
meta w
ref-0-id-319
meta x
ref-0-id-320
meta y
ref-0-id-321
meta z
ref-0-id-322
sub {MissingArg} set {MissingArg} to {MissingArg} end sub
ref-0-id-323
sub star {MissingArg} set {MissingArg} to {MissingArg} end sub
ref-0-id-324
the empty set
ref-0-id-325
example remainder
ref-0-id-326
make visible {MissingArg} end visible
ref-0-id-327
intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-328
intro {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-329
error {MissingArg} term {MissingArg} end error
ref-0-id-330
error two {MissingArg} term {MissingArg} end error
ref-0-id-331
proof {MissingArg} term {MissingArg} cache {MissingArg} end proof
ref-0-id-332
proof two {MissingArg} term {MissingArg} end proof
ref-0-id-333
sequent eval {MissingArg} term {MissingArg} end eval
ref-0-id-334
seqeval init {MissingArg} term {MissingArg} end eval
ref-0-id-335
seqeval modus {MissingArg} term {MissingArg} end eval
ref-0-id-336
seqeval modus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-337
seqeval verify {MissingArg} term {MissingArg} end eval
ref-0-id-338
seqeval verify one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-339
sequent eval plus {MissingArg} term {MissingArg} end eval
ref-0-id-340
seqeval plus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-341
seqeval minus {MissingArg} term {MissingArg} end eval
ref-0-id-342
seqeval minus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-343
seqeval deref {MissingArg} term {MissingArg} end eval
ref-0-id-344
seqeval deref one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-345
seqeval deref two {MissingArg} term {MissingArg} sequent {MissingArg} def {MissingArg} end eval
ref-0-id-346
seqeval at {MissingArg} term {MissingArg} end eval
ref-0-id-347
seqeval at one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-348
seqeval infer {MissingArg} term {MissingArg} end eval
ref-0-id-349
seqeval infer one {MissingArg} term {MissingArg} premise {MissingArg} sequent {MissingArg} end eval
ref-0-id-350
seqeval endorse {MissingArg} term {MissingArg} end eval
ref-0-id-351
seqeval endorse one {MissingArg} term {MissingArg} side {MissingArg} sequent {MissingArg} end eval
ref-0-id-352
seqeval est {MissingArg} term {MissingArg} end eval
ref-0-id-353
seqeval est one {MissingArg} term {MissingArg} name {MissingArg} sequent {MissingArg} end eval
ref-0-id-354
seqeval est two {MissingArg} term {MissingArg} name {MissingArg} sequent {MissingArg} def {MissingArg} end eval
ref-0-id-355
seqeval all {MissingArg} term {MissingArg} end eval
ref-0-id-356
seqeval all one {MissingArg} term {MissingArg} variable {MissingArg} sequent {MissingArg} end eval
ref-0-id-357
seqeval cut {MissingArg} term {MissingArg} end eval
ref-0-id-358
seqeval cut one {MissingArg} term {MissingArg} forerunner {MissingArg} end eval
ref-0-id-359
seqeval cut two {MissingArg} term {MissingArg} forerunner {MissingArg} sequent {MissingArg} end eval
ref-0-id-360
computably true {MissingArg} end true
ref-0-id-361
claims {MissingArg} cache {MissingArg} ref {MissingArg} end claims
ref-0-id-362
claims two {MissingArg} cache {MissingArg} ref {MissingArg} end claims
ref-0-id-363
the proof aspect
ref-0-id-364
proof
ref-0-id-365
lemma {MissingArg} says {MissingArg} end lemma
ref-0-id-366
proof of {MissingArg} reads {MissingArg} end proof
ref-0-id-367
in theory {MissingArg} lemma {MissingArg} says {MissingArg} end lemma
ref-0-id-368
in theory {MissingArg} antilemma {MissingArg} says {MissingArg} end antilemma
ref-0-id-369
in theory {MissingArg} rule {MissingArg} says {MissingArg} end rule
ref-0-id-370
in theory {MissingArg} antirule {MissingArg} says {MissingArg} end antirule
ref-0-id-371
verifier
ref-0-id-372
verify one {MissingArg} end verify
ref-0-id-373
verify two {MissingArg} proofs {MissingArg} end verify
ref-0-id-374
verify three {MissingArg} ref {MissingArg} sequents {MissingArg} diagnose {MissingArg} end verify
ref-0-id-375
verify four {MissingArg} premises {MissingArg} end verify
ref-0-id-376
verify five {MissingArg} ref {MissingArg} array {MissingArg} sequents {MissingArg} end verify
ref-0-id-377
verify six {MissingArg} ref {MissingArg} list {MissingArg} sequents {MissingArg} end verify
ref-0-id-378
verify seven {MissingArg} ref {MissingArg} id {MissingArg} sequents {MissingArg} end verify
ref-0-id-379
cut {MissingArg} and {MissingArg} end cut
ref-0-id-380
head {MissingArg} end head
ref-0-id-381
tail {MissingArg} end tail
ref-0-id-382
rule one {MissingArg} theory {MissingArg} end rule
ref-0-id-383
rule {MissingArg} subcodex {MissingArg} end rule
ref-0-id-384
rule tactic
ref-0-id-385
plus {MissingArg} and {MissingArg} end plus
ref-0-id-386
theory {MissingArg} end theory
ref-0-id-387
theory two {MissingArg} cache {MissingArg} end theory
ref-0-id-388
theory three {MissingArg} name {MissingArg} end theory
ref-0-id-389
theory four {MissingArg} name {MissingArg} sum {MissingArg} end theory
ref-0-id-390
example axiom lemma primed
ref-0-id-391
example scheme lemma primed
ref-0-id-392
example rule lemma primed
ref-0-id-393
contraexample lemma primed
ref-0-id-394
example axiom lemma
ref-0-id-395
example scheme lemma
ref-0-id-396
example rule lemma
ref-0-id-397
contraexample lemma
ref-0-id-398
example theory
ref-0-id-399
ragged right
ref-0-id-400
ragged right expansion
ref-0-id-401
parameter term {MissingArg} stack {MissingArg} seed {MissingArg} end parameter
ref-0-id-402
parameter term star {MissingArg} stack {MissingArg} seed {MissingArg} end parameter
ref-0-id-403
instantiate {MissingArg} with {MissingArg} end instantiate
ref-0-id-404
instantiate star {MissingArg} with {MissingArg} end instantiate
ref-0-id-405
occur {MissingArg} in {MissingArg} substitution {MissingArg} end occur
ref-0-id-406
occur star {MissingArg} in {MissingArg} substitution {MissingArg} end occur
ref-0-id-407
unify {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-408
unify star {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-409
unify two {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-410
ell a
ref-0-id-411
ell b
ref-0-id-412
ell c
ref-0-id-413
ell d
ref-0-id-414
ell e
ref-0-id-415
ell f
ref-0-id-416
ell g
ref-0-id-417
ell h
ref-0-id-418
ell i
ref-0-id-419
ell j
ref-0-id-420
ell k
ref-0-id-421
ell l
ref-0-id-422
ell m
ref-0-id-423
ell n
ref-0-id-424
ell o
ref-0-id-425
ell p
ref-0-id-426
ell q
ref-0-id-427
ell r
ref-0-id-428
ell s
ref-0-id-429
ell t
ref-0-id-430
ell u
ref-0-id-431
ell v
ref-0-id-432
ell w
ref-0-id-433
ell x
ref-0-id-434
ell y
ref-0-id-435
ell z
ref-0-id-436
ell big a
ref-0-id-437
ell big b
ref-0-id-438
ell big c
ref-0-id-439
ell big d
ref-0-id-440
ell big e
ref-0-id-441
ell big f
ref-0-id-442
ell big g
ref-0-id-443
ell big h
ref-0-id-444
ell big i
ref-0-id-445
ell big j
ref-0-id-446
ell big k
ref-0-id-447
ell big l
ref-0-id-448
ell big m
ref-0-id-449
ell big n
ref-0-id-450
ell big o
ref-0-id-451
ell big p
ref-0-id-452
ell big q
ref-0-id-453
ell big r
ref-0-id-454
ell big s
ref-0-id-455
ell big t
ref-0-id-456
ell big u
ref-0-id-457
ell big v
ref-0-id-458
ell big w
ref-0-id-459
ell big x
ref-0-id-460
ell big y
ref-0-id-461
ell big z
ref-0-id-462
ell dummy
ref-0-id-463
sequent reflexivity
ref-0-id-464
tactic reflexivity
ref-0-id-465
sequent commutativity
ref-0-id-466
tactic commutativity
ref-0-id-467
the tactic aspect
ref-0-id-468
tactic
ref-0-id-469
tactic define {MissingArg} as {MissingArg} end define
ref-0-id-470
proof expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-471
proof expand list {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-472
proof state
ref-0-id-473
conclude one {MissingArg} cache {MissingArg} end conclude
ref-0-id-474
conclude two {MissingArg} proves {MissingArg} cache {MissingArg} end conclude
ref-0-id-475
conclude three {MissingArg} proves {MissingArg} lemma {MissingArg} substitution {MissingArg} end conclude
ref-0-id-476
conclude four {MissingArg} lemma {MissingArg} end conclude
ref-0-id-477
{MissingArg} sub {MissingArg} end sub
ref-0-id-478
{MissingArg} intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-479
{MissingArg} intro {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-480
{MissingArg} intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} name {MissingArg} end intro
ref-0-id-481
{MissingArg} intro {MissingArg} pyk {MissingArg} tex {MissingArg} name {MissingArg} end intro
ref-0-id-482
{MissingArg} prime
ref-0-id-483
{MissingArg} assoc {MissingArg} end assoc
ref-0-id-484
{MissingArg} set {MissingArg} to {MissingArg} end set
ref-0-id-485
{MissingArg} set multi {MissingArg} to {MissingArg} end set
ref-0-id-486
{MissingArg} bit nil
ref-0-id-487
{MissingArg} bit one
ref-0-id-488
binary
ref-0-id-489
{MissingArg} color {MissingArg} end color
ref-0-id-490
{MissingArg} color star {MissingArg} end color
ref-0-id-491
{MissingArg} raw head
ref-0-id-492
{MissingArg} raw tail
ref-0-id-493
{MissingArg} cardinal untag
ref-0-id-494
{MissingArg} head
ref-0-id-495
{MissingArg} tail
ref-0-id-496
{MissingArg} is singular
ref-0-id-497
{MissingArg} is cardinal
ref-0-id-498
{MissingArg} is data
ref-0-id-499
{MissingArg} is atomic
ref-0-id-500
{MissingArg} cardinal retract
ref-0-id-501
{MissingArg} tagged retract
ref-0-id-502
{MissingArg} boolean retract
ref-0-id-503
{MissingArg} ref
ref-0-id-504
{MissingArg} id
ref-0-id-505
{MissingArg} debug
ref-0-id-506
{MissingArg} root
ref-0-id-507
{MissingArg} zeroth
ref-0-id-508
{MissingArg} first
ref-0-id-509
{MissingArg} second
ref-0-id-510
{MissingArg} third
ref-0-id-511
{MissingArg} fourth
ref-0-id-512
{MissingArg} fifth
ref-0-id-513
{MissingArg} sixth
ref-0-id-514
{MissingArg} seventh
ref-0-id-515
{MissingArg} eighth
ref-0-id-516
{MissingArg} ninth
ref-0-id-517
{MissingArg} is error
ref-0-id-518
{MissingArg} is metavar
ref-0-id-519
{MissingArg} is metaclosed
ref-0-id-520
{MissingArg} is metaclosed star
ref-0-id-521
newline {MissingArg}
ref-0-id-522
macro newline {MissingArg}
ref-0-id-523
{MissingArg} apply {MissingArg}
ref-0-id-524
{MissingArg} tagged apply {MissingArg}
ref-0-id-525
{MissingArg} times {MissingArg}
ref-0-id-526
{MissingArg} times zero {MissingArg}
ref-0-id-527
{MissingArg} plus {MissingArg}
ref-0-id-528
{MissingArg} plus zero {MissingArg}
ref-0-id-529
{MissingArg} plus one {MissingArg}
ref-0-id-530
{MissingArg} minus {MissingArg}
ref-0-id-531
{MissingArg} minus zero {MissingArg}
ref-0-id-532
{MissingArg} minus one {MissingArg}
ref-0-id-533
{MissingArg} term plus {MissingArg} end plus
ref-0-id-534
{MissingArg} term union {MissingArg}
ref-0-id-535
{MissingArg} term minus {MissingArg} end minus
ref-0-id-536
{MissingArg} raw pair {MissingArg}
ref-0-id-537
{MissingArg} eager pair {MissingArg}
ref-0-id-538
{MissingArg} tagged pair {MissingArg}
ref-0-id-539
{MissingArg} untagged double {MissingArg}
ref-0-id-540
{MissingArg} pair {MissingArg}
ref-0-id-541
{MissingArg} double {MissingArg}
ref-0-id-542
{MissingArg} comma {MissingArg}
ref-0-id-543
{MissingArg} boolean equal {MissingArg}
ref-0-id-544
{MissingArg} data equal {MissingArg}
ref-0-id-545
{MissingArg} cardinal equal {MissingArg}
ref-0-id-546
{MissingArg} peano equal {MissingArg}
ref-0-id-547
{MissingArg} tagged equal {MissingArg}
ref-0-id-548
{MissingArg} math equal {MissingArg}
ref-0-id-549
{MissingArg} reduce to {MissingArg}
ref-0-id-550
{MissingArg} term equal {MissingArg}
ref-0-id-551
{MissingArg} term list equal {MissingArg}
ref-0-id-552
{MissingArg} term root equal {MissingArg}
ref-0-id-553
{MissingArg} term in {MissingArg}
ref-0-id-554
{MissingArg} term subset {MissingArg}
ref-0-id-555
{MissingArg} term set equal {MissingArg}
ref-0-id-556
{MissingArg} sequent equal {MissingArg}
ref-0-id-557
{MissingArg} free in {MissingArg}
ref-0-id-558
{MissingArg} free in star {MissingArg}
ref-0-id-559
{MissingArg} free for {MissingArg} in {MissingArg}
ref-0-id-560
{MissingArg} free for star {MissingArg} in {MissingArg}
ref-0-id-561
{MissingArg} claim in {MissingArg}
ref-0-id-562
{MissingArg} less {MissingArg}
ref-0-id-563
{MissingArg} less zero {MissingArg}
ref-0-id-564
{MissingArg} less one {MissingArg}
ref-0-id-565
not {MissingArg}
ref-0-id-566
{MissingArg} and {MissingArg}
ref-0-id-567
{MissingArg} macro and {MissingArg}
ref-0-id-568
{MissingArg} simple and {MissingArg}
ref-0-id-569
{MissingArg} claim and {MissingArg}
ref-0-id-570
{MissingArg} or {MissingArg}
ref-0-id-571
{MissingArg} parallel {MissingArg}
ref-0-id-572
{MissingArg} macro or {MissingArg}
ref-0-id-573
{MissingArg} macro imply {MissingArg}
ref-0-id-574
{MissingArg} guard {MissingArg}
ref-0-id-575
{MissingArg} spy {MissingArg}
ref-0-id-576
{MissingArg} tagged guard {MissingArg}
ref-0-id-577
{MissingArg} select {MissingArg} else {MissingArg} end select
ref-0-id-578
lambda {MissingArg} dot {MissingArg}
ref-0-id-579
tagged lambda {MissingArg} dot {MissingArg}
ref-0-id-580
tagging {MissingArg}
ref-0-id-581
open if {MissingArg} then {MissingArg} else {MissingArg}
ref-0-id-582
let {MissingArg} be {MissingArg} in {MissingArg}
ref-0-id-583
let {MissingArg} abbreviate {MissingArg} in {MissingArg}
ref-0-id-584
{MissingArg} init
ref-0-id-585
{MissingArg} modus
ref-0-id-586
{MissingArg} verify
ref-0-id-587
{MissingArg} curry plus
ref-0-id-588
{MissingArg} curry minus
ref-0-id-589
{MissingArg} dereference
ref-0-id-590
{MissingArg} at {MissingArg}
ref-0-id-591
{MissingArg} modus ponens {MissingArg}
ref-0-id-592
{MissingArg} modus probans {MissingArg}
ref-0-id-593
{MissingArg} conclude {MissingArg}
ref-0-id-594
{MissingArg} infer {MissingArg}
ref-0-id-595
{MissingArg} endorse {MissingArg}
ref-0-id-596
{MissingArg} id est {MissingArg}
ref-0-id-597
all {MissingArg} indeed {MissingArg}
ref-0-id-598
{MissingArg} rule plus {MissingArg}
ref-0-id-599
{MissingArg} cut {MissingArg}
ref-0-id-600
{MissingArg} proves {MissingArg}
ref-0-id-601
{MissingArg} proof of {MissingArg} reads {MissingArg}
ref-0-id-602
line {MissingArg} because {MissingArg} indeed {MissingArg} end line {MissingArg}
ref-0-id-603
because {MissingArg} indeed {MissingArg} qed
ref-0-id-604
line {MissingArg} premise {MissingArg} end line {MissingArg}
ref-0-id-605
line {MissingArg} side condition {MissingArg} end line {MissingArg}
ref-0-id-606
arbitrary {MissingArg} end line {MissingArg}
ref-0-id-607
locally define {MissingArg} as {MissingArg} end line {MissingArg}
ref-0-id-608
{MissingArg} tab {MissingArg}
ref-0-id-609
{MissingArg} row {MissingArg}
The pyk compiler
, version 0.grue.20060417+ by
Klaus Grue
,
GRD-2006-05-04.UTC:15:30:23.702808
=
MJD-53859.TAI:15:30:56.702808
=
LGT-4653473456702808e-6