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