| 0 | 0 | proofreport |
| 1 | 0 | peano zero |
| 2 | 0 | peano one |
| 3 | 0 | peano two |
| 4 | 0 | peano a |
| 5 | 0 | peano b |
| 6 | 0 | peano c |
| 7 | 0 | peano d |
| 8 | 0 | peano e |
| 9 | 0 | peano f |
| 10 | 0 | peano g |
| 11 | 0 | peano h |
| 12 | 0 | peano i |
| 13 | 0 | peano j |
| 14 | 0 | peano k |
| 15 | 0 | peano l |
| 16 | 0 | peano m |
| 17 | 0 | peano n |
| 18 | 0 | peano o |
| 19 | 0 | peano p |
| 20 | 0 | peano q |
| 21 | 0 | peano r |
| 22 | 0 | peano s |
| 23 | 0 | peano t |
| 24 | 0 | peano u |
| 25 | 0 | peano v |
| 26 | 0 | peano w |
| 27 | 0 | peano x |
| 28 | 0 | peano y |
| 29 | 0 | peano z |
| 30 | 2 | peano nonfree * in * end nonfree |
| 31 | 2 | peano nonfree star * in * end nonfree |
| 32 | 3 | peano free * set * to * end free |
| 33 | 3 | peano free star * set * to * end free |
| 34 | 4 | peano sub * is * where * is * end sub |
| 35 | 4 | peano sub star * is * where * is * end sub |
| 36 | 0 | system prime s |
| 37 | 0 | axiom prime a one |
| 38 | 0 | axiom prime a two |
| 39 | 0 | axiom prime a three |
| 40 | 0 | axiom prime a four |
| 41 | 0 | axiom prime a five |
| 42 | 0 | axiom prime s one |
| 43 | 0 | axiom prime s two |
| 44 | 0 | axiom prime s three |
| 45 | 0 | axiom prime s four |
| 46 | 0 | axiom prime s five |
| 47 | 0 | axiom prime s six |
| 48 | 0 | axiom prime s seven |
| 49 | 0 | axiom prime s eight |
| 50 | 0 | axiom prime s nine |
| 51 | 0 | rule prime mp |
| 52 | 0 | rule prime gen |
| 53 | 0 | lemma prime l three two a |
| 54 | 0 | nani nase kita...:54 |
| 55 | 0 | nani nase kita...:55 |
| 56 | 0 | nani nase kita...:56 |
| 57 | 0 | lemma prime l three two b |
| 58 | 0 | lemma prime l three two c |
| 59 | 0 | lemma prime l three two d one |
| 60 | 0 | lemma prime l three two d two |
| 61 | 0 | lemma prime l three two f |
| 62 | 0 | lemma prime l three two g |
| 63 | 0 | lemma prime l three two h one |
| 64 | 0 | lemma prime l three two h two |
| 65 | 0 | lemma prime l three two h |
| 66 | 0 | nani nase kita...:66 |
| 67 | 0 | hypothetical three two d |
| 68 | 0 | mendelson corollary one ten a |
| 69 | 0 | mendelson corollary one ten b |
| 70 | 0 | mendelson corollary one ten pre b |
| 71 | 0 | mendelson corollary one ten b plus plus |
| 72 | 0 | hypothetical rule prime mp plus plus |
| 73 | 0 | hypothesize plus plus |
| 74 | 0 | mendelson one seven plus plus |
| 75 | 0 | mendelson one seven |
| 76 | 0 | hypothetical rule prime mp |
| 77 | 0 | hypothesize |
| 78 | 0 | hypothetical rule prime gen |
| 79 | 0 | mendelson three two a |
| 80 | 0 | hypothetical three two a |
| 81 | 0 | hypothetical three two b |
| 82 | 0 | hypothetical three one s one |
| 83 | 0 | hypothetical three two c |
| 84 | 0 | hypothetical three one s two |
| 85 | 0 | hypothetical three one s five |
| 86 | 0 | hypothetical three one s six |
| 87 | 0 | mendelson three two f |
| 88 | 1 | * peano var |
| 89 | 1 | * peano succ |
| 90 | 2 | * peano times * |
| 91 | 2 | * peano plus * |
| 92 | 2 | * peano is * |
| 93 | 1 | * is peano var |
| 94 | 1 | peano not * |
| 95 | 2 | * peano and * |
| 96 | 2 | * peano or * |
| 97 | 2 | peano all * indeed * |
| 98 | 2 | peano exist * indeed * |
| 99 | 2 | * peano imply * |
| 100 | 2 | * peano iff * |
| 101 | 2 | * macro modus ponens * |
| 102 | 2 | * hypothetical modus ponens * |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,