setprecrightabove "*" "+"; (* 2 *) Axiom "reflx" [] ["a1=a1"]; (* 3 *) (* 2 reflx: |- 1: a1 = a1 *) (* 3 *) Axiom "symm" [] ["(a1=a2)->(a2=a1)"]; (* 4 *) (* 3 symm: |- 1: a1 = a2 -> a2 = a1 *) (* 4 *) Axiom "trans" [] ["((a1=a2)&(a2=a3))->(a1=a3)"]; (* 5 *) (* 4 trans: |- 1: a1 = a2 & a2 = a3 -> a1 = a3 *) (* 5 *) Axiom "rplus" [] ["Real(a1+a2)"]; (* 6 *) (* 5 rplus: |- 1: Real(a1 + a2) *) (* 6 *) Axiom "rtimes" [] ["Real(a1*a2)"]; (* 7 *) (* 6 rtimes: |- 1: Real(a1 * a2) *) (* 7 *) Axiom "rminus" [] ["Real(-(a1))"]; (* 8 *) (* 7 rminus: |- 1: Real(-(a1)) *) (* 8 *) Axiom "rinv" [] ["Real( /(a1))"]; (* 9 *) (* 8 rinv: |- 1: Real(/(a1)) *) (* 9 *) Axiom "acom" [] ["a1+a2=a2+a1"]; (* 10 *) (* 9 acom: |- 1: a1 + a2 = a2 + a1 *) (* 10 *) Axiom "aas" [] ["[a1+a2]+a3=a1+a2+a3"]; (* 11 *) (* 10 aas: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 *) (* 11 *) Axiom "aeq" [] ["(a1=a2)->(a1+a3=a2+a3)"]; (* 12 *) (* 11 aeq: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 *) (* 12 *) Axiom "aid" [] ["a1+0=a1"]; (* 13 *) (* 12 aid: |- 1: a1 + 0 = a1 *) (* 13 *) Axiom "ainv" [] ["a1+ -(a1)=0"]; (* 14 *) (* 13 ainv: |- 1: a1 + -(a1) = 0 *) (* 14 *) Definefunction 2 "--" "x1--x2" "x1+ -(x2)"; (* 15 *) (* 15 *) Definepredicate 2 "eq" "x1 eq x2" "x1+0=x2+0"; (* 16 *) (* 16 *) Axiom "mas" [] ["[a1*a2]*a3=a1*a2*a3"]; (* 17 *) (* 16 mas: |- 1: [a1 * a2] * a3 = a1 * a2 * a3 *) (* 17 *) Axiom "mcom" [] ["a1*a2=a2*a1"]; (* 18 *) (* 17 mcom: |- 1: a1 * a2 = a2 * a1 *) (* 18 *) Axiom "meq" [] ["(a1=a2)->(a1*a3=a2*a3)"]; (* 19 *) (* 18 meq: |- 1: a1 = a2 -> a1 * a3 = a2 * a3 *) (* 19 *) Axiom "mid" [] ["a1*1=a1"]; (* 20 *) (* 19 mid: |- 1: a1 * 1 = a1 *) (* 20 *) Axiom "minv" [] ["~(a1 eq 0)-> (a1* /(a1) = 1)"]; (* 21 *) (* 20 minv: |- 1: ~a1 eq 0 -> a1 * /(a1) = 1 *) (* 21 *) Axiom "dst" [] ["a1*[a2+a3]=a1*a2+a1*a3"]; (* 22 *) (* 21 dst: |- 1: a1 * [a2 + a3] = a1 * a2 + a1 * a3 *) (* 22 *) StartSequent ["a1+a3=a2+a3"] ["a1=a2"]; (* 23 *) ThmCut "aeq"; (* 24 *) su 4 "a1+a3"; (* 25 *) su 5 "a2+a3"; (* 26 *) su 6 "-(a3)"; (* 27 *) l(); Done(); (* 29 *) ThmCut "aas"; (* 30 *) rwl []; ThmCut "aas"; (* 32 *) gl2 3; rwl []; pl 1; pl 3; ThmCut "ainv"; (* 37 *) rwl []; pl 1; ThmCut "aid"; (* 40 *) ThmCut "aid"; (* 41 *) gl2 3; rwl []; gl 4; gl2 3; rwl []; gl 2; gr 1; Done(); (* 49 *) NameSequent 1 "thm 3_1_i"; (* 50 *) (* 49 thm 3_1_i: 1: a1 + a3 = a2 + a3 |- 1: a1 = a2 *) (* 50 *) StartSequent [] ["a1*0 = 0"]; (* 51 *) ThmCut "aid"; (* 52 *) su 2 "a1"; (* 53 *) undo(); undo(); undo(); ThmCut "dst"; (* 57 *) su 2 "a1"; (* 58 *) su 3 "0"; (* 59 *) su 4 "0"; (* 60 *) ThmCut "aid"; (* 61 *) su 4 "0"; (* 62 *) rwl [1]; pl 1; ThmCut "aid"; (* 65 *) su 4 "a1*0"; (* 66 *) rwl [1]; ThmCut "acom"; (* 68 *) undo(); undo(); ThmCut "symm"; (* 71 *) su 4 "a1*0 + 0"; (* 72 *) su 5 "a1*0"; (* 73 *) l(); Done(); (* 75 *) gl2 3; rwl [1]; ThmCut "acom"; (* 78 *) su 5 "a1*0"; (* 79 *) su 6 "0"; (* 80 *) gl2 3; rwl [1]; ThmCut "thm_3_1_i"; (* 83 *) (* 82 No such theorem as thm_3_1_i*) (* Sequent snapshot: 1: a1 * 0 + 0 = 0 + a1 * 0 2: 0 + a1 * 0 = a1 * 0 + a1 * 0 3: a1 * 0 + 0 = a1 * 0 4: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 *) su 8 "a1*0"; (* 84 *) su 7 "a1*0"; (* 85 *) gl 2; gr 1; Done(); (* 88 *) (* 87 Not done!*) (* Sequent snapshot: 1: 0 + a1 * 0 = a1 * 0 + a1 * 0 2: a1 * 0 + 0 = a1 * 0 3: a1 * 0 = a1 * 0 + 0 4: a1 * 0 + 0 = 0 + a1 * 0 |- 1: a1 * 0 = 0 *) ThmCut "symm"; (* 89 *) su 7 "0"; (* 90 *) su 8 "a1*0"; (* 91 *) l(); Done(); (* 93 *) (* 92 Not done!*) (* Sequent snapshot: 1: 0 + a1 * 0 = a1 * 0 + a1 * 0 2: a1 * 0 + 0 = a1 * 0 3: a1 * 0 = a1 * 0 + 0 4: a1 * 0 + 0 = 0 + a1 * 0 |- 1: U6 = 0 2: a1 * 0 = 0 *) undo(); undo(); undo(); undo(); undo(); undo(); ThmCut "thm 3_1_i"; (* 100 *) su 6 "0"; (* 101 *) su 8 "a1*0"; (* 102 *) su 7 "a1*0"; (* 103 *) Done(); (* 104 *) ThmCut "symm"; (* 105 *) su 7 "0"; (* 106 *) su 8 "a1*0"; (* 107 *) l(); Done(); (* 109 *) Done(); (* 110 *) NameSequent 1 "thm 3_1_ii"; (* 111 *) (* 110 thm 3_1_ii: |- 1: a1 * 0 = 0 *) (* 110 reflx: |- 1: a1 = a1 *) (* 110 symm: |- 1: a1 = a2 -> a2 = a1 *) (* 110 trans: |- 1: a1 = a2 & a2 = a3 -> a1 = a3 *) (* 110 rplus: |- 1: Real(a1 + a2) *) (* 110 rtimes: |- 1: Real(a1 * a2) *) (* 110 rminus: |- 1: Real(-(a1)) *) (* 110 rinv: |- 1: Real(/(a1)) *) (* 110 acom: |- 1: a1 + a2 = a2 + a1 *) (* 110 aas: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 *) (* 110 aeq: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 *) (* 110 aid: |- 1: a1 + 0 = a1 *) (* 110 ainv: |- 1: a1 + -(a1) = 0 *) (* 110 mas: |- 1: [a1 * a2] * a3 = a1 * a2 * a3 *) (* 110 mcom: |- 1: a1 * a2 = a2 * a1 *) (* 110 meq: |- 1: a1 = a2 -> a1 * a3 = a2 * a3 *) (* 110 mid: |- 1: a1 * 1 = a1 *) (* 110 minv: |- 1: ~a1 eq 0 -> a1 * /(a1) = 1 *) (* 110 dst: |- 1: a1 * [a2 + a3] = a1 * a2 + a1 * a3 *) (* 111 *) StartSequent [] ["-(a1) * a2 = -(a1*a2)"]; (* 112 *) ThmCut "ainv"; (* 113 *) su 3 "a1"; (* 114 *) ThmCut "meq"; (* 115 *) su 3 "a1 + -(a1)"; (* 116 *) su 4 "0"; (* 117 *) su 5 "a2"; (* 118 *) l(); Done(); (* 120 *) ThmCut "acomm"; (* 121 *) (* 120 No such theorem as acomm*) (* Sequent snapshot: 1: [a1 + -(a1)] * a2 = 0 * a2 2: a1 + -(a1) = 0 |- 1: -(a1) * a2 = -(a1 * a2) *) ThmCut "acomm"; (* 122 *) (* 121 No such theorem as acomm*) (* Sequent snapshot: 1: [a1 + -(a1)] * a2 = 0 * a2 2: a1 + -(a1) = 0 |- 1: -(a1) * a2 = -(a1 * a2) *) ThmCut "mcom"; (* 123 *) ThmCut "mcom"; (* 124 *) su 5 "[a1 + -(a1)]"; (* 125 *) su 6 "a2"; (* 126 *) gl 2; rwl []; pl 1; su 7 "0"; (* 130 *) su 8 "a2"; (* 131 *) gl 3; rwl []; ThmCut "dst"; (* 134 *) su 8 "a2"; (* 135 *) su 9 "a1"; (* 136 *) su 10 "-(a1)"; (* 137 *) gl2 3; rwl []; pl 1; pl 3; pl 2; ThmCut "thm 3_1_ii"; (* 143 *) su 10 "a2"; (* 144 *) rwl []; pl 1; ThmCut "acom"; (* 147 *) su 10 "a2*a1"; (* 148 *) su 11 "a2* -(a1)"; (* 149 *) rwl []; pl 1; ThmCut "aeq"; (* 152 *) su 11 "a2 * -(a1) + a2*a1"; (* 153 *) su 12 "0"; (* 154 *) su 13 "-(a1 * a2)"; (* 155 *) l(); Done(); (* 157 *) pl 2; ThmCut "aas"; (* 159 *) su 13 "a2* -(a1)"; (* 160 *) su 15 "a2*a1"; (* 161 *) su 14 "-(a1*a2)"; (* 162 *) rwl []; pl 1; ThmCut "aas"; (* 165 *) undo(); undo(); ThmCut "acom"; (* 168 *) su 14 "0"; (* 169 *) su 15 "-(a1*a2)"; (* 170 *) rwl []; pl 1; ThmCut "aid"; (* 173 *) rwl []; pl 1; ThmCut "mcom"; (* 176 *) su 15 "a2"; (* 177 *) su 16 "a1"; (* 178 *) rwl []; pl 1; ThmCut "ainv"; (* 181 *) su 16 "a1*a2"; (* 182 *) rwl []; pl 1; ThmCut "aid"; (* 185 *) rwl []; pl 1; ThmCut "mcom"; (* 188 *) rwl [1]; gl 2; gr 1; Done(); (* 192 *) NameSequent 1 "thm 3_1_iii"; (* 193 *) (* 192 thm 3_1_iii: |- 1: -(a1) * a2 = -(a1 * a2) *)