6252
|
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 |
|