| 0 | 0 | peano commutativity |
| 1 | 0 | weakening |
| 2 | 0 | conditioned mp prime |
| 3 | 0 | permute antecedents |
| 4 | 0 | imply transitivity |
| 5 | 0 | equal reflexivity |
| 6 | 0 | equal symmetry |
| 7 | 0 | equal transitivity |
| 8 | 0 | mendelson three two d |
| 9 | 0 | substitution macro |
| 10 | 0 | mendelson three two f base |
| 11 | 0 | mendelson three two f induction |
| 12 | 0 | mendelson three two f |
| 13 | 0 | mendelson three two g base |
| 14 | 0 | mendelson three two g induction |
| 15 | 0 | mendelson three two g |
| 16 | 0 | mendelson three two g rt switch |
| 17 | 0 | add one |
| 18 | 0 | mendelson three two d rule |
| 19 | 0 | mendelson three two d conditioned rule |
| 20 | 0 | equal transitivity rule |
| 21 | 0 | equal transitivity conditioned rule |
| 22 | 0 | plus commutativity base |
| 23 | 0 | plus commutativity induction |
| 24 | 0 | plus commutativity |
| 25 | 0 | double mp prime |
| 26 | 0 | induction macro |
| 27 | 0 | equal symmetry rule |
| 28 | 0 | double conditioned mp prime |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,