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