(* 0

zero:



|-

1:  Real(0)

*)



(* 0

one:



|-

1:  Real(1)

*)



(* 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

aid:



1:  Real(a1)

|-

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

mid:



1:  Real(a1)

|-

1:  a1 * 1 = a1

*)



(* 0

minv:



|-

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

*)



(* 0

dist:



|-

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

*)



(* 0

totorder:



|-

1:  a1 <= a2 v a2 <= a1

*)



(* 0

eqbyord:



|-

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

*)



(* 0

ordtrans:



|-

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

*)



(* 0

ordadd:



|-

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

*)



(* 0

ordaddl:



|-

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

*)



(* 0

ordmult:



|-

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

*)



(* 0

reflx:



|-

1:  a1 = a1

*)



(* 0

symm:



|-

1:  a1 = a2 -> a2 = a1

*)



(* 0

trans:



|-

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

*)



(* 0

aeq:



|-

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

*)



(* 0

aeql:



|-

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

*)



(* 0

meq:



|-

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

*)



(* 0

meql:



|-

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

*)



(* 0

distr:



|-

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

*)



(* 0

thm 3.1.i:



1:  Real(a1)

2:  Real(a2)

|-

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

*)



(* 0

thm 3.1.ii:



1:  Real(0)

|-

1:  a1 * 0 = 0

*)



(* 0

thm 3.1.iii:



|-

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

*)



(* 0

thm 3.1.iv:



|-

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

*)



(* 0

thm 3.1.v:



1:  Real(a1)

2:  Real(a2)

3:  a1 * a3 = a2 * a3

4:  ~a3 eq 0

|-

1:  a1 = a2

*)



(* 0

thm 3.1.vi:



1:  Real(a1)

2:  a1 * a2 = 0

3:  ~a2 eq 0

|-

1:  a1 = 0 v a2 = 0

*)



(* 0

thm 3.2.i:



1:  a1 <= a2

|-

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

*)



(* 0

zeros:



|-

1:  -(0) = 0

*)



(* 0

2neg:



1:  Real(a1)

|-

1:  -(-(a1)) = a1

*)



(* 0

thm 3.2.ii:



1:  a1 <= a2

2:  a3 <= 0

|-

1:  a2 * a3 <= a1 * a3

*)



(* 0

thm 3.2.iii:



1:  0 <= a1

2:  0 <= a2

|-

1:  0 <= a1 * a2

*)



(* 0

thm 3.2.iv:



|-

1:  0 <= a1 * a1

*)



(* 0

eqsymm:



1:  a1 eq a2

|-

1:  a2 eq a1

*)



(* 0

req:



1:  a1 eq a2

2:  Real(a1)

3:  Real(a2)

|-

1:  a1 = a2

*)



(* 0

negeqsymm:



1:  ~a1 eq a2

|-

1:  ~a2 eq a1

*)



(* 0

thm 3.2.v:



1:  Real(1)

2:  ~0 eq 1

|-

1:  0 < 1

*)



(* 1 *)  StartSequent ["Real(a1)","~(a1 eq 0)","~(1 eq 0)"] ["~(/(a1) eq 0)"]; 
(* 2 *)  ThmCut "minv"; 
(* 3 *)  su 2 "a1"; 
(* 4 *)  l(); gl 2; gr 1; Done(); 
(* 8 *)  r(); gl 4; l(); r(); gl 2; l(); ThmCut "aid"; 
(* 15 *)  ThmCut "rinv"; 
(* 16 *)  su 3 "a1"; 
(* 17 *)  su 2 "/(a1)"; 
(* 18 *)  Done(); 
(* 19 *)  rwl []; pl 1; ThmCut "aid"; 
(* 22 *)  ThmCut "zero"; 
(* 23 *)  su 2 "0"; 
(* 24 *)  Done(); 
(* 25 *)  rwl []; pl 1; ThmCut "meql"; 
(* 28 *)  su 2 "/(a1)"; 
(* 29 *)  su 4 "0"; 
(* 30 *)  l(); Done(); 
(* 32 *)  su 3 "a1"; 
(* 33 *)  gl 3; gl2 4; rwl []; ThmCut "thm 3.1.ii"; 
(* 37 *)  ThmCut "zero"; 
(* 38 *)  Done(); 
(* 39 *)  su 3 "a1"; 
(* 40 *)  pl 2; gl 5; rwl []; ThmCut "meql"; 
(* 44 *)  su 3 "1"; 
(* 45 *)  su 5 "0"; 
(* 46 *)  l(); gl 2; gr 1; Done(); 
(* 50 *)  su 4 "a1"; 
(* 51 *)  ThmCut "mid"; 
(* 52 *)  su 4 "a1"; 
(* 53 *)  gl 5; gr 1; Done(); 
(* 56 *)  rwl []; pl 1; gl 2; gl2 6; rwl []; ThmCut "aeq"; 
(* 62 *)  su 4 "a1"; 
(* 63 *)  su 5 "0"; 
(* 64 *)  su 6 "0"; 
(* 65 *)  l(); gl 2; gr 1; Done(); 
(* 69 *)  Done(); 
(* 70 *)  NameSequent 1 "lemma 1.1"; 
(* 71 *)  

(* 70

lemma 1.1:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  ~/(a1) eq 0

*)



(* 71 *)  StartSequent ["Real(a1)","~(a1 eq 0)"] ["/(/(a1))=a1"]; 
(* 72 *)  ThmCut "mas"; 
(* 73 *)  su 2 "a1"; 
(* 74 *)  su 4 "/(a1)"; 
(* 75 *)  su 3 "/(/(a1))"; 
(* 76 *)  ThmCut "minv"; 
(* 77 *)  su 3 "a1"; 
(* 78 *)  l(); gl 3; gr 1; Done(); 
(* 82 *)  rwl [1]; pl 1; ThmCut "mcom"; 
(* 85 *)  rwl []; pl 1; ThmCut "mid"; 
(* 88 *)  ThmCut "rinv"; 
(* 89 *)  su 4 "/(a1)"; 
(* 90 *)  su 3 "/(/(a1))"; 
(* 91 *)  Done(); 
(* 92 *)  rwl []; pl 1; ThmCut "lemma 1.1"; 
(* 95 *)  su 3 "a1"; 
(* 96 *)  gl 2; gr 1; Done(); 
(* 99 *)  gl 3; gr 1; Done(); 
(* 102 *)  ThmCut "minv"; 
(* 103 *)  su 3 "/(a1)"; 
(* 104 *)  l(); Done(); 
(* 106 *)  ThmCut "mcom"; 
(* 107 *)  su 3 "a1"; 
(* 108 *)  su 4 "/(a1) * /(/(a1))"; 
(* 109 *)  gl2 4; rwl []; pl 1; gl 4; gl2 3; rwl []; pl 1; ThmCut "mcom"; 
(* 117 *)  rwl []; pl 1; ThmCut "mid"; 
(* 120 *)  su 4 "a1"; 
(* 121 *)  gl 2; gr 1; Done(); 
(* 124 *)  rwl []; gl 2; gr 1; Done(); 
(* 128 *)  NameSequent 1 "lemma 1.2"; 
(* 129 *)  

(* 128

lemma 1.2:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  /(/(a1)) = a1

*)



(* 129 *)  StartSequent ["0 < a1","~(0 eq 1)","Real(a1)","Real(1)","Real(0)"] ["0 < /(a1)"]; 
(* 130 *)  l(); l(); r(); r(); gl 3; l(); undo(); ThmCut "thm 3.2.v"; 
(* 138 *)  gl 2; gr 1; Done(); 
(* 141 *)  

(* 140

Not done!*)


(* Sequent snapshot:


1:  Real(a1)

2:  Real(1)

3:  Real(0)

4:  0 <= a1

5:  ~0 eq a1

6:  ~0 eq 1

|-

1:  Real(1)

2:  0 <= /(a1)


*)

gl 2; gr 1; Done(); 
(* 144 *)  Done(); 
(* 145 *)  l(); l(); pl 2; gl 7; ThmCut "minv"; 
(* 150 *)  su 2 "a1"; 
(* 151 *)  l(); ThmCut "negeqsymm"; 
(* 153 *)  su 2 "0"; 
(* 154 *)  su 3 "a1"; 
(* 155 *)  gl 7; gr 1; Done(); 
(* 158 *)  Done(); 
(* 159 *)  rwr []; ThmCut "symm"; 
(* 161 *)  su 3 "a1 * /(a1)"; 
(* 162 *)  su 4 "1"; 
(* 163 *)  l(); Done(); 
(* 165 *)  gl2 3; rwl []; ThmCut "3.2.iv"; 
(* 168 *)  

(* 167

No such theorem as 3.2.iv*)


(* Sequent snapshot:


1:  1 = a1 * /(a1)

2:  0 <= a1 * /(a1)

3:  ~0 eq 1

4:  Real(a1)

5:  Real(1)

6:  Real(0)

7:  0 <= a1

8:  ~0 eq a1

9:  a1 * /(a1) = 1

|-

1:  0 <= /(a1)


*)

ThmCut "thm 3.2.iv"; 
(* 169 *)  su 4 "/(a1)"; 
(* 170 *)  ThmCut "ordmult"; 
(* 171 *)  su 4 "0"; 
(* 172 *)  su 6 "/(a1) * /(a1)"; 
(* 173 *)  su 5 "a1"; 
(* 174 *)  l(); r(); Done(); 
(* 177 *)  gl 8; gr 1; Done(); 
(* 180 *)  ThmCut "mcom"; 
(* 181 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 184 *)  rwl [2]; pl 1; ThmCut "mcom"; 
(* 187 *)  su 5 "a1 * /(a1)"; 
(* 188 *)  su 6 "/(a1)"; 
(* 189 *)  rwl []; pl 1; ThmCut "mas"; 
(* 192 *)  su 6 "a1"; 
(* 193 *)  su 7 "/(a1)"; 
(* 194 *)  su 8 "/(a1)"; 
(* 195 *)  ThmCut "symm"; 
(* 196 *)  su 8 "[a1 * /(a1)] * /(a1)"; 
(* 197 *)  su 9 "a1 * /(a1) * /(a1)"; 
(* 198 *)  l(); Done(); 
(* 200 *)  gl2 3; rwl []; ThmCut "minv"; 
(* 203 *)  su 9 "a1"; 
(* 204 *)  l(); ThmCut "negeqsymm"; 
(* 206 *)  su 9 "0"; 
(* 207 *)  su 10 "a1"; 
(* 208 *)  gl 11; gr 1; Done(); 
(* 211 *)  Done(); 
(* 212 *)  gl2 3; rwl []; ThmCut "thm 3.1.ii"; 
(* 215 *)  gl 9; gr 1; Done(); 
(* 218 *)  gl2 3; rwl []; ThmCut "mcom"; 
(* 221 *)  gl2 3; rwl []; pl 1; ThmCut "mid"; 
(* 225 *)  ThmCut "rinv"; 
(* 226 *)  su 11 "a1"; 
(* 227 *)  su 10 "/(a1)"; 
(* 228 *)  Done(); 
(* 229 *)  rwl []; gl 2; gr 1; Done(); 
(* 233 *)  ThmCut "lemma 1.1"; 
(* 234 *)  su 10 "a1"; 
(* 235 *)  gl 4; gr 1; Done(); 
(* 238 *)  gl 2; gr 1; Done(); 
(* 241 *)  

(* 240

Not done!*)


(* Sequent snapshot:


1:  ~0 eq a1

2:  ~0 eq 1

3:  Real(a1)

4:  Real(1)

5:  Real(0)

6:  0 <= a1

|-

1:  ~a1 eq 0

2:  ~0 eq /(a1)


*)

ThmCut "negeqsymm"; 
(* 242 *)  su 10 "0"; 
(* 243 *)  su 11 "a1"; 
(* 244 *)  Done(); 
(* 245 *)  Done(); 
(* 246 *)  ThmCut "negeqsymm"; 
(* 247 *)  su 11 "/(a1)"; 
(* 248 *)  su 12 "0"; 
(* 249 *)  Done(); 
(* 250 *)  Done(); 
(* 251 *)  NameSequent 1 "3.2.vi"; 
(* 252 *)  

(* 251

3.2.vi:



1:  0 < a1

2:  ~0 eq 1

3:  Real(a1)

4:  Real(1)

5:  Real(0)

|-

1:  0 < /(a1)

*)