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