setprecrightabove "*" "+"; 

(* 2 *)  Axiom "zero" [] ["Real(0)"]; 
(* 3 *)  

(* 2

zero:



|-

1:  Real(0)

*)



(* 3 *)  Axiom "one" [] ["Real(1)"]; 
(* 4 *)  

(* 3

one:



|-

1:  Real(1)

*)



(* 4 *)  Axiom "rplus" [] ["Real(a1+a2)"]; 
(* 5 *)  

(* 4

rplus:



|-

1:  Real(a1 + a2)

*)



(* 5 *)  Axiom "rtimes" [] ["Real(a1*a2)"]; 
(* 6 *)  

(* 5

rtimes:



|-

1:  Real(a1 * a2)

*)



(* 6 *)  Axiom "rminus" [] ["Real(-(a1))"]; 
(* 7 *)  

(* 6

rminus:



|-

1:  Real(-(a1))

*)



(* 7 *)  Axiom "rinv" [] ["Real( /(a1))"]; 
(* 8 *)  

(* 7

rinv:



|-

1:  Real(/(a1))

*)



(* 8 *)  Axiom "acom" [] ["a1+a2=a2+a1"]; 
(* 9 *)  

(* 8

acom:



|-

1:  a1 + a2 = a2 + a1

*)



(* 9 *)  Axiom "aas" [] ["[a1+a2]+a3=a1+a2+a3"]; 
(* 10 *)  

(* 9

aas:



|-

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

*)



(* 10 *)  Axiom "aid" ["Real(a1)"] ["a1+0=a1"]; 
(* 11 *)  

(* 10

aid:



1:  Real(a1)

|-

1:  a1 + 0 = a1

*)



(* 11 *)  Axiom "ainv" [] ["a1+ -(a1)=0"]; 
(* 12 *)  

(* 11

ainv:



|-

1:  a1 + -(a1) = 0

*)



(* 12 *)  Definefunction 2 "--" "x1--x2" "x1+ -(x2)"; 
(* 13 *)  

(* 13 *)  Definepredicate 2 "eq" "x1 eq x2" "x1+0=x2+0"; 
(* 14 *)  

(* 14 *)  Axiom "mas" [] ["[a1*a2]*a3=a1*a2*a3"]; 
(* 15 *)  

(* 14

mas:



|-

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

*)



(* 15 *)  Axiom "mcom" [] ["a1*a2=a2*a1"]; 
(* 16 *)  

(* 15

mcom:



|-

1:  a1 * a2 = a2 * a1

*)



(* 16 *)  Axiom "mid" ["Real(a1)"] ["a1*1=a1"]; 
(* 17 *)  

(* 16

mid:



1:  Real(a1)

|-

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 "dist" [] ["a1*[a2+a3]=a1*a2+a1*a3"]; 
(* 19 *)  

(* 18

dist:



|-

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

*)



(* 19 *)  Axiom "totrder" [] ["(a1 <= a2) v (a2 <= a1)"]; 
(* 20 *)  

(* 19

totrder:



|-

1:  a1 <= a2 v a2 <= a1

*)



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

(* 20

eqbyord:



|-

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

*)



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

(* 21

ordtrans:



|-

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

*)



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

(* 22

ordeq:



|-

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

*)



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

(* 23

ordeql:



|-

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

*)



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

(* 24

ordmult:



|-

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

*)



(* 25 *)  Axiom "strctord" [] ["(a1 < a2) == ((a1 <= a2)& ~(a1 = a2))"]; 
(* 26 *)  

(* 25

strctord:



|-

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

*)



(* 26 *)  StartSequent [] ["a1=a1"]; 
(* 27 *)  r(); NameSequent 1 "reflx"; 
(* 29 *)  

(* 28

reflx:



|-

1:  a1 = a1

*)



(* 29 *)  StartSequent [] ["a1=a2 -> a2=a1"]; 
(* 30 *)  r(); crwr []; ThmCut "reflx"; 
(* 33 *)  su 3 "a1"; 
(* 34 *)  Done(); 
(* 35 *)  NameSequent 1 "symm"; 
(* 36 *)  

(* 35

symm:



|-

1:  a1 = a2 -> a2 = a1

*)



(* 36 *)  StartSequent [] ["((a1=a2) & (a2=a3))->(a1=a3)"]; 
(* 37 *)  r(); l(); crwl []; gl 2; gr 1; Done(); 
(* 43 *)  NameSequent 1 "trans"; 
(* 44 *)  

(* 43

trans:



|-

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

*)



(* 44 *)  StartSequent [] ["(a1=a2)-> (a1+a3 = a2+a3)"]; 
(* 45 *)  r(); crwr []; r(); NameSequent 1 "aeq"; 
(* 49 *)  

(* 48

aeq:



|-

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

*)



(* 49 *)  StartSequent [] ["(a1=a2)-> (a3+a1 = a3+a2)"]; 
(* 50 *)  r(); crwr []; r(); NameSequent 1 "aeql"; 
(* 54 *)  

(* 53

aeql:



|-

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

*)



(* 54 *)  StartSequent [] ["(a1=a2)-> (a1*a3 = a2*a3)"]; 
(* 55 *)  r(); crwr []; r(); NameSequent 1 "meq"; 
(* 59 *)  

(* 58

meq:



|-

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

*)



(* 59 *)  StartSequent [] ["(a1=a2)-> (a3*a1 = a3*a2)"]; 
(* 60 *)  r(); crwr []; r(); NameSequent 1 "meql"; 
(* 64 *)  

(* 63

meql:



|-

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

*)



(* 64 *)  StartSequent [] ["[a1+a2]*a3 = a1*a3 + a2*a3"]; 
(* 65 *)  ThmCut "dist"; 
(* 66 *)  su 4 "a3"; 
(* 67 *)  su 5 "a1"; 
(* 68 *)  su 6 "a2"; 
(* 69 *)  ThmCut "mcom"; 
(* 70 *)  su 6 "a3"; 
(* 71 *)  su 7 "[a1+a2]"; 
(* 72 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 75 *)  su 7 "a3"; 
(* 76 *)  su 8 "a1"; 
(* 77 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 80 *)  su 8 "a3"; 
(* 81 *)  su 9 "a2"; 
(* 82 *)  rwl []; gl 2; gr 1; Done(); 
(* 86 *)  NameSequent 1 "distr"; 
(* 87 *)  

(* 86

distr:



|-

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

*)



(* 87 *)  StartSequent ["Real(a1)","Real(a2)","Real(a3)"] ["(a1+a3=a2+a3)-> a1=a2"]; 
(* 88 *)  r(); ThmCut "aeq"; 
(* 90 *)  su 4 "a1+a3"; 
(* 91 *)  su 5 "a2+a3"; 
(* 92 *)  su 6 "-(a3)"; 
(* 93 *)  l(); Done(); 
(* 95 *)  ThmCut "aas"; 
(* 96 *)  su 6 "a1"; 
(* 97 *)  su 7 "-(a3)"; 
(* 98 *)  su 8 "a3"; 
(* 99 *)  rwl []; pl 1; pl 2; gl 4; ThmCut "aas"; 
(* 104 *)  su 8 "a2"; 
(* 105 *)  su 10 "a3"; 
(* 106 *)  su 9 "-(a3)"; 
(* 107 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 110 *)  su 9 "a3"; 
(* 111 *)  rwl []; pl 1; ThmCut "aid"; 
(* 114 *)  su 9 "a1"; 
(* 115 *)  gl 2; gr 1; Done(); 
(* 118 *)  rwl []; pl 1; ThmCut "aid"; 
(* 121 *)  su 9 "a2"; 
(* 122 *)  gl 3; gr 1; Done(); 
(* 125 *)  rwl []; gl 2; gr 1; Done(); 
(* 129 *)  NameSequent 1 "thm 3.1.i"; 
(* 130 *)  

(* 129

thm 3.1.i:



1:  Real(a1)

2:  Real(a2)

|-

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

*)



(* 130 *)  StartSequent ["Real(a1)","Real(0)"] ["a1*0 = 0"]; 
(* 131 *)  ThmCut "dist"; 
(* 132 *)  su 2 "a1"; 
(* 133 *)  su 3 "0"; 
(* 134 *)  su 4 "0"; 
(* 135 *)  ThmCut "aid"; 
(* 136 *)  su 4 "0"; 
(* 137 *)  gl 3; gr 1; Done(); 
(* 140 *)  rwl []; pl 1; ThmCut "aeq"; 
(* 143 *)  su 4 "a1*0"; 
(* 144 *)  su 5 "a1*0 + a1*0"; 
(* 145 *)  su 6 "-(a1*0)"; 
(* 146 *)  l(); Done(); 
(* 148 *)  ThmCut "ainv"; 
(* 149 *)  su 6 "a1*0"; 
(* 150 *)  ThmCut "aas"; 
(* 151 *)  su 6 "a1*0"; 
(* 152 *)  su 8 "a1*0"; 
(* 153 *)  su 7 "-(a1*0)"; 
(* 154 *)  gl2 3; rwl []; pl 1; gl 2; gl2 5; gl 5; gl2 3; rwl []; pl 1; ThmCut "aid"; 
(* 164 *)  ThmCut "rtimes"; 
(* 165 *)  su 8 "a1"; 
(* 166 *)  su 9 "0"; 
(* 167 *)  su 7 "a1*0"; 
(* 168 *)  Done(); 
(* 169 *)  rwl []; pl 1; ThmCut "acom"; 
(* 172 *)  undo(); undo(); ThmCut "symm"; 
(* 175 *)  su 9 "0"; 
(* 176 *)  su 10 "a1*0"; 
(* 177 *)  l(); Done(); 
(* 179 *)  Done(); 
(* 180 *)  NameSequent 1 "thm 3.1.ii"; 
(* 181 *)  

(* 180

thm 3.1.ii:



1:  Real(0)

|-

1:  a1 * 0 = 0

*)



(* 181 *)  StartSequent [] ["-(a1)*a2 = -(a1*a2)"]; 
(* 182 *)  ThmCut "ainv"; 
(* 183 *)  su 3 "a1"; 
(* 184 *)  ThmCut "distr"; 
(* 185 *)  ThmCut "meq"; 
(* 186 *)  su 6 "a1+ -(a1)"; 
(* 187 *)  su 7 "0"; 
(* 188 *)  l(); gl 2; gr 1; Done(); 
(* 192 *)  su 8 "a2"; 
(* 193 *)  su 3 "a1"; 
(* 194 *)  su 5 "-(a1)"; 
(* 195 *)  su 4 "a2"; 
(* 196 *)  gl 2; gl2 3; rwl []; pl 1; ThmCut "mcom"; 
(* 201 *)  su 8 "0"; 
(* 202 *)  su 9 "a2"; 
(* 203 *)  rwl []; pl 1; ThmCut "thm 3.1.ii"; 
(* 206 *)  ThmCut "zero"; 
(* 207 *)  Done(); 
(* 208 *)  su 9 "a2"; 
(* 209 *)  rwl []; pl 1; pl 2; ThmCut "aeql"; 
(* 213 *)  su 9 "a1*a2 + -(a1)*a2"; 
(* 214 *)  su 11 "0"; 
(* 215 *)  l(); Done(); 
(* 217 *)  su 10 "-(a1*a2)"; 
(* 218 *)  ThmCut "acom"; 
(* 219 *)  su 10 "-(a1*a2)"; 
(* 220 *)  su 11 "a1*a2"; 
(* 221 *)  rwl []; crwl []; rwl [1]; crwl [1]; rwl [2]; undo(); undo(); ThmCut "aas"; 
(* 229 *)  su 11 "-(a1*a2)"; 
(* 230 *)  su 13 "a1*a2"; 
(* 231 *)  su 12 "-(a1)*a2"; 
(* 232 *)  ThmCut "symm"; 
(* 233 *)  su 12 "[-(a1 * a2) + a1 * a2] + -(a1) * a2"; 
(* 234 *)  su 13 "-(a1 * a2) + a1 * a2 + -(a1) * a2"; 
(* 235 *)  l(); Done(); 
(* 237 *)  pl 2; gl 4; gl2 3; rwl []; pl 1; gl 3; rwl []; pl 1; pl 2; ThmCut "aid"; 
(* 247 *)  ThmCut "rminus"; 
(* 248 *)  su 14 "a1*a2"; 
(* 249 *)  su 13 "-(a1*a2)"; 
(* 250 *)  Done(); 
(* 251 *)  rwl []; pl 1; ThmCut "ainv"; 
(* 254 *)  su 13 "a1*a2"; 
(* 255 *)  rwl []; pl 1; ThmCut "acom"; 
(* 258 *)  su 13 "0"; 
(* 259 *)  su 14 "-(a1) * a2"; 
(* 260 *)  rwl []; pl 1; ThmCut "aid"; 
(* 263 *)  ThmCut "rtimes"; 
(* 264 *)  su 15 "-(a1)"; 
(* 265 *)  su 16 "a2"; 
(* 266 *)  su 14 "-(a1) * a2"; 
(* 267 *)  Done(); 
(* 268 *)  rwl []; gl 2; gr 1; Done(); 
(* 272 *)  NameSequent 1 "thm 3.1.iii"; 
(* 273 *)  

(* 272

thm 3.1.iii:



|-

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

*)



(* 273 *)  StartSequent ["Real(a1)","Real(a2)"] ["-(a1)* -(a2) = a1*a2"]; 
(* 274 *)  ThmCut "ainv"; 
(* 275 *)  su 3 "a1"; 
(* 276 *)  ThmCut "meq"; 
(* 277 *)  su 3 "a1 + -(a1)"; 
(* 278 *)  su 4 "0"; 
(* 279 *)  l(); Done(); 
(* 281 *)  

(* 281 *)  StartSequent ["Real(a1)","Real(a2)"] ["-(a1)* -(a2) = a1*a2"]; 
(* 282 *)  ThmCut "ainv"; 
(* 283 *)  su 3 "a2"; 
(* 284 *)  ThmCut "meql"; 
(* 285 *)  su 3 "a2 + -(a2)"; 
(* 286 *)  su 5 "0"; 
(* 287 *)  l(); Done(); 
(* 289 *)  su 4 "-(a1)"; 
(* 290 *)  ThmCut "thm 3.1.ii"; 
(* 291 *)  ThmCut "zero"; 
(* 292 *)  Done(); 
(* 293 *)  su 4 "-(a1)"; 
(* 294 *)  rwl []; pl 1; pl 2; ThmCut "dist"; 
(* 298 *)  su 4 "-(a1)"; 
(* 299 *)  su 5 "a2"; 
(* 300 *)  su 6 "-(a2)"; 
(* 301 *)  gl2 4; rwl []; pl 1; ThmCut "aeql"; 
(* 305 *)  su 6 "-(a1) * a2 + -(a1) * -(a2)"; 
(* 306 *)  su 8 "0"; 
(* 307 *)  l(); Done(); 
(* 309 *)  su 7 "a1*a2"; 
(* 310 *)  pl 2; ThmCut "thm 3.1.iii"; 
(* 312 *)  su 7 "a1"; 
(* 313 *)  su 8 "a2"; 
(* 314 *)  gl2 4; rwl []; pl 1; ThmCut "ainv"; 
(* 318 *)  su 8 "a1*a2"; 
(* 319 *)  rwl []; ThmCut "aas"; 
(* 321 *)  su 8 "a1*a2"; 
(* 322 *)  su 10 "-(a1 * a2)"; 
(* 323 *)  su 9 "-(a1) * -(a2)"; 
(* 324 *)  ThmCut "symm"; 
(* 325 *)  gl 2; gl2 3; rwl []; su 9 "[a1 * a2 + -(a1 * a2)] + -(a1) * -(a2)"; 
(* 329 *)  su 10 "a1 * a2 + -(a1 * a2) + -(a1) * -(a2)"; 
(* 330 *)  gl 5; l(); gl 2; gr 1; Done(); 
(* 335 *)  gl2 4; rwl []; pl 1; pl 5; gl 4; rwl []; pl 1; ThmCut "aid"; 
(* 343 *)  ThmCut "rtimes"; 
(* 344 *)  su 11 "a1"; 
(* 345 *)  su 12 "a2"; 
(* 346 *)  su 10 "a1 * a2"; 
(* 347 *)  Done(); 
(* 348 *)  rwl []; pl 1; ThmCut "acom"; 
(* 351 *)  su 12 "0"; 
(* 352 *)  su 13 "-(a1) * -(a2)"; 
(* 353 *)  rwl []; pl 1; ThmCut "aid"; 
(* 356 *)  ThmCut "rtimes"; 
(* 357 *)  su 14 "-(a1)"; 
(* 358 *)  su 15 "-(a2)"; 
(* 359 *)  su 13 "-(a1) * -(a2)"; 
(* 360 *)  Done(); 
(* 361 *)  rwl []; gl 2; gr 1; Done(); 
(* 365 *)  NameSequent 1 "thm 3.1.iv"; 
(* 366 *)  

(* 365

thm 3.1.iv:



|-

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

*)



(* 366 *)  StartSequent ["Real(a1)","Real(a2)","Real(a3)","a1*a3=a2*a3","~(a3 eq 0)"] ["a1=a2"]; 
(* 367 *)  ThmCut "meq"; 
(* 368 *)  su 4 "a1 * a3"; 
(* 369 *)  su 5 "a2 * a3"; 
(* 370 *)  l(); gl 4; gr 1; Done(); 
(* 374 *)  su 6 "/(a3)"; 
(* 375 *)  ThmCut "mas"; 
(* 376 *)  su 6 "a1"; 
(* 377 *)  su 8 "a3"; 
(* 378 *)  su 7 "/(a3)"; 
(* 379 *)  rwl []; pl 1; ThmCut "mas"; 
(* 382 *)  su 7 "a2"; 
(* 383 *)  su 9 "a3"; 
(* 384 *)  su 10 "/(a3)"; 
(* 385 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 388 *)  su 9 "a3 * /(a3)"; 
(* 389 *)  rwl []; ThmCut "mcom"; 
(* 391 *)  su 9 "a3 * /(a3)"; 
(* 392 *)  pl 2; gl 7; rwl []; pl 1; ThmCut "mid"; 
(* 397 *)  ThmCut "minv"; 
(* 398 *)  su 9 "a3"; 
(* 399 *)  l(); gl 6; gr 1; Done(); 
(* 403 *)  rwl []; pl 1; su 8 "a1"; 
(* 406 *)  gl 2; gr 1; Done(); 
(* 409 *)  undo(); undo(); Done(); 
(* 412 *)  undo(); 

(* 412

something weird happens here when I use Done()*)


(* Sequent snapshot:


1:  Real(a1)

2:  Real(a2)

3:  Real(a3)

4:  a1 * a3 = a2 * a3

5:  ~a3 eq 0

6:  1 * a1 = 1 * a2

|-

1:  Real(a1)

2:  a1 = a2


*)

Done(); 
(* 414 *)  

(* 413

I lose 1*a1=1*a2 and get [a3 * /(a3)] * a1 = [a3 * /(a3)] * a2, which should have been gone from a couple of steps ago.*)


(* Sequent snapshot:


1:  a1 * 1 = a1

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

3:  Real(a1)

4:  Real(a2)

5:  Real(a3)

6:  a1 * a3 = a2 * a3

7:  ~a3 eq 0

|-

1:  a1 = a2


*)



(* 413

I'll scroll backward now...*)


(* Sequent snapshot:


1:  a1 * 1 = a1

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

3:  Real(a1)

4:  Real(a2)

5:  Real(a3)

6:  a1 * a3 = a2 * a3

7:  ~a3 eq 0

|-

1:  a1 = a2


*)

undo(); undo(); ThmCut "mcom"; 
(* 417 *)  su 8 "1"; 
(* 418 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 421 *)  su 9 "1"; 
(* 422 *)  rwl []; pl 1; gl 2; gr 1; Done(); 
(* 427 *)  undo(); undo(); undo(); pl 1; undo(); pr 1; ThmCut "mid"; 
(* 434 *)  su 10 "a1"; 
(* 435 *)  gl 2; gr 1; Done(); 
(* 438 *)  rwl []; pl 1; ThmCut "mid"; 
(* 441 *)  su 10 "a2"; 
(* 442 *)  gl 3; gr 1; Done(); 
(* 445 *)  rwl []; gl 2; gr 1; Done(); 
(* 449 *)  

(* 448

this is very weird.  I just proved this.  I shouldn't have to do it again.  There shouldn't have been any branching in this proof!!!*)


(* Sequent snapshot:


1:  a1 * 1 = a1

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

3:  Real(a1)

4:  Real(a2)

5:  Real(a3)

6:  a1 * a3 = a2 * a3

7:  ~a3 eq 0

|-

1:  a1 = a2


*)

ThmCut "minv"; 
(* 450 *)  su 10 "a3"; 
(* 451 *)  l(); gl 7; gr 1; Done(); 
(* 455 *)  gl2 3; rwl []; pl 1; ThmCut "mid"; 
(* 459 *)  undo(); undo(); ThmCut "mcom"; 
(* 462 *)  su 10 "1"; 
(* 463 *)  rwl []; pl 1; ThmCut "mcom"; 
(* 466 *)  su 11 "1"; 
(* 467 *)  rwl []; pl 1; gl 7; rwl []; pl 1; ThmCut "mid"; 
(* 473 *)  su 12 "a2"; 
(* 474 *)  gl 3; gr 1; Done(); 
(* 477 *)  rwl []; gl 2; gr 1; Done(); 
(* 481 *)  NameSequent 1 "3.1.v"; 
(* 482 *)  

(* 481

3.1.v:



1:  Real(a1)

2:  Real(a2)

3:  a1 * a3 = a2 * a3

4:  ~a3 eq 0

|-

1:  a1 = a2

*)