setprecrightabove "*" "+"; (* 2 *) Axiom "rplus" [] ["Real(a1+a2)"]; (* 3 *) (* 2 rplus: |- 1: Real(a1 + a2) *) (* 3 *) Axiom "rtimes" [] ["Real(a1*a2)"]; (* 4 *) (* 3 rtimes: |- 1: Real(a1 * a2) *) (* 4 *) Axiom "rminus" [] ["Real(-(a1))"]; (* 5 *) (* 4 rminus: |- 1: Real(-(a1)) *) (* 5 *) Axiom "rinv" [] ["Real( /(a1))"]; (* 6 *) (* 5 rinv: |- 1: Real(/(a1)) *) (* 6 *) Axiom "acom" [] ["a1+a2=a2+a1"]; (* 7 *) (* 6 acom: |- 1: a1 + a2 = a2 + a1 *) (* 7 *) Axiom "aas" [] ["[a1+a2]+a3=a1+a2+a3"]; (* 8 *) (* 7 aas: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 *) (* 8 *) Axiom "aeq" [] ["(a1=a2)->(a1+a3=a2+a3)"]; (* 9 *) (* 8 aeq: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 *) (* 9 *) Axiom "aid" [] ["a1+0=a1"]; (* 10 *) (* 9 aid: |- 1: a1 + 0 = a1 *) (* 10 *) Axiom "ainv" [] ["a1+ -(a1)=0"]; (* 11 *) (* 10 ainv: |- 1: a1 + -(a1) = 0 *) (* 11 *) Definefunction 2 "--" "x1--x2" "x1+ -(x2)"; (* 12 *) (* 12 *) Definepredicate 2 "eq" "x1 eq x2" "x1+0=x2+0"; (* 13 *) (* 13 *) Axiom "mas" [] ["[a1*a2]*a3=a1*a2*a3"]; (* 14 *) (* 13 mas: |- 1: [a1 * a2] * a3 = a1 * a2 * a3 *) (* 14 *) Axiom "mcom" [] ["a1*a2=a2*a1"]; (* 15 *) (* 14 mcom: |- 1: a1 * a2 = a2 * a1 *) (* 15 *) Axiom "meq" [] ["(a1=a2)->(a1*a3=a2*a3)"]; (* 16 *) (* 15 meq: |- 1: a1 = a2 -> a1 * a3 = a2 * a3 *) (* 16 *) Axiom "mid" [] ["a1*1=a1"]; (* 17 *) (* 16 mid: |- 1: a1 * 1 = a1 *) (* 17 *) Axiom "minv" [] ["~(a1 eq 0)-> (a1* /(a1) = 1)"]; (* 18 *) (* 17 minv: |- 1: ~a1 eq 0 -> a1 * /(a1) = 1 *) (* 18 *) Axiom "dst" [] ["a1*[a2+a3]=a1*a2+a1*a3"]; (* 19 *) (* 18 dst: |- 1: a1 * [a2 + a3] = a1 * a2 + a1 * a3 *) (* 19 *) StartSequent ["a1+a3=a2+a3"] ["a1=a2"]; (* 20 *) ThmCut "aeq"; (* 21 *) su 4 "a1+a3"; (* 22 *) su 5 "a2+a3"; (* 23 *) su 6 "-(a3)"; (* 24 *) l(); Done(); (* 26 *) ThmCut "aas"; (* 27 *) rwl []; ThmCut "aas"; (* 29 *) gl2 3; rwl []; pl 1; pl 3; ThmCut "ainv"; (* 34 *) rwl []; pl 1; ThmCut "aid"; (* 37 *) ThmCut "aid"; (* 38 *) gl2 3; rwl []; gl 4; gl2 3; rwl []; gl 2; gr 1; Done(); (* 46 *) (* 45 -------------------- Proved ---------------------- Line 1: 1: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 3, 2*) (* 45 -------------------- Proved ---------------------- Line 3: 1: a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3) 2: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 5, 4*) (* 45 -------------------- Proved ---------------------- Line 5: 1: [a1 + a3] + -(a3) = [a2 + a3] + -(a3) 2: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 7, 6*) (* 45 -------------------- Proved ---------------------- Line 7: 1: [a1 + a3] + -(a3) = a1 + a3 + -(a3) 2: [a1 + a3] + -(a3) = [a2 + a3] + -(a3) 3: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 8*) (* 45 -------------------- Proved ---------------------- Line 8: 1: [a1 + a3] + -(a3) = a1 + a3 + -(a3) 2: a1 + a3 + -(a3) = [a2 + a3] + -(a3) 3: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 10, 9*) (* 45 -------------------- Proved ---------------------- Line 10: 1: [a2 + a3] + -(a3) = a2 + a3 + -(a3) 2: a1 + a3 + -(a3) = [a2 + a3] + -(a3) 3: a1 + a3 = a2 + a3 4: [a1 + a3] + -(a3) = a1 + a3 + -(a3) |- 1: a1 = a2 By 11*) (* 45 -------------------- Proved ---------------------- Line 11: 1: a1 + a3 + -(a3) = a2 + a3 + -(a3) 2: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 13, 12*) (* 45 -------------------- Proved ---------------------- Line 13: 1: a3 + -(a3) = 0 2: a1 + a3 + -(a3) = a2 + a3 + -(a3) 3: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 14*) (* 45 -------------------- Proved ---------------------- Line 14: 1: a1 + 0 = a2 + 0 2: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 16, 15*) (* 45 -------------------- Proved ---------------------- Line 16: 1: a2 + 0 = a2 2: a1 + 0 = a2 + 0 3: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 18, 17*) (* 45 -------------------- Proved ---------------------- Line 18: 1: a1 + 0 = a1 2: a1 + 0 = a2 + 0 3: a1 + a3 = a2 + a3 4: a2 + 0 = a2 |- 1: a1 = a2 By 19*) (* 45 -------------------- Proved ---------------------- Line 19: 1: a2 + 0 = a2 2: a1 = a2 + 0 3: a1 + a3 = a2 + a3 4: a1 + 0 = a1 |- 1: a1 = a2 By 20*) (* 45 -------------------- Trivial --------------------- Line 20: 1: a1 = a2 2: a1 + a3 = a2 + a3 3: a1 + 0 = a1 4: a2 + 0 = a2 |- 1: a1 = a2 *) (* 45 -------------------- Proved ---------------------- Line 17: |- 1: a1 + 0 = a1 By aid*) (* 45 Proof of aid begins *) (* 45 -------------------- Proved ---------------------- Line 8.1: |- 1: a1 + 0 = a1 By aid.*) (* 45 is an axiom*) (* 45 Proof of aid ends*) (* 45 -------------------- Proved ---------------------- Line 15: |- 1: a2 + 0 = a2 By aid*) (* 45 Already shown(8)*) (* 45 -------------------- Proved ---------------------- Line 12: |- 1: a3 + -(a3) = 0 By ainv*) (* 45 Proof of ainv begins *) (* 45 -------------------- Proved ---------------------- Line 9.1: |- 1: a1 + -(a1) = 0 By ainv.*) (* 45 is an axiom*) (* 45 Proof of ainv ends*) (* 45 -------------------- Proved ---------------------- Line 9: |- 1: [a2 + a3] + -(a3) = a2 + a3 + -(a3) By aas*) (* 45 Proof of aas begins *) (* 45 -------------------- Proved ---------------------- Line 6.1: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 By aas.*) (* 45 is an axiom*) (* 45 Proof of aas ends*) (* 45 -------------------- Proved ---------------------- Line 6: |- 1: [a1 + a3] + -(a3) = a1 + a3 + -(a3) By aas*) (* 45 Already shown(6)*) (* 45 -------------------- Trivial --------------------- Line 4: 1: a1 + a3 = a2 + a3 |- 1: a1 + a3 = a2 + a3 2: a1 = a2 *) (* 45 -------------------- Proved ---------------------- Line 2: |- 1: a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3) By aeq*) (* 45 Proof of aeq begins *) (* 45 -------------------- Proved ---------------------- Line 7.1: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 By aeq.*) (* 45 is an axiom*) (* 45 Proof of aeq ends*) NameSequent 1 "Thm_3_1_i"; (* 47 *) (* 46 Thm_3_1_i: 1: a1 + a3 = a2 + a3 |- 1: a1 = a2 *) (* 46 rplus: |- 1: Real(a1 + a2) *) (* 46 rtimes: |- 1: Real(a1 * a2) *) (* 46 rminus: |- 1: Real(-(a1)) *) (* 46 rinv: |- 1: Real(/(a1)) *) (* 46 acom: |- 1: a1 + a2 = a2 + a1 *) (* 46 aas: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 *) (* 46 aeq: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 *) (* 46 aid: |- 1: a1 + 0 = a1 *) (* 46 ainv: |- 1: a1 + -(a1) = 0 *) (* 46 mas: |- 1: [a1 * a2] * a3 = a1 * a2 * a3 *) (* 46 mcom: |- 1: a1 * a2 = a2 * a1 *) (* 46 meq: |- 1: a1 = a2 -> a1 * a3 = a2 * a3 *) (* 46 mid: |- 1: a1 * 1 = a1 *) (* 46 minv: |- 1: ~a1 eq 0 -> a1 * /(a1) = 1 *) (* 46 dst: |- 1: a1 * [a2 + a3] = a1 * a2 + a1 * a3 *) (* 46 Thm_3_1_i: 1: a1 + a3 = a2 + a3 |- 1: a1 = a2 *) (* 47 *) StartSequent [] ["a*0 = 0"]; (* 48 *) (* 47 Parse error prevents starting sequent*) (* 48 *) StartSequent [""] ["a1*0 = 0"]; (* 49 *) (* 48 Parse error prevents starting sequent*) (* 49 *) StartSequent [] ["a1*0 = 0"]; (* 50 *) ThmCut "aid"; (* 51 *) su 2 "a1"; (* 52 *) undo(); undo(); undo(); ThmCut "dst"; (* 56 *) su 2 "a1"; (* 57 *) su 3 "0"; (* 58 *) su 4 "0"; (* 59 *) ThmCut "aid"; (* 60 *) su 4 "0"; (* 61 *) rwl [1]; pl 1; ThmCut "aid"; (* 64 *) su 4 "a1*0"; (* 65 *) rwl [1]; ThmCut "acom"; (* 67 *) undo(); undo(); (* 69 *) Axiom "reflx" [] ["a1=a1"]; (* 70 *) (* 69 reflx: |- 1: a1 = a1 *) (* Sequent snapshot: 1: a1 * 0 + 0 = a1 * 0 2: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 *) (* 70 *) Axiom "symm" [] ["(a1=a2)->(a2=a1)"]; (* 71 *) (* 70 symm: |- 1: a1 = a2 -> a2 = a1 *) (* Sequent snapshot: 1: a1 * 0 + 0 = a1 * 0 2: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 *) ThmCut "symm"; (* 72 *) su 4 "a1*0 + 0"; (* 73 *) su 5 "a1*0"; (* 74 *) l(); Done(); (* 76 *) gl2 3; rwl [1]; ThmCut "acom"; (* 79 *) su 5 "a1*0"; (* 80 *) su 6 "0"; (* 81 *) gl2 3; rwl [1]; ThmCut "Thm_3_1_i"; (* 84 *) su 6 "0"; (* 85 *) su 8 "a1*0"; (* 86 *) su 7 "a1*0"; (* 87 *) gl 2; gr 1; Done(); (* 90 *) Done(); (* 91 *) (* 90 Not done!*) (* Sequent snapshot: 1: 0 = a1 * 0 2: a1 * 0 + 0 = 0 + a1 * 0 3: 0 + a1 * 0 = a1 * 0 + a1 * 0 4: a1 * 0 + 0 = a1 * 0 5: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 *) ThmCut "symm"; (* 92 *) su 7 "0"; (* 93 *) su 8 "a1*0"; (* 94 *) l(); Done(); (* 96 *) Done(); (* 97 *) (* 96 -------------------- Proved ---------------------- Line 1: |- 1: a1 * 0 = 0 By 3, 2*) (* 96 -------------------- Proved ---------------------- Line 3: 1: a1 * [0 + 0] = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 By 5, 4*) (* 96 -------------------- Proved ---------------------- Line 5: 1: 0 + 0 = 0 2: a1 * [0 + 0] = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 By 6*) (* 96 -------------------- Proved ---------------------- Line 6: 1: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 By 8, 7*) (* 96 -------------------- Proved ---------------------- Line 8: 1: a1 * 0 + 0 = a1 * 0 2: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 By 11, 10*) (* 96 -------------------- Proved ---------------------- Line 11: 1: a1 * 0 + 0 = a1 * 0 -> a1 * 0 = a1 * 0 + 0 2: a1 * 0 + 0 = a1 * 0 3: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 = 0 By 13, 12*) (* 96 -------------------- Proved ---------------------- Line 13: 1: a1 * 0 = a1 * 0 + 0 2: a1 * 0 = a1 * 0 + a1 * 0 3: a1 * 0 + 0 = a1 * 0 |- 1: a1 * 0 = 0 By 14*) (* 96 -------------------- Proved ---------------------- Line 14: 1: a1 * 0 = a1 * 0 + 0 2: a1 * 0 + 0 = a1 * 0 + a1 * 0 3: a1 * 0 + 0 = a1 * 0 |- 1: a1 * 0 = 0 By 16, 15*) (* 96 -------------------- Proved ---------------------- Line 16: 1: a1 * 0 + 0 = 0 + a1 * 0 2: a1 * 0 + 0 = a1 * 0 + a1 * 0 3: a1 * 0 + 0 = a1 * 0 4: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 By 17*) (* 96 -------------------- Proved ---------------------- Line 17: 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 By 20, 18, 19*) (* 96 -------------------- Proved ---------------------- Line 20: 1: 0 = a1 * 0 2: a1 * 0 + 0 = 0 + a1 * 0 3: 0 + a1 * 0 = a1 * 0 + a1 * 0 4: a1 * 0 + 0 = a1 * 0 5: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 By 22, 21*) (* 96 -------------------- Proved ---------------------- Line 22: 1: 0 = a1 * 0 -> a1 * 0 = 0 2: 0 = a1 * 0 3: a1 * 0 + 0 = 0 + a1 * 0 4: 0 + a1 * 0 = a1 * 0 + a1 * 0 5: a1 * 0 + 0 = a1 * 0 6: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 By 24, 23*) (* 96 -------------------- Trivial --------------------- Line 24: 1: a1 * 0 = 0 2: 0 = a1 * 0 3: a1 * 0 + 0 = 0 + a1 * 0 4: 0 + a1 * 0 = a1 * 0 + a1 * 0 5: a1 * 0 + 0 = a1 * 0 6: a1 * 0 = a1 * 0 + 0 |- 1: a1 * 0 = 0 *) (* 96 -------------------- Trivial --------------------- Line 23: 1: 0 = a1 * 0 2: a1 * 0 + 0 = 0 + a1 * 0 3: 0 + a1 * 0 = a1 * 0 + a1 * 0 4: a1 * 0 + 0 = a1 * 0 5: a1 * 0 = a1 * 0 + 0 |- 1: 0 = a1 * 0 2: a1 * 0 = 0 *) (* 96 -------------------- Proved ---------------------- Line 21: |- 1: 0 = a1 * 0 -> a1 * 0 = 0 By symm*) (* 96 Proof of symm begins *) (* 96 -------------------- Proved ---------------------- Line 18.1: |- 1: a1 = a2 -> a2 = a1 By symm.*) (* 96 is an axiom*) (* 96 Proof of symm ends*) (* 96 -------------------- Proved ---------------------- Line 18: 1: 0 + a1 * 0 = a1 * 0 + a1 * 0 |- 1: 0 = a1 * 0 By Thm_3_1_i*) (* 96 Proof of Thm_3_1_i begins *) (* 96 -------------------- Proved ---------------------- Line 16.1: 1: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 2, 3*) (* 96 -------------------- Proved ---------------------- Line 16.2: |- 1: a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3) By Thm_3_1_i.aeq*) (* 96 Proof of Thm_3_1_i.aeq begins *) (* 96 -------------------- Proved ---------------------- Line 7.1: |- 1: a1 = a2 -> a1 + a3 = a2 + a3 By Thm_3_1_i.aeq.*) (* 96 is an axiom*) (* 96 Proof of Thm_3_1_i.aeq ends*) (* 96 -------------------- Proved ---------------------- Line 16.3: 1: a1 + a3 = a2 + a3 -> [a1 + a3] + -(a3) = [a2 + a3] + -(a3) 2: a1 + a3 = a2 + a3 |- 1: a1 = a2 By 4, 5*) (* 96 -------------------- Trivial --------------------- Line 16.4: 1: a1 + a3 = a2 + a3 |- 1: a1 + a3 = a2 + a3 *) (* 96 -------------------- Proved ---------------------- Line 16.5: 1: [a1 + a3] + -(a3) = [a2 + a3] + -(a3) |- 1: a1 = a2 By 6, 7*) (* 96 -------------------- Proved ---------------------- Line 16.6: |- 1: [a1 + a3] + -(a3) = a1 + a3 + -(a3) By Thm_3_1_i.aas*) (* 96 Proof of Thm_3_1_i.aas begins *) (* 96 -------------------- Proved ---------------------- Line 6.1: |- 1: [a1 + a2] + a3 = a1 + a2 + a3 By Thm_3_1_i.aas.*) (* 96 is an axiom*) (* 96 Proof of Thm_3_1_i.aas ends*) (* 96 -------------------- Proved ---------------------- Line 16.7: 1: [a1 + a3] + -(a3) = a1 + a3 + -(a3) 2: [a1 + a3] + -(a3) = [a2 + a3] + -(a3) |- 1: a1 = a2 By 8*) (* 96 -------------------- Proved ---------------------- Line 16.8: 1: a1 + a3 + -(a3) = [a2 + a3] + -(a3) |- 1: a1 = a2 By 9, 10*) (* 96 -------------------- Proved ---------------------- Line 16.9: |- 1: [a2 + a3] + -(a3) = a2 + a3 + -(a3) By Thm_3_1_i.aas*) (* 96 Already shown(6)*) (* 96 -------------------- Proved ---------------------- Line 16.10: 1: [a2 + a3] + -(a3) = a2 + a3 + -(a3) 2: a1 + a3 + -(a3) = [a2 + a3] + -(a3) |- 1: a1 = a2 By 11*) (* 96 -------------------- Proved ---------------------- Line 16.11: 1: a1 + a3 + -(a3) = a2 + a3 + -(a3) |- 1: a1 = a2 By 12, 13*) (* 96 -------------------- Proved ---------------------- Line 16.12: |- 1: a3 + -(a3) = 0 By Thm_3_1_i.ainv*) (* 96 Proof of Thm_3_1_i.ainv begins *) (* 96 -------------------- Proved ---------------------- Line 9.1: |- 1: a1 + -(a1) = 0 By Thm_3_1_i.ainv.*) (* 96 is an axiom*) (* 96 Proof of Thm_3_1_i.ainv ends*) (* 96 -------------------- Proved ---------------------- Line 16.13: 1: a3 + -(a3) = 0 2: a1 + a3 + -(a3) = a2 + a3 + -(a3) |- 1: a1 = a2 By 14*) (* 96 -------------------- Proved ---------------------- Line 16.14: 1: a1 + 0 = a2 + 0 |- 1: a1 = a2 By 15, 16*) (* 96 -------------------- Proved ---------------------- Line 16.15: |- 1: a2 + 0 = a2 By Thm_3_1_i.aid*) (* 96 Proof of Thm_3_1_i.aid begins *) (* 96 -------------------- Proved ---------------------- Line 8.1: |- 1: a1 + 0 = a1 By Thm_3_1_i.aid.*) (* 96 is an axiom*) (* 96 Proof of Thm_3_1_i.aid ends*) (* 96 -------------------- Proved ---------------------- Line 16.16: 1: a2 + 0 = a2 2: a1 + 0 = a2 + 0 |- 1: a1 = a2 By 17, 18*) (* 96 -------------------- Proved ---------------------- Line 16.17: |- 1: a1 + 0 = a1 By Thm_3_1_i.aid*) (* 96 Already shown(8)*) (* 96 -------------------- Proved ---------------------- Line 16.18: 1: a1 + 0 = a1 2: a1 + 0 = a2 + 0 3: a2 + 0 = a2 |- 1: a1 = a2 By 19*) (* 96 -------------------- Proved ---------------------- Line 16.19: 1: a2 + 0 = a2 2: a1 = a2 + 0 |- 1: a1 = a2 By 20*) (* 96 -------------------- Trivial --------------------- Line 16.20: 1: a1 = a2 |- 1: a1 = a2 *) (* 96 Proof of Thm_3_1_i ends*) (* 96 -------------------- Trivial --------------------- Line 19: 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: 0 + a1 * 0 = a1 * 0 + a1 * 0 2: a1 * 0 = 0 *) (* 96 -------------------- Proved ---------------------- Line 15: |- 1: a1 * 0 + 0 = 0 + a1 * 0 By acom*) (* 96 Proof of acom begins *) (* 96 -------------------- Proved ---------------------- Line 5.1: |- 1: a1 + a2 = a2 + a1 By acom.*) (* 96 is an axiom*) (* 96 Proof of acom ends*) (* 96 -------------------- Trivial --------------------- Line 12: 1: a1 * 0 + 0 = a1 * 0 2: a1 * 0 = a1 * 0 + a1 * 0 |- 1: a1 * 0 + 0 = a1 * 0 2: a1 * 0 = 0 *) (* 96 -------------------- Proved ---------------------- Line 10: |- 1: a1 * 0 + 0 = a1 * 0 -> a1 * 0 = a1 * 0 + 0 By symm*) (* 96 Already shown(18)*) (* 96 -------------------- Proved ---------------------- Line 7: |- 1: a1 * 0 + 0 = a1 * 0 By aid*) (* 96 Already shown(8)*) (* 96 -------------------- Proved ---------------------- Line 4: |- 1: 0 + 0 = 0 By aid*) (* 96 Already shown(8)*) (* 96 -------------------- Proved ---------------------- Line 2: |- 1: a1 * [0 + 0] = a1 * 0 + a1 * 0 By dst*) (* 96 Proof of dst begins *) (* 96 -------------------- Proved ---------------------- Line 15.1: |- 1: a1 * [a2 + a3] = a1 * a2 + a1 * a3 By dst.*) (* 96 is an axiom*) (* 96 Proof of dst ends*) NameSequent 1 "thm 3_1_ii"; (* 98 *) (* 97 thm 3_1_ii: |- 1: a1 * 0 = 0 *) (* 98 *) StartSequent [] ["-(a1) * a2 = -(a1*a2)"]; (* 99 *) (* 99 *) Axiom "trans" [] ["(a1=a2 ^ a2=a3)-> (a1=a3)"]; (* 100 *) (* 99 Parse error prevents starting sequent*) (* Sequent snapshot: |- 1: -(a1) * a2 = -(a1 * a2) *) (* 100 *) Axiom "trans" [] ["((a1=a2) ^ (a2=a3)) -> (a1=a3)"]; (* 101 *) (* 100 Parse error prevents starting sequent*) (* Sequent snapshot: |- 1: -(a1) * a2 = -(a1 * a2) *) (* 101 *) Axiom "Trans" [] ["((a1 = a2) ^ (a2 = a3)) -> (a1 = a3)"]; (* 102 *) (* 101 Parse error prevents starting sequent*) (* Sequent snapshot: |- 1: -(a1) * a2 = -(a1 * a2) *) (* 102 *) Axiom "trans" [] ["a1=a2 ^ a2=a3 -> a1=a3"]; (* 103 *) (* 102 trans: |- 1: a1 = a2 *) (* Sequent snapshot: |- 1: -(a1) * a2 = -(a1 * a2) *) undo(); undo(); undo(); undo(); undo();