(* 0

reflx:



|-

1:  a1 = a1

*)



(* 0

symm:



|-

1:  a1 = a2 -> a2 = a1

*)



(* 0

trans:



|-

1:  a1 = a2 & a2 = a3 -> a1 = a3

*)



(* 0

rplus:



|-

1:  Real(a1 + a2)

*)



(* 0

rtimes:



|-

1:  Real(a1 * a2)

*)



(* 0

rminus:



|-

1:  Real(-(a1))

*)



(* 0

rinv:



|-

1:  Real(/(a1))

*)



(* 0

acom:



|-

1:  a1 + a2 = a2 + a1

*)



(* 0

aas:



|-

1:  [a1 + a2] + a3 = a1 + a2 + a3

*)



(* 0

aeq:



|-

1:  a1 = a2 -> a1 + a3 = a2 + a3

*)



(* 0

aid:



|-

1:  a1 + 0 = a1

*)



(* 0

ainv:



|-

1:  a1 + -(a1) = 0

*)



(* 0

mas:



|-

1:  [a1 * a2] * a3 = a1 * a2 * a3

*)



(* 0

mcom:



|-

1:  a1 * a2 = a2 * a1

*)



(* 0

meq:



|-

1:  a1 = a2 -> a1 * a3 = a2 * a3

*)



(* 0

mid:



|-

1:  a1 * 1 = a1

*)



(* 0

minv:



|-

1:  ~a1 eq 0 -> a1 * /(a1) = 1

*)



(* 0

dst:



|-

1:  a1 * [a2 + a3] = a1 * a2
      + a1 * a3

*)



(* 0

thm 3_1_i:



1:  a1 + a3 = a2 + a3

|-

1:  a1 = a2

*)



(* 0

thm 3_1_ii:



|-

1:  a1 * 0 = 0

*)



(* 0

thm 3_1_iii:



|-

1:  -(a1) * a2 = -(a1 * a2)

*)



(* 1 *)  StartSequent [] ["-(a1)* -(a2)= a1*a2"]; 
(* 2 *)  ThmCut "ainv"; 
(* 3 *)  su 3 "a2"; 
(* 4 *)  ThmCut "dst"; 
(* 5 *)  undo(); undo(); ThmCut "meq"; 
(* 8 *)  su 3 "a2 + -(a2)"; 
(* 9 *)  su 4 "0"; 
(* 10 *)  su 5 "-(a1)"; 
(* 11 *)  l(); Done(); 
(* 13 *)  pl 2; ThmCut "mcom"; 
(* 15 *)  rwl []; ThmCut "mcom"; 
(* 17 *)  pl 2; gl 2; rwl [2]; pl 1; ThmCut "dst"; 
(* 22 *)  su 5 "-(a1)"; 
(* 23 *)  su 6 "a2"; 
(* 24 *)  su 7 "-(a2)"; 
(* 25 *)  rwl []; pl 1; ThmCut "mid"; 
(* 28 *)  undo(); undo(); ThmCut "thm 3_1_ii"; 
(* 31 *)  rwl []; pl 1; ThmCut "acom"; 
(* 34 *)  rwl []; pl 1; ThmCut "aeq"; 
(* 37 *)  su 7 "-(a1)* -(a2) + -(a1)*a2"; 
(* 38 *)  su 8 "0"; 
(* 39 *)  su 9 "a1*a2"; 
(* 40 *)  l(); Done(); 
(* 42 *)  pl 2; ThmCut "thm 3_1_iii"; 
(* 44 *)  su 9 "-(a1)"; 
(* 45 *)  su 10 "a2"; 
(* 46 *)  undo(); undo(); su 9 "a1"; 
(* 49 *)  su 10 "a2"; 
(* 50 *)  rwl []; pl 1; ThmCut "aas"; 
(* 53 *)  rwl []; pl 1; ThmCut "acom"; 
(* 56 *)  su 10 "0"; 
(* 57 *)  su 11 "a1*a2"; 
(* 58 *)  rwl []; pl 1; ThmCut "aid"; 
(* 61 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 64 *)  rwl []; su 11 "a1*a2"; 
(* 66 *)  ThmCut "acom"; 
(* 67 *)  su 11 "-(a1*a2)"; 
(* 68 *)  su 12 "a1*a2"; 
(* 69 *)  gl2 3; rwl []; pl 1; gl 2; rwl []; pl 1; ThmCut "aid"; 
(* 76 *)  rwl []; gl 2; gr 1; Done(); 
(* 80 *)  NameSequent 1 "thm 3_1_iv"; 
(* 81 *)  

(* 80

thm 3_1_iv:



|-

1:  -(a1) * -(a2) = a1 * a2

*)



(* 81 *)  Axiom "aeql" [] ["(a1=a2)->(a3+a1=a3+a2)"]; 
(* 82 *)  

(* 81

aeql:



|-

1:  a1 = a2 -> a3 + a1 = a3 + a2

*)



(* 82 *)  Axiom "meql" [] ["(a1=a2)->(a3*a1=a3*a2)"]; 
(* 83 *)  

(* 82

meql:



|-

1:  a1 = a2 -> a3 * a1 = a3 * a2

*)



(* 83 *)  Axiom "dstr" [] ["[a1+a2]*a3=a1*a3+a2*a3"]; 
(* 84 *)  

(* 83

dstr:



|-

1:  [a1 + a2] * a3 = a1 * a3 + a2 * a3

*)



(* 84 *)  StartSequent ["a1*a3=a2*a3 & ~(a3 eq 0)"] ["a1=a2"]; 
(* 85 *)  l(); ThmCut "meq"; 
(* 87 *)  su 4 "a1*a3"; 
(* 88 *)  su 5 "a2*a3"; 
(* 89 *)  su 6 "/(a3)"; 
(* 90 *)  l(); Done(); 
(* 92 *)  pl 2; ThmCut "mas"; 
(* 94 *)  gl2 3; rwl []; pl 1; ThmCut "mas"; 
(* 98 *)  rwl []; pl 1; ThmCut "minv"; 
(* 101 *)  ThmCut "minv"; 
(* 102 *)  gl2 3; su 7 "a3"; 
(* 104 *)  rwl []; 

(* 104

No left rewrite rule applies.*)


(* Sequent snapshot:


1:  ~a3 eq 0 -> a3 * /(a3) = 1

2:  a1 * a3 * /(a3) = a2 * a3 * /(a3)

3:  ~a3 eq 0

4:  ~U6 eq 0 -> U6 * /(U6) = 1

|-

1:  a1 = a2


*)

l(); gl 2; gr 1; Done(); 
(* 109 *)  rwl []; pl 1; pl 3; ThmCut "mid"; 
(* 113 *)  ThmCut "mid"; 
(* 114 *)  gl2 3; rwl []; pl 1; gl 3; rwl []; gl 2; gr 1; Done(); 
(* 122 *)  NameSequent 1 "thm 3_1_v"; 
(* 123 *)  

(* 122

thm 3_1_v:



1:  a1 * a3 = a2 * a3 & ~a3 eq 0

|-

1:  a1 = a2

*)



(* 123 *)  StartSequent ["a1*a2=0"] ["a1=0 v a2=0"]; 
(* 124 *)  r(); ThmCut "meq"; 
(* 126 *)  su 3 "a1*a2"; 
(* 127 *)  su 4 "0"; 
(* 128 *)  su 5 "/(a2)"; 
(* 129 *)  l(); Done(); 
(* 131 *)  pl 2; ThmCut "mas"; 
(* 133 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 136 *)  su 5 "0"; 
(* 137 *)  su 6 "/(a2)"; 
(* 138 *)  rwl []; pl 1; ThmCut "thm 3_1_ii"; 
(* 141 *)  rwl []; pl 1; Cut "~(a2 eq 0)"; 
(* 144 *)  r(); r(); undo(); l(); ThmCut "aid"; 
(* 149 *)  rwl []; pl 1; ThmCut "aid"; 
(* 152 *)  rwl []; pl 1; gl 1; gr 2; Done(); 
(* 157 *)  ThmCut "minv"; 
(* 158 *)  su 6 "a2"; 
(* 159 *)  l(); Done(); 
(* 161 *)  gl2 3; rwl []; pl 1; ThmCut "mid"; 
(* 165 *)  rwl []; gl 2; gr 1; Done(); 
(* 169 *)  NameSequent 1 "thm 3_1_vi"; 
(* 170 *)  

(* 169

thm 3_1_vi:



1:  a1 * a2 = 0

|-

1:  a1 = 0 v a2 = 0

*)



(* 170 *)  Axiom "rinequal" [] ["Real(a1 <= a2)"]; 
(* 171 *)  

(* 170

Parse error prevents starting sequent*)



(* 171 *)  Axiom "totrder" [] ["(a1 <= a2) v (a2 <= a1)"]; 
(* 172 *)  

(* 171

totrder:



|-

1:  a1 <= a2 v a2 <= a1

*)



(* 172 *)  Axiom "eqbyord" [] ["((a1 <= a2)&(a2 <= a1))->(a1=a2)"]; 
(* 173 *)  

(* 172

eqbyord:



|-

1:  a1 <= a2 & a2 <= a1 -> a1 = a2

*)



(* 173 *)  Axiom "ordtrans" [] ["((a1 <= a2)&(a2 <= a3))->(a1 <= a3)"]; 
(* 174 *)  

(* 173

ordtrans:



|-

1:  a1 <= a2 & a2 <= a3 -> a1 <= a3

*)



(* 174 *)  Axiom "ordeq" [] ["(a1 <= a2)->(a1+a3 <= a2+a3)"]; 
(* 175 *)  

(* 174

ordeq:



|-

1:  a1 <= a2 -> a1 + a3 <= a2 + a3

*)



(* 175 *)  Axiom "ordeql" [] ["(a1 <= a2)->(a3+a1 <= a3+a2)"]; 
(* 176 *)  

(* 175

ordeql:



|-

1:  a1 <= a2 -> a3 + a1 <= a3 + a2

*)



(* 176 *)  Axiom "ordmult" [] ["((a1 <= a2) & (0 <= a3))-> (a1*a3 <= a2*a3)"]; 
(* 177 *)  

(* 176

ordmult:



|-

1:  a1 <= a2 & 0 <= a3 -> a1 * a3 <= a2 * a3

*)



(* 177 *)  Axiom "strctord" [] ["(a1 < a2) == ((a1 <= a2)& ~(a1 = a2))"]; 
(* 178 *)  

(* 177

strctord:



|-

1:  a1 < a2 == a1 <= a2 & ~a1 = a2

*)



(* 178 *)  StartSequent ["a1 <= a2"] ["-a2 <= a1"]; 
(* 179 *)  

(* 178

Parse error prevents starting sequent*)



(* 179 *)  StartSequent ["a1 <= a2"] ["-(a2) <= a1"]; 
(* 180 *)