(* 1 *)  Declarepredicate "Real" [0]; 
(* 2 *)  

(* 2 *)  Declarefunction "+" [0,0,0]; 
(* 3 *)  

(* 3 *)  Declarefunction "*" [0,0,0]; 
(* 4 *)  

(* 4 *)  Declarefunction "-" [0,0]; 
(* 5 *)  setprecrightabove "*" "+"; 

(* 6 *)  Declarepredicate "<=" [0,0]; 
(* 7 *)  

(* 7 *)  Declarefunction "/" [0,0]; 
(* 8 *)  

(* 8 *)  Definefunction 2 "--" "x1--x2" "x1+ -(x2)"; 
(* 9 *)  

(* 9 *)  Definepredicate 2 "eq" "x1 eq x2" "x1+0=x2+0"; 
(* 10 *)  

(* 10 *)  Definepredicate 2 "<" "x1 < x2" "(x1 <= x2) & ~(x1 eq x2)"; 
(* 11 *)  

(* 11 *)  Axiom "nontriv" [] ["~(0 eq 1)"]; 
(* 12 *)  

(* 11

nontriv:



|-

1:  ~0 eq 1

*)



(* 12 *)  Axiom "rplus" [] ["Real(a1+a2)"]; 
(* 13 *)  

(* 12

rplus:



|-

1:  Real(a1 + a2)

*)



(* 13 *)  Axiom "rtimes" [] ["Real(a1*a2)"]; 
(* 14 *)  

(* 13

rtimes:



|-

1:  Real(a1 * a2)

*)



(* 14 *)  Axiom "rminus" [] ["Real(-(a1))"]; 
(* 15 *)  

(* 14

rminus:



|-

1:  Real(-(a1))

*)



(* 15 *)  Axiom "rinv" [] ["Real( /(a1))"]; 
(* 16 *)  

(* 15

rinv:



|-

1:  Real(/(a1))

*)



(* 16 *)  Axiom "acom" [] ["a1+a2=a2+a1"]; 
(* 17 *)  

(* 16

acom:



|-

1:  a1 + a2 = a2 + a1

*)



(* 17 *)  Axiom "aas" [] ["[a1+a2]+a3=a1+a2+a3"]; 
(* 18 *)  

(* 17

aas:



|-

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

*)



(* 18 *)  Axiom "aid" ["Real(a1)"] ["a1+0=a1"]; 
(* 19 *)  

(* 18

aid:



1:  Real(a1)

|-

1:  a1 + 0 = a1

*)



(* 19 *)  Axiom "ainv" [] ["a1+ -(a1)=0"]; 
(* 20 *)  

(* 19

ainv:



|-

1:  a1 + -(a1) = 0

*)



(* 20 *)  Axiom "mas" [] ["[a1*a2]*a3=a1*a2*a3"]; 
(* 21 *)  

(* 20

mas:



|-

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

*)



(* 21 *)  Axiom "mcom" [] ["a1*a2=a2*a1"]; 
(* 22 *)  

(* 21

mcom:



|-

1:  a1 * a2 = a2 * a1

*)



(* 22 *)  Axiom "mid" ["Real(a1)"] ["a1*1=a1"]; 
(* 23 *)  

(* 22

mid:



1:  Real(a1)

|-

1:  a1 * 1 = a1

*)



(* 23 *)  Axiom "minv" [] ["~(a1 eq 0)-> (a1* /(a1) = 1)"]; 
(* 24 *)  

(* 23

minv:



|-

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

*)



(* 24 *)  Axiom "dist" [] ["a1*[a2+a3]=a1*a2+a1*a3"]; 
(* 25 *)  

(* 24

dist:



|-

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

*)



(* 25 *)  Axiom "totorder" [] ["(a1 <= a2) v (a2 <= a1)"]; 
(* 26 *)  

(* 25

totorder:



|-

1:  a1 <= a2 v a2 <= a1

*)



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

(* 26

eqbyord:



|-

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

*)



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

(* 27

ordtrans:



|-

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

*)



(* 28 *)  Axiom "ordadd" [] ["(a1 <= a2)->(a1+a3 <= a2+a3)"]; 
(* 29 *)  

(* 28

ordadd:



|-

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

*)



(* 29 *)  Axiom "ordaddl" [] ["(a1 <= a2)->(a3+a1 <= a3+a2)"]; 
(* 30 *)  

(* 29

ordaddl:



|-

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

*)



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

(* 30

ordmult:



|-

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

*)



(* 31 *)  StartSequent [] ["a1=a1"]; 
(* 32 *)  r(); NameSequent 1 "reflx"; 
(* 34 *)  

(* 33

reflx:



|-

1:  a1 = a1

*)



(* 34 *)  StartSequent [] ["a1=a2 -> a2=a1"]; 
(* 35 *)  r(); crwr []; ThmCut "reflx"; 
(* 38 *)  su 3 "a1"; 
(* 39 *)  Done(); 
(* 40 *)  NameSequent 1 "symm"; 
(* 41 *)  

(* 40

symm:



|-

1:  a1 = a2 -> a2 = a1

*)



(* 41 *)  StartSequent [] ["((a1=a2) & (a2=a3))->(a1=a3)"]; 
(* 42 *)  r(); l(); crwl []; gl 2; gr 1; Done(); 
(* 48 *)  NameSequent 1 "trans"; 
(* 49 *)  

(* 48

trans:



|-

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

*)



(* 49 *)  StartSequent ["Real(a1)","Real(a2)","~(a1 eq a2)"] ["~(a2 eq a1)"]; 
(* 50 *)  gl 3; l(); gr 2; r(); l(); r(); ThmCut "symm"; 
(* 57 *)  su 3 "a2 + 0"; 
(* 58 *)  su 4 "a1 + 0"; 
(* 59 *)  l(); Done(); 
(* 61 *)  Done(); 
(* 62 *)  NameSequent 1 "negeqsymm"; 
(* 63 *)  

(* 62

negeqsymm:



1:  ~a1 eq a2

|-

1:  ~a2 eq a1

*)



(* 63 *)  StartSequent [] ["Real(0)"]; 
(* 64 *)  ThmCut "rplus"; 
(* 65 *)  su 1 "1"; 
(* 66 *)  su 2 "-(1)"; 
(* 67 *)  ThmCut "ainv"; 
(* 68 *)  su 2 "1"; 
(* 69 *)  rwl []; gl 2; gr 1; Done(); 
(* 73 *)  NameSequent 1 "zero"; 
(* 74 *)  

(* 73

zero:



|-

1:  Real(0)

*)



(* 74 *)  StartSequent [] ["Real(1)"]; 
(* 75 *)  ThmCut "rtimes"; 
(* 76 *)  su 1 "1"; 
(* 77 *)  su 2 "/(1)"; 
(* 78 *)  ThmCut "minv"; 
(* 79 *)  su 2 "1"; 
(* 80 *)  l(); ThmCut "nontriv"; 
(* 82 *)  ThmCut "negeqsymm"; 
(* 83 *)  su 2 "0"; 
(* 84 *)  su 3 "1"; 
(* 85 *)  Done(); 
(* 86 *)  Done(); 
(* 87 *)  rwl []; gl 2; gr 1; Done(); 
(* 91 *)  NameSequent 1 "one"; 
(* 92 *)  

(* 91

one:



|-

1:  Real(1)

*)



(* 92 *)  StartSequent [] ["(a1=a2)-> (a1+a3 = a2+a3)"]; 
(* 93 *)  r(); crwr []; r(); NameSequent 1 "aeq"; 
(* 97 *)  

(* 96

aeq:



|-

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

*)



(* 97 *)  StartSequent [] ["(a1=a2)-> (a3+a1 = a3+a2)"]; 
(* 98 *)  r(); crwr []; r(); NameSequent 1 "aeql"; 
(* 102 *)  

(* 101

aeql:



|-

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

*)



(* 102 *)  StartSequent [] ["(a1=a2)-> (a1*a3 = a2*a3)"]; 
(* 103 *)  r(); crwr []; r(); NameSequent 1 "meq"; 
(* 107 *)  

(* 106

meq:



|-

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

*)



(* 107 *)  StartSequent [] ["(a1=a2)-> (a3*a1 = a3*a2)"]; 
(* 108 *)  r(); crwr []; r(); NameSequent 1 "meql"; 
(* 112 *)  

(* 111

meql:



|-

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

*)



(* 112 *)  StartSequent [] ["[a1+a2]*a3 = a1*a3 + a2*a3"]; 
(* 113 *)  ThmCut "dist"; 
(* 114 *)  su 4 "a3"; 
(* 115 *)  su 5 "a1"; 
(* 116 *)  su 6 "a2"; 
(* 117 *)  ThmCut "mcom"; 
(* 118 *)  su 6 "a3"; 
(* 119 *)  su 7 "[a1+a2]"; 
(* 120 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 123 *)  su 7 "a3"; 
(* 124 *)  su 8 "a1"; 
(* 125 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 128 *)  su 8 "a3"; 
(* 129 *)  su 9 "a2"; 
(* 130 *)  rwl []; gl 2; gr 1; Done(); 
(* 134 *)  NameSequent 1 "distr"; 
(* 135 *)  

(* 134

distr:



|-

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

*)



(* 135 *)  StartSequent ["Real(a1)","Real(a2)","Real(a3)"] ["(a1+a3=a2+a3)-> a1=a2"]; 
(* 136 *)  r(); ThmCut "aeq"; 
(* 138 *)  su 4 "a1+a3"; 
(* 139 *)  su 5 "a2+a3"; 
(* 140 *)  su 6 "-(a3)"; 
(* 141 *)  l(); Done(); 
(* 143 *)  ThmCut "aas"; 
(* 144 *)  su 6 "a1"; 
(* 145 *)  su 7 "-(a3)"; 
(* 146 *)  su 8 "a3"; 
(* 147 *)  rwl []; pl 1; pl 2; gl 4; ThmCut "aas"; 
(* 152 *)  su 8 "a2"; 
(* 153 *)  su 10 "a3"; 
(* 154 *)  su 9 "-(a3)"; 
(* 155 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 158 *)  su 9 "a3"; 
(* 159 *)  rwl []; pl 1; ThmCut "aid"; 
(* 162 *)  su 9 "a1"; 
(* 163 *)  gl 2; gr 1; Done(); 
(* 166 *)  rwl []; pl 1; ThmCut "aid"; 
(* 169 *)  su 9 "a2"; 
(* 170 *)  gl 3; gr 1; Done(); 
(* 173 *)  rwl []; gl 2; gr 1; Done(); 
(* 177 *)  NameSequent 1 "thm 3.1.i"; 
(* 178 *)  

(* 177

thm 3.1.i:



1:  Real(a1)

2:  Real(a2)

|-

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

*)



(* 178 *)  StartSequent ["Real(a1)","Real(0)"] ["a1*0 = 0"]; 
(* 179 *)  ThmCut "dist"; 
(* 180 *)  su 2 "a1"; 
(* 181 *)  su 3 "0"; 
(* 182 *)  su 4 "0"; 
(* 183 *)  ThmCut "aid"; 
(* 184 *)  su 4 "0"; 
(* 185 *)  gl 3; gr 1; Done(); 
(* 188 *)  rwl []; pl 1; ThmCut "aeq"; 
(* 191 *)  su 4 "a1*0"; 
(* 192 *)  su 5 "a1*0 + a1*0"; 
(* 193 *)  su 6 "-(a1*0)"; 
(* 194 *)  l(); Done(); 
(* 196 *)  ThmCut "ainv"; 
(* 197 *)  su 6 "a1*0"; 
(* 198 *)  ThmCut "aas"; 
(* 199 *)  su 6 "a1*0"; 
(* 200 *)  su 8 "a1*0"; 
(* 201 *)  su 7 "-(a1*0)"; 
(* 202 *)  gl2 3; rwl []; pl 1; gl 2; gl2 5; gl 5; gl2 3; rwl []; pl 1; ThmCut "aid"; 
(* 212 *)  ThmCut "rtimes"; 
(* 213 *)  su 8 "a1"; 
(* 214 *)  su 9 "0"; 
(* 215 *)  su 7 "a1*0"; 
(* 216 *)  Done(); 
(* 217 *)  rwl []; pl 1; ThmCut "acom"; 
(* 220 *)  undo(); undo(); ThmCut "symm"; 
(* 223 *)  su 9 "0"; 
(* 224 *)  su 10 "a1*0"; 
(* 225 *)  l(); Done(); 
(* 227 *)  Done(); 
(* 228 *)  NameSequent 1 "thm 3.1.ii"; 
(* 229 *)  

(* 228

thm 3.1.ii:



1:  Real(0)

|-

1:  a1 * 0 = 0

*)



(* 229 *)  StartSequent [] ["-(a1)*a2 = -(a1*a2)"]; 
(* 230 *)  ThmCut "ainv"; 
(* 231 *)  su 3 "a1"; 
(* 232 *)  ThmCut "distr"; 
(* 233 *)  ThmCut "meq"; 
(* 234 *)  su 6 "a1+ -(a1)"; 
(* 235 *)  su 7 "0"; 
(* 236 *)  l(); gl 2; gr 1; Done(); 
(* 240 *)  su 8 "a2"; 
(* 241 *)  su 3 "a1"; 
(* 242 *)  su 5 "-(a1)"; 
(* 243 *)  su 4 "a2"; 
(* 244 *)  gl 2; gl2 3; rwl []; pl 1; ThmCut "mcom"; 
(* 249 *)  su 8 "0"; 
(* 250 *)  su 9 "a2"; 
(* 251 *)  rwl []; pl 1; ThmCut "thm 3.1.ii"; 
(* 254 *)  ThmCut "zero"; 
(* 255 *)  Done(); 
(* 256 *)  su 9 "a2"; 
(* 257 *)  rwl []; pl 1; pl 2; ThmCut "aeql"; 
(* 261 *)  su 9 "a1*a2 + -(a1)*a2"; 
(* 262 *)  su 11 "0"; 
(* 263 *)  l(); Done(); 
(* 265 *)  su 10 "-(a1*a2)"; 
(* 266 *)  ThmCut "acom"; 
(* 267 *)  su 10 "-(a1*a2)"; 
(* 268 *)  su 11 "a1*a2"; 
(* 269 *)  rwl []; crwl []; rwl [1]; crwl [1]; rwl [2]; undo(); undo(); ThmCut "aas"; 
(* 277 *)  su 11 "-(a1*a2)"; 
(* 278 *)  su 13 "a1*a2"; 
(* 279 *)  su 12 "-(a1)*a2"; 
(* 280 *)  ThmCut "symm"; 
(* 281 *)  su 12 "[-(a1 * a2) + a1 * a2] + -(a1) * a2"; 
(* 282 *)  su 13 "-(a1 * a2) + a1 * a2 + -(a1) * a2"; 
(* 283 *)  l(); Done(); 
(* 285 *)  pl 2; gl 4; gl2 3; rwl []; pl 1; gl 3; rwl []; pl 1; pl 2; ThmCut "aid"; 
(* 295 *)  ThmCut "rminus"; 
(* 296 *)  su 14 "a1*a2"; 
(* 297 *)  su 13 "-(a1*a2)"; 
(* 298 *)  Done(); 
(* 299 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 302 *)  su 13 "a1*a2"; 
(* 303 *)  rwl []; pl 1; ThmCut "acom"; 
(* 306 *)  su 13 "0"; 
(* 307 *)  su 14 "-(a1) * a2"; 
(* 308 *)  rwl []; pl 1; ThmCut "aid"; 
(* 311 *)  ThmCut "rtimes"; 
(* 312 *)  su 15 "-(a1)"; 
(* 313 *)  su 16 "a2"; 
(* 314 *)  su 14 "-(a1) * a2"; 
(* 315 *)  Done(); 
(* 316 *)  rwl []; gl 2; gr 1; Done(); 
(* 320 *)  NameSequent 1 "thm 3.1.iii"; 
(* 321 *)  

(* 320

thm 3.1.iii:



|-

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

*)



(* 321 *)  StartSequent ["Real(a1)","Real(a2)"] ["-(a1)* -(a2) = a1*a2"]; 
(* 322 *)  ThmCut "ainv"; 
(* 323 *)  su 3 "a2"; 
(* 324 *)  ThmCut "meql"; 
(* 325 *)  su 3 "a2 + -(a2)"; 
(* 326 *)  su 5 "0"; 
(* 327 *)  l(); Done(); 
(* 329 *)  su 4 "-(a1)"; 
(* 330 *)  ThmCut "thm 3.1.ii"; 
(* 331 *)  ThmCut "zero"; 
(* 332 *)  Done(); 
(* 333 *)  su 4 "-(a1)"; 
(* 334 *)  rwl []; pl 1; pl 2; ThmCut "dist"; 
(* 338 *)  su 4 "-(a1)"; 
(* 339 *)  su 5 "a2"; 
(* 340 *)  su 6 "-(a2)"; 
(* 341 *)  gl2 4; rwl []; pl 1; ThmCut "aeql"; 
(* 345 *)  su 6 "-(a1) * a2 + -(a1) * -(a2)"; 
(* 346 *)  su 8 "0"; 
(* 347 *)  l(); Done(); 
(* 349 *)  su 7 "a1*a2"; 
(* 350 *)  pl 2; ThmCut "thm 3.1.iii"; 
(* 352 *)  su 7 "a1"; 
(* 353 *)  su 8 "a2"; 
(* 354 *)  gl2 4; rwl []; pl 1; ThmCut "ainv"; 
(* 358 *)  su 8 "a1*a2"; 
(* 359 *)  rwl []; ThmCut "aas"; 
(* 361 *)  su 8 "a1*a2"; 
(* 362 *)  su 10 "-(a1 * a2)"; 
(* 363 *)  su 9 "-(a1) * -(a2)"; 
(* 364 *)  ThmCut "symm"; 
(* 365 *)  gl 2; gl2 3; rwl []; su 9 "[a1 * a2 + -(a1 * a2)] + -(a1) * -(a2)"; 
(* 369 *)  su 10 "a1 * a2 + -(a1 * a2) + -(a1) * -(a2)"; 
(* 370 *)  gl 5; l(); gl 2; gr 1; Done(); 
(* 375 *)  gl2 4; rwl []; pl 1; pl 5; gl 4; rwl []; pl 1; ThmCut "aid"; 
(* 383 *)  ThmCut "rtimes"; 
(* 384 *)  su 11 "a1"; 
(* 385 *)  su 12 "a2"; 
(* 386 *)  su 10 "a1 * a2"; 
(* 387 *)  Done(); 
(* 388 *)  rwl []; pl 1; ThmCut "acom"; 
(* 391 *)  su 12 "0"; 
(* 392 *)  su 13 "-(a1) * -(a2)"; 
(* 393 *)  rwl []; pl 1; ThmCut "aid"; 
(* 396 *)  ThmCut "rtimes"; 
(* 397 *)  su 14 "-(a1)"; 
(* 398 *)  su 15 "-(a2)"; 
(* 399 *)  su 13 "-(a1) * -(a2)"; 
(* 400 *)  Done(); 
(* 401 *)  rwl []; gl 2; gr 1; Done(); 
(* 405 *)  NameSequent 1 "thm 3.1.iv"; 
(* 406 *)  

(* 405

thm 3.1.iv:



|-

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

*)



(* 406 *)  StartSequent ["Real(a1)","Real(a2)","Real(a3)","a1*a3=a2*a3","~(a3 eq 0)"] ["a1=a2"]; 
(* 407 *)  ThmCut "meq"; 
(* 408 *)  su 4 "a1 * a3"; 
(* 409 *)  su 5 "a2 * a3"; 
(* 410 *)  l(); gl 4; gr 1; Done(); 
(* 414 *)  su 6 "/(a3)"; 
(* 415 *)  pl 5; ThmCut "mas"; 
(* 417 *)  su 7 "/(a3)"; 
(* 418 *)  gl2 3; rwl []; pl 1; ThmCut "mas"; 
(* 422 *)  su 9 "/(a3)"; 
(* 423 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 426 *)  su 10 "a1"; 
(* 427 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 430 *)  su 11 "a2"; 
(* 431 *)  rwl []; pl 1; ThmCut "minv"; 
(* 434 *)  su 12 "a3"; 
(* 435 *)  l(); gl 5; gr 1; Done(); 
(* 439 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 442 *)  su 12 "1"; 
(* 443 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 446 *)  su 13 "1"; 
(* 447 *)  rwl []; pl 1; ThmCut "mid"; 
(* 450 *)  su 14 "a1"; 
(* 451 *)  gl 2; gr 1; Done(); 
(* 454 *)  rwl []; pl 1; ThmCut "mid"; 
(* 457 *)  su 14 "a2"; 
(* 458 *)  gl 3; gr 1; Done(); 
(* 461 *)  rwl []; gl 2; gr 1; Done(); 
(* 465 *)  NameSequent 1 "thm 3.1.v"; 
(* 466 *)  

(* 465

thm 3.1.v:



1:  Real(a1)

2:  Real(a2)

3:  a1 * a3 = a2 * a3

4:  ~a3 eq 0

|-

1:  a1 = a2

*)



(* 466 *)  StartSequent ["Real(a1)","Real(a2)","a1*a2=0","~(a2 eq 0)"] ["(a1=0) v (a2=0)"]; 
(* 467 *)  ThmCut "meq"; 
(* 468 *)  gl2 4; su 3 "a1*a2"; 
(* 470 *)  su 4 "0"; 
(* 471 *)  l(); Done(); 
(* 473 *)  su 5 "/(a2)"; 
(* 474 *)  ThmCut "mas"; 
(* 475 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 478 *)  su 5 "0"; 
(* 479 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 482 *)  su 6 "a1"; 
(* 483 *)  rwl []; pl 1; ThmCut "thm 3.1.ii"; 
(* 486 *)  ThmCut "zero"; 
(* 487 *)  Done(); 
(* 488 *)  rwl []; pl 1; ThmCut "minv"; 
(* 491 *)  su 7 "a2"; 
(* 492 *)  l(); gl 3; gr 1; Done(); 
(* 496 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 499 *)  rwl []; pl 1; ThmCut "mid"; 
(* 502 *)  su 7 "a1"; 
(* 503 *)  gl 4; gr 1; Done(); 
(* 506 *)  rwl []; r(); gl 2; gr 1; Done(); 
(* 511 *)  NameSequent 1 "thm 3.1.vi"; 
(* 512 *)  

(* 511

thm 3.1.vi:



1:  Real(a1)

2:  a1 * a2 = 0

3:  ~a2 eq 0

|-

1:  a1 = 0 v a2 = 0

*)



(* 512 *)  StartSequent ["Real(a1)","Real(a2)","a1 <= a2"] ["-(a2) <= -(a1)"]; 
(* 513 *)  ThmCut "ordadd"; 
(* 514 *)  su 3 "a1"; 
(* 515 *)  su 4 "a2"; 
(* 516 *)  l(); gl 3; gr 1; Done(); 
(* 520 *)  su 5 "-(a1)"; 
(* 521 *)  ThmCut "ainv"; 
(* 522 *)  rwl []; pl 1; ThmCut "ordadd"; 
(* 525 *)  su 5 "0"; 
(* 526 *)  su 6 "a2 + -(a1)"; 
(* 527 *)  l(); Done(); 
(* 529 *)  su 7 "-(a2)"; 
(* 530 *)  ThmCut "acom"; 
(* 531 *)  rwl []; pl 1; ThmCut "acom"; 
(* 534 *)  su 7 "a2"; 
(* 535 *)  su 8 "-(a1)"; 
(* 536 *)  rwl []; pl 1; ThmCut "aid"; 
(* 539 *)  ThmCut "rminus"; 
(* 540 *)  su 9 "a2"; 
(* 541 *)  su 8 "-(a2)"; 
(* 542 *)  Done(); 
(* 543 *)  rwl []; pl 1; ThmCut "aas"; 
(* 546 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 549 *)  su 8 "a2"; 
(* 550 *)  rwl []; pl 1; ThmCut "rminus"; 
(* 553 *)  su 8 "a1"; 
(* 554 *)  ThmCut "aid"; 
(* 555 *)  su 8 "-(a1)"; 
(* 556 *)  Done(); 
(* 557 *)  pl 2; gl 6; rwl []; gl 2; gr 1; Done(); 
(* 563 *)  NameSequent 1 "thm 3.2.i"; 
(* 564 *)  

(* 563

thm 3.2.i:



1:  a1 <= a2

|-

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

*)



(* 564 *)  StartSequent [] ["-(0) = 0"]; 
(* 565 *)  ThmCut "acom"; 
(* 566 *)  su 1 "-(0)"; 
(* 567 *)  su 2 "0"; 
(* 568 *)  ThmCut "aid"; 
(* 569 *)  ThmCut "rminus"; 
(* 570 *)  su 3 "0"; 
(* 571 *)  su 2 "-(0)"; 
(* 572 *)  Done(); 
(* 573 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 576 *)  su 2 "0"; 
(* 577 *)  rwl []; gl 2; gr 1; Done(); 
(* 581 *)  NameSequent 1 "zeros"; 
(* 582 *)  

(* 581

zeros:



|-

1:  -(0) = 0

*)



(* 582 *)  StartSequent ["Real(a1)"] ["-(-(a1))=a1"]; 
(* 583 *)  ThmCut "aas"; 
(* 584 *)  su 2 "a1"; 
(* 585 *)  su 4 "-(a1)"; 
(* 586 *)  su 3 "-(-(a1))"; 
(* 587 *)  ThmCut "ainv"; 
(* 588 *)  su 3 "-(a1)"; 
(* 589 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 592 *)  rwl []; pl 1; ThmCut "aid"; 
(* 595 *)  su 3 "a1"; 
(* 596 *)  gl 2; gr 1; Done(); 
(* 599 *)  rwl []; pl 1; ThmCut "acom"; 
(* 602 *)  rwl []; pl 1; ThmCut "aid"; 
(* 605 *)  su 3 "-(-(a1))"; 
(* 606 *)  ThmCut "rminus"; 
(* 607 *)  su 3 "-(a1)"; 
(* 608 *)  Done(); 
(* 609 *)  rwl []; gl 2; gr 1; Done(); 
(* 613 *)  NameSequent 1 "2neg"; 
(* 614 *)  

(* 613

2neg:



1:  Real(a1)

|-

1:  -(-(a1)) = a1

*)



(* 614 *)  StartSequent ["Real(a1)","Real(a2)","Real(a3)","a1 <= a2","a3 <= 0"] ["a2*a3 <= a1*a3"]; 
(* 615 *)  ThmCut "thm 3.2.i"; 
(* 616 *)  su 4 "a3"; 
(* 617 *)  su 5 "0"; 
(* 618 *)  gl 5; gr 1; Done(); 
(* 621 *)  ThmCut "zeros"; 
(* 622 *)  rwl []; pl 1; ThmCut "ordmult"; 
(* 625 *)  su 5 "a1"; 
(* 626 *)  su 7 "a2"; 
(* 627 *)  su 6 "-(a3)"; 
(* 628 *)  l(); r(); gl 5; gr 1; Done(); 
(* 633 *)  Done(); 
(* 634 *)  ThmCut "mcom"; 
(* 635 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 638 *)  rwl [2]; pl 1; ThmCut "thm 3.1.iii"; 
(* 641 *)  rwl []; pl 1; ThmCut "thm 3.1.iii"; 
(* 644 *)  rwl [2]; su 6 "a3"; 
(* 646 *)  su 7 "a2"; 
(* 647 *)  rwl []; pl 1; ThmCut "thm 3.2.i"; 
(* 650 *)  su 7 "-(a3 * a1)"; 
(* 651 *)  su 8 "-(a3 * a2)"; 
(* 652 *)  Done(); 
(* 653 *)  ThmCut "2neg"; 
(* 654 *)  su 8 "a3 * a2"; 
(* 655 *)  ThmCut "rtimes"; 
(* 656 *)  su 8 "a3"; 
(* 657 *)  su 9 "a2"; 
(* 658 *)  Done(); 
(* 659 *)  rwl []; pl 1; ThmCut "2neg"; 
(* 662 *)  su 9 "a3 * a1"; 
(* 663 *)  ThmCut "rtimes"; 
(* 664 *)  su 9 "a3"; 
(* 665 *)  su 10 "a1"; 
(* 666 *)  Done(); 
(* 667 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 670 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 673 *)  rwl [2]; gl 2; gr 1; Done(); 
(* 677 *)  NameSequent 1 "thm 3.2.ii"; 
(* 678 *)  

(* 677

thm 3.2.ii:



1:  a1 <= a2

2:  a3 <= 0

|-

1:  a2 * a3 <= a1 * a3

*)



(* 678 *)  StartSequent ["Real(a1)","Real(a2)","0 <= a1","0 <= a2"] ["0 <= a1*a2"]; 
(* 679 *)  ThmCut "ordmult"; 
(* 680 *)  su 3 "0"; 
(* 681 *)  su 5 "a1"; 
(* 682 *)  su 4 "a2"; 
(* 683 *)  l(); r(); gl 3; gr 1; Done(); 
(* 688 *)  gl 4; gr 1; Done(); 
(* 691 *)  ThmCut "mcom"; 
(* 692 *)  rwl []; pl 1; ThmCut "mid"; 
(* 695 *)  su 4 "a2"; 
(* 696 *)  gl 3; gr 1; Done(); 
(* 699 *)  undo(); undo(); undo(); undo(); undo(); undo(); ThmCut "thm 3.1.ii"; 
(* 706 *)  ThmCut "zero"; 
(* 707 *)  Done(); 
(* 708 *)  rwl []; gl 2; gr 1; Done(); 
(* 712 *)  NameSequent 1 "thm 3.2.iii"; 
(* 713 *)  

(* 712

thm 3.2.iii:



1:  0 <= a1

2:  0 <= a2

|-

1:  0 <= a1 * a2

*)



(* 713 *)  StartSequent ["Real(a1)"] ["0 <= a1*a1"]; 
(* 714 *)  ThmCut "totorder"; 
(* 715 *)  su 2 "0"; 
(* 716 *)  su 3 "a1"; 
(* 717 *)  l(); ThmCut "ordmult"; 
(* 719 *)  su 3 "0"; 
(* 720 *)  su 5 "a1"; 
(* 721 *)  su 4 "a1"; 
(* 722 *)  l(); r(); Done(); 
(* 725 *)  Done(); 
(* 726 *)  ThmCut "mcom"; 
(* 727 *)  rwl []; pl 1; ThmCut "thm 3.1.ii"; 
(* 730 *)  ThmCut "zero"; 
(* 731 *)  Done(); 
(* 732 *)  rwl []; gl 2; gr 1; Done(); 
(* 736 *)  ThmCut "thm 3.2.i"; 
(* 737 *)  su 4 "a1"; 
(* 738 *)  su 5 "0"; 
(* 739 *)  Done(); 
(* 740 *)  ThmCut "zeros"; 
(* 741 *)  rwl []; pl 1; ThmCut "ordmult"; 
(* 744 *)  su 5 "0"; 
(* 745 *)  su 7 "-(a1)"; 
(* 746 *)  su 6 "-(a1)"; 
(* 747 *)  l(); r(); Done(); 
(* 750 *)  Done(); 
(* 751 *)  ThmCut "mcom"; 
(* 752 *)  rwl []; pl 1; ThmCut "thm 3.1.ii"; 
(* 755 *)  ThmCut "zero"; 
(* 756 *)  Done(); 
(* 757 *)  su 6 "-(a1)"; 
(* 758 *)  rwl []; pl 1; ThmCut "thm 3.1.iv"; 
(* 761 *)  rwl []; gl 2; gr 1; Done(); 
(* 765 *)  NameSequent 1 "thm 3.2.iv"; 
(* 766 *)  

(* 765

thm 3.2.iv:



|-

1:  0 <= a1 * a1

*)



(* 766 *)  StartSequent ["Real(a1)","Real(a2)","a1 eq a2"] ["a2 eq a1"]; 
(* 767 *)  gl 3; l(); ThmCut "symm"; 
(* 770 *)  su 3 "a1 + 0"; 
(* 771 *)  su 4 "a2 + 0"; 
(* 772 *)  l(); Done(); 
(* 774 *)  rwl []; r(); Done(); 
(* 777 *)  NameSequent 1 "eqsymm"; 
(* 778 *)  

(* 777

eqsymm:



1:  a1 eq a2

|-

1:  a2 eq a1

*)



(* 778 *)  StartSequent ["Real(a1)","Real(a2)","a1 eq a2"] ["a1 = a2"]; 
(* 779 *)  gl 3; l(); ThmCut "aid"; 
(* 782 *)  su 3 "a1"; 
(* 783 *)  gl 2; gr 1; Done(); 
(* 786 *)  rwl []; pl 1; ThmCut "aid"; 
(* 789 *)  su 3 "a2"; 
(* 790 *)  gl 3; gr 1; Done(); 
(* 793 *)  rwl []; gl 2; gr 1; Done(); 
(* 797 *)  NameSequent 1 "req"; 
(* 798 *)  

(* 797

req:



1:  a1 eq a2

2:  Real(a1)

3:  Real(a2)

|-

1:  a1 = a2

*)



(* 798 *)  StartSequent ["Real(a1)","~(a1 eq 0)","~(1 eq 0)"] ["~(/(a1) eq 0)"]; 
(* 799 *)  ThmCut "minv"; 
(* 800 *)  su 2 "a1"; 
(* 801 *)  l(); gl 2; gr 1; Done(); 
(* 805 *)  r(); gl 4; l(); r(); gl 2; l(); ThmCut "aid"; 
(* 812 *)  ThmCut "rinv"; 
(* 813 *)  su 3 "a1"; 
(* 814 *)  su 2 "/(a1)"; 
(* 815 *)  Done(); 
(* 816 *)  rwl []; pl 1; ThmCut "aid"; 
(* 819 *)  ThmCut "zero"; 
(* 820 *)  su 2 "0"; 
(* 821 *)  Done(); 
(* 822 *)  rwl []; pl 1; ThmCut "meql"; 
(* 825 *)  su 2 "/(a1)"; 
(* 826 *)  su 4 "0"; 
(* 827 *)  l(); Done(); 
(* 829 *)  su 3 "a1"; 
(* 830 *)  gl 3; gl2 4; rwl []; ThmCut "thm 3.1.ii"; 
(* 834 *)  ThmCut "zero"; 
(* 835 *)  Done(); 
(* 836 *)  su 3 "a1"; 
(* 837 *)  pl 2; gl 5; rwl []; ThmCut "meql"; 
(* 841 *)  su 3 "1"; 
(* 842 *)  su 5 "0"; 
(* 843 *)  l(); gl 2; gr 1; Done(); 
(* 847 *)  su 4 "a1"; 
(* 848 *)  ThmCut "mid"; 
(* 849 *)  su 4 "a1"; 
(* 850 *)  gl 5; gr 1; Done(); 
(* 853 *)  rwl []; pl 1; gl 2; gl2 6; rwl []; ThmCut "aeq"; 
(* 859 *)  su 4 "a1"; 
(* 860 *)  su 5 "0"; 
(* 861 *)  su 6 "0"; 
(* 862 *)  l(); gl 2; gr 1; Done(); 
(* 866 *)  Done(); 
(* 867 *)  NameSequent 1 "lemma 1.1"; 
(* 868 *)  

(* 867

lemma 1.1:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  ~/(a1) eq 0

*)



(* 868 *)  StartSequent ["Real(0)","Real(1)","~(0 eq 1)"] ["0 < 1"]; 
(* 869 *)  ThmCut "thm 3.2.iv"; 
(* 870 *)  su 1 "1"; 
(* 871 *)  ThmCut "mid"; 
(* 872 *)  su 1 "1"; 
(* 873 *)  gl 3; gr 1; Done(); 
(* 876 *)  rwl []; r(); r(); gl 2; gr 1; Done(); 
(* 882 *)  gl 5; gr 1; Done(); 
(* 885 *)  NameSequent 1 "thm 3.2.v"; 
(* 886 *)  

(* 885

thm 3.2.v:



1:  Real(1)

2:  ~0 eq 1

|-

1:  0 < 1

*)



(* 886 *)  StartSequent ["Real(a1)","~(a1 eq 0)"] ["/(/(a1))=a1"]; 
(* 887 *)  ThmCut "mas"; 
(* 888 *)  su 2 "a1"; 
(* 889 *)  su 4 "/(a1)"; 
(* 890 *)  su 3 "/(/(a1))"; 
(* 891 *)  ThmCut "minv"; 
(* 892 *)  su 3 "a1"; 
(* 893 *)  l(); gl 3; gr 1; Done(); 
(* 897 *)  rwl [1]; pl 1; ThmCut "mcom"; 
(* 900 *)  rwl []; pl 1; ThmCut "mid"; 
(* 903 *)  ThmCut "rinv"; 
(* 904 *)  su 4 "/(a1)"; 
(* 905 *)  su 3 "/(/(a1))"; 
(* 906 *)  Done(); 
(* 907 *)  rwl []; pl 1; ThmCut "lemma 1.1"; 
(* 910 *)  su 3 "a1"; 
(* 911 *)  gl 2; gr 1; Done(); 
(* 914 *)  gl 3; gr 1; Done(); 
(* 917 *)  ThmCut "minv"; 
(* 918 *)  su 3 "/(a1)"; 
(* 919 *)  l(); Done(); 
(* 921 *)  ThmCut "mcom"; 
(* 922 *)  su 3 "a1"; 
(* 923 *)  su 4 "/(a1) * /(/(a1))"; 
(* 924 *)  gl2 4; rwl []; pl 1; gl 4; gl2 3; rwl []; pl 1; ThmCut "mcom"; 
(* 932 *)  rwl []; pl 1; ThmCut "mid"; 
(* 935 *)  su 4 "a1"; 
(* 936 *)  gl 2; gr 1; Done(); 
(* 939 *)  rwl []; gl 2; gr 1; Done(); 
(* 943 *)  NameSequent 1 "lemma 1.2"; 
(* 944 *)  

(* 943

lemma 1.2:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  /(/(a1)) = a1

*)



(* 944 *)  StartSequent ["0 < a1","~(0 eq 1)","Real(a1)","Real(1)","Real(0)"] ["0 < /(a1)"]; 
(* 945 *)  l(); l(); r(); r(); gl 3; l(); undo(); ThmCut "thm 3.2.v"; 
(* 953 *)  gl 2; gr 1; gl 2; gr 1; Done(); 
(* 958 *)  Done(); 
(* 959 *)  l(); l(); pl 2; gl 7; ThmCut "minv"; 
(* 964 *)  su 2 "a1"; 
(* 965 *)  l(); ThmCut "negeqsymm"; 
(* 967 *)  su 2 "0"; 
(* 968 *)  su 3 "a1"; 
(* 969 *)  gl 7; gr 1; Done(); 
(* 972 *)  Done(); 
(* 973 *)  rwr []; ThmCut "symm"; 
(* 975 *)  su 3 "a1 * /(a1)"; 
(* 976 *)  su 4 "1"; 
(* 977 *)  l(); Done(); 
(* 979 *)  gl2 3; rwl []; ThmCut "thm 3.2.iv"; 
(* 982 *)  su 4 "/(a1)"; 
(* 983 *)  ThmCut "ordmult"; 
(* 984 *)  su 4 "0"; 
(* 985 *)  su 6 "/(a1) * /(a1)"; 
(* 986 *)  su 5 "a1"; 
(* 987 *)  l(); r(); Done(); 
(* 990 *)  gl 8; gr 1; Done(); 
(* 993 *)  ThmCut "mcom"; 
(* 994 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 997 *)  rwl [2]; pl 1; ThmCut "mcom"; 
(* 1000 *)  su 5 "a1 * /(a1)"; 
(* 1001 *)  su 6 "/(a1)"; 
(* 1002 *)  rwl []; pl 1; ThmCut "mas"; 
(* 1005 *)  su 6 "a1"; 
(* 1006 *)  su 7 "/(a1)"; 
(* 1007 *)  su 8 "/(a1)"; 
(* 1008 *)  ThmCut "symm"; 
(* 1009 *)  su 8 "[a1 * /(a1)] * /(a1)"; 
(* 1010 *)  su 9 "a1 * /(a1) * /(a1)"; 
(* 1011 *)  l(); Done(); 
(* 1013 *)  gl2 3; rwl []; ThmCut "minv"; 
(* 1016 *)  su 9 "a1"; 
(* 1017 *)  l(); ThmCut "negeqsymm"; 
(* 1019 *)  su 9 "0"; 
(* 1020 *)  su 10 "a1"; 
(* 1021 *)  gl 11; gr 1; Done(); 
(* 1024 *)  Done(); 
(* 1025 *)  gl2 3; rwl []; ThmCut "thm 3.1.ii"; 
(* 1028 *)  gl 9; gr 1; Done(); 
(* 1031 *)  gl2 3; rwl []; ThmCut "mcom"; 
(* 1034 *)  gl2 3; rwl []; pl 1; ThmCut "mid"; 
(* 1038 *)  ThmCut "rinv"; 
(* 1039 *)  su 11 "a1"; 
(* 1040 *)  su 10 "/(a1)"; 
(* 1041 *)  Done(); 
(* 1042 *)  rwl []; gl 2; gr 1; Done(); 
(* 1046 *)  ThmCut "lemma 1.1"; 
(* 1047 *)  su 10 "a1"; 
(* 1048 *)  gl 4; gr 1; Done(); 
(* 1051 *)  gl 2; gr 1; ThmCut "negeqsymm"; 
(* 1054 *)  su 10 "0"; 
(* 1055 *)  su 11 "a1"; 
(* 1056 *)  Done(); 
(* 1057 *)  Done(); 
(* 1058 *)  ThmCut "negeqsymm"; 
(* 1059 *)  su 11 "/(a1)"; 
(* 1060 *)  su 12 "0"; 
(* 1061 *)  Done(); 
(* 1062 *)  Done(); 
(* 1063 *)  NameSequent 1 "3.2.vi"; 
(* 1064 *)  

(* 1063

3.2.vi:



1:  0 < a1

2:  ~0 eq 1

3:  Real(a1)

4:  Real(1)

5:  Real(0)

|-

1:  0 < /(a1)

*)