0 | 0 | logic |
1 | 0 | double rule prime mp |
2 | 0 | inference axiom prime a one |
3 | 0 | rule hypothesize |
4 | 0 | inference axiom prime a two |
5 | 0 | inference inference axiom prime a two |
6 | 0 | hypothetical rule prime mp |
7 | 0 | double inference inference axiom prime a two |
8 | 0 | double hypothetical rule prime mp |
9 | 0 | mendelson lemma one eight |
10 | 0 | inference mendelson lemma one eight |
11 | 0 | rule repetition |
12 | 0 | mendelson exercise one fourtyseven b |
13 | 0 | mendelson exercise one fourtyseven c |
14 | 0 | mendelson exercise one fourtyseven e |
15 | 0 | mendelson lemma one eleven d |
16 | 0 | hypothetical inference axiom prime a one |
17 | 0 | hypothetical inference axiom prime a two |
18 | 0 | hypothetical inference inference axiom prime a two |
19 | 0 | hypothetical mendelson exercise one fourtyseven b |
20 | 0 | hypothetical mendelson exercise one fourtyseven c |
21 | 0 | mendelson lemma one eleven c |
22 | 0 | mendelson exercise one fourtyeight d |
23 | 0 | mendelson exercise one fourtyeight e |
24 | 0 | mendelson exercise one fourtyeight h |
25 | 0 | mendelson corollary one ten a |
26 | 0 | mendelson corollary one ten b |
27 | 0 | inference axiom prime s one |
28 | 0 | inference inference axiom prime s one |
29 | 0 | inference axiom prime s two |
30 | 0 | hypothetical inference axiom prime s two |
31 | 0 | inference inference axiom prime s nine |
32 | 0 | rule induction |
33 | 0 | mendelson proposition three two a |
34 | 0 | mendelson proposition three two b |
35 | 0 | inference mendelson proposition three two b |
36 | 0 | mendelson proposition three two c |
37 | 0 | inference inference mendelson proposition three two c |
38 | 0 | hypothetical inference inference mendelson proposition three two c |
39 | 0 | mendelson proposition three two d |
40 | 0 | inference inference mendelson proposition three two d |
41 | 0 | hypothetical inference inference mendelson proposition three two d |
42 | 0 | mendelson proposition three two f |
43 | 0 | mendelson proposition three two f i |
44 | 0 | mendelson proposition three two f ii |
45 | 0 | mendelson proposition three two g |
46 | 0 | mendelson proposition three two g i |
47 | 0 | mendelson proposition three two g ii |
48 | 0 | mendelson proposition three two h |
49 | 0 | mendelson proposition three two h i |
50 | 0 | mendelson proposition three two h ii |
51 | 0 | hypothesis |
52 | 0 | instance |
53 | 0 | conclusion |
54 | 2 | * macro modus ponens * |
55 | 3 | * macro first modus ponens * macro second modus ponens * |
56 | 2 | * hypothetical macro modus ponens * |
57 | 3 | * hypothetical macro first modus ponens * hypothetical macro second modus ponens var * |
58 | 5 | line * hypothesis modus ponens * modus ponens * indeed * end line * |
59 | 5 | line * hypothesis first modus ponens * modus ponens * indeed * end line * |
60 | 5 | line * hypothesis second modus ponens * modus ponens * indeed * end line * |
61 | 6 | line * hypothesis double modus ponens * modus ponens * modus ponens * indeed * end line * |
62 | 3 | line * hypothesis indeed * end line * |
63 | 4 | line * hypothesis because * indeed * end line * |
64 | 4 | line * hypothesis raw because * indeed * end line * |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,