| 0 | 0 | peano |
| 1 | 4 | intro * index * pyk * tex * end intro |
| 2 | 3 | intro * pyk * tex * end intro |
| 3 | 0 | peano zero |
| 4 | 0 | peano one |
| 5 | 0 | peano two |
| 6 | 0 | peano a |
| 7 | 0 | peano b |
| 8 | 0 | peano c |
| 9 | 0 | peano d |
| 10 | 0 | peano e |
| 11 | 0 | peano f |
| 12 | 0 | peano g |
| 13 | 0 | peano h |
| 14 | 0 | peano i |
| 15 | 0 | peano j |
| 16 | 0 | peano k |
| 17 | 0 | peano l |
| 18 | 0 | peano m |
| 19 | 0 | peano n |
| 20 | 0 | peano o |
| 21 | 0 | peano p |
| 22 | 0 | peano q |
| 23 | 0 | peano r |
| 24 | 0 | peano s |
| 25 | 0 | peano t |
| 26 | 0 | peano u |
| 27 | 0 | peano v |
| 28 | 0 | peano w |
| 29 | 0 | peano x |
| 30 | 0 | peano y |
| 31 | 0 | peano z |
| 32 | 2 | peano nonfree * in * end nonfree |
| 33 | 2 | peano nonfree star * in * end nonfree |
| 34 | 3 | peano free * set * to * end free |
| 35 | 3 | peano free star * set * to * end free |
| 36 | 4 | peano sub * is * where * is * end sub |
| 37 | 4 | peano sub star * is * where * is * end sub |
| 38 | 0 | system s |
| 39 | 0 | axiom a one |
| 40 | 0 | axiom a two |
| 41 | 0 | axiom a three |
| 42 | 0 | axiom a four |
| 43 | 0 | axiom a five |
| 44 | 0 | axiom s one |
| 45 | 0 | axiom s two |
| 46 | 0 | axiom s three |
| 47 | 0 | axiom s four |
| 48 | 0 | axiom s five |
| 49 | 0 | axiom s six |
| 50 | 0 | axiom s seven |
| 51 | 0 | axiom s eight |
| 52 | 0 | axiom s nine |
| 53 | 0 | rule mp |
| 54 | 0 | rule gen |
| 55 | 0 | lemma l three two a |
| 56 | 1 | * peano var |
| 57 | 1 | * peano succ |
| 58 | 2 | * peano times * |
| 59 | 2 | * peano plus * |
| 60 | 2 | * peano is * |
| 61 | 1 | * is peano var |
| 62 | 1 | peano not * |
| 63 | 2 | * peano and * |
| 64 | 2 | * peano or * |
| 65 | 2 | peano all * indeed * |
| 66 | 2 | peano exist * indeed * |
| 67 | 2 | * peano imply * |
| 68 | 2 | * peano iff * |
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,