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 teki nina...:54 |
55 | 0 | nani teki nina...:55 |
56 | 0 | nani teki nina...: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 teki nina...: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,