|
1 |
|
2 (* from [kleene 52] pp 118,119 *) |
|
3 |
|
4 |
|
5 val k49a = auto1 "|- [* A > ( - ( - A)) *]"; |
|
6 |
|
7 val k49b = auto1 "|- [*( - ( - ( - A))) = ( - A)*]"; |
|
8 |
|
9 val k49c = auto1 "|- [* (A | - A) > ( - - A = A) *]"; |
|
10 |
|
11 val k50a = auto2 "|- [* - (A = - A) *]"; |
|
12 |
|
13 (* |
|
14 [rtac impr_contract 1 THEN REPEAT (rtac conj_lemma 1), |
|
15 res_inst_tac [("A","!((! A) -o 0)")] cut 1 |
|
16 THEN rtac context1 1 |
|
17 THEN ALLGOALS (best_tac power_cs)]); |
|
18 *) |
|
19 |
|
20 val k51a = auto2 "|- [* - - (A | - A) *]"; |
|
21 |
|
22 val k51b = auto2 "|- [* - - (- - A > A) *]"; |
|
23 |
|
24 val k56a = auto1 "|- [* (A | B) > - (- A & - B) *]"; |
|
25 |
|
26 val k56b = auto1 "|- [* (-A | B) > - (A & -B) *]"; |
|
27 |
|
28 val k57a = auto1 "|- [* (A & B) > - (-A | -B) *]"; |
|
29 |
|
30 val k57b = auto2 "|- [* (A & -B) > -(-A | B) *]"; |
|
31 |
|
32 val k58a = auto1 "|- [* (A > B) > - (A & -B) *]"; |
|
33 |
|
34 val k58b = auto1 "|- [* (A > -B) = -(A & B) *]"; |
|
35 |
|
36 val k58c = auto1 "|- [* - (A & B) = (- - A > - B) *]"; |
|
37 |
|
38 val k58d = auto1 "|- [* (- - A > - B) = - - (-A | -B) *]"; |
|
39 |
|
40 val k58e = auto1 "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"; |
|
41 |
|
42 val k58f = auto1 "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"; |
|
43 |
|
44 val k58g = auto1 "|- [* (- -A > B) > - (A & -B) *]"; |
|
45 |
|
46 val k59a = auto1 "|- [* (-A | B) > (A > B) *]"; |
|
47 |
|
48 val k59b = auto2 "|- [* (A > B) > - - (-A | B) *]"; |
|
49 |
|
50 val k59c = auto2 "|- [* (-A > B) > - -(A | B) *]"; |
|
51 |
|
52 val k60a = auto1 "|- [* (A & B) > - (A > -B) *]"; |
|
53 |
|
54 val k60b = auto1 "|- [* (A & -B) > - (A > B) *]"; |
|
55 |
|
56 val k60c = auto1 "|- [* ( - - A & B) > - (A > -B) *]"; |
|
57 |
|
58 val k60d = auto1 "|- [* (- - A & - B) = - (A > B) *]"; |
|
59 |
|
60 val k60e = auto1 "|- [* - (A > B) = - (-A | B) *]"; |
|
61 |
|
62 val k60f = auto1 "|- [* - (-A | B) = - - (A & -B) *]"; |
|
63 |
|
64 val k60g = auto2 "|- [* - - (A > B) = - (A & -B) *]"; |
|
65 |
|
66 (* |
|
67 [step_tac safe_cs 1, best_tac safe_cs 1, |
|
68 rtac impr 1 THEN rtac impr_contract 1 |
|
69 THEN best_tac safe_cs 1]; |
|
70 *) |
|
71 |
|
72 val k60h = auto1 "|- [* - (A & -B) = (A > - -B) *]"; |
|
73 |
|
74 val k60i = auto1 "|- [* (A > - -B) = (- -A > - -B) *]"; |
|
75 |
|
76 val k61a = auto1 "|- [* (A | B) > (-A > B) *]"; |
|
77 |
|
78 val k61b = auto2 "|- [* - (A | B) = - (-A > B) *]"; |
|
79 |
|
80 val k62a = auto1 "|- [* (-A | -B) > - (A & B) *]"; |
|
81 |