0 | 0 | hmpeano |
1 | 0 | prop three two a |
2 | 0 | prop three two b |
3 | 0 | prop three two b rule |
4 | 0 | prop three two c |
5 | 0 | prop three two c rule |
6 | 0 | prop three two c hyp rule |
7 | 0 | prop three two d |
8 | 0 | prop three two d rule |
9 | 0 | prop three two d hyp rule |
10 | 0 | prop three two f |
11 | 0 | prop three two f base |
12 | 0 | prop three two f ind |
13 | 0 | prop three two f t |
14 | 0 | prop three two g |
15 | 0 | prop three two g base |
16 | 0 | prop three two g ind |
17 | 0 | prop three two g rt hyp |
18 | 0 | prop three two h |
19 | 0 | prop three two h base |
20 | 0 | prop three two h ind |
21 | 0 | axiom prime s six hyp |
22 | 0 | permute premises |
23 | 0 | no middle man |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,