(* 1 *)  Declarefunction "An" [0,1]; 
(* 2 *)  

(* 2 *)  Axiom "AN" ["a2 E a1"] ["An(a1) E a1"]; 
(* 3 *)  

(* 2

AN:



1:  a2 E a1

|-

1:  An(a1) E a1

*)


(* Sequent snapshot:


|-


*)



(* 3 *)  Declarepredicate "Real" [0]; 
(* 4 *)  

(* 4 *)  Declarefunction "0" [0]; 
(* 5 *)  

(* 5 *)  Declarefunction "1" [0]; 
(* 6 *)  

(* 6 *)  Declarefunction "+" [0,0,0]; 
(* 7 *)  

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

(* 9 *)  Declarepredicate "<" [0,0]; 
(* 10 *)  

(* 10 *)  Declarefunction "Minus" [0,0]; 
(* 11 *)  

(* 11 *)  Declarefunction "Inv" [0,0]; 
(* 12 *)  

(* 12 *)  Declarefunction "Sup" [0,1]; 
(* 13 *)  

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

(* 13

RPLUS:



|-

1:  Real(a1 + a2)

*)


(* Sequent snapshot:


|-


*)



(* 14 *)  Axiom "RTIMES" [] ["Real(a1*a2)"]; 
(* 15 *)  

(* 14

RTIMES:



|-

1:  Real(a1 * a2)

*)


(* Sequent snapshot:


|-


*)



(* 15 *)  Axiom "RMINUS" [] ["Real(Minus(a1))"]; 
(* 16 *)  

(* 15

RMINUS:



|-

1:  Real(Minus(a1))

*)


(* Sequent snapshot:


|-


*)



(* 16 *)  Axiom "RINV" [] ["Real(Inv(a1))"]; 
(* 17 *)  

(* 16

RINV:



|-

1:  Real(Inv(a1))

*)


(* Sequent snapshot:


|-


*)



(* 17 *)  Axiom "RSUP" [] ["Real(Sup(a1))"]; 
(* 18 *)  

(* 17

RSUP:



|-

1:  Real(Sup(a1))

*)


(* Sequent snapshot:


|-


*)



(* 18 *)  Axiom "CPLUS" [] ["a1+a2=a2+a1"]; 
(* 19 *)  

(* 18

CPLUS:



|-

1:  a1 + a2 = a2 + a1

*)


(* Sequent snapshot:


|-


*)



(* 19 *)  Axiom "CTIMES" [] ["a1*a2=a2*a1"]; 
(* 20 *)  

(* 19

CTIMES:



|-

1:  a1 * a2 = a2 * a1

*)


(* Sequent snapshot:


|-


*)



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

(* 20

APLUS:



|-

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

*)


(* Sequent snapshot:


|-


*)



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

(* 21

ATIMES:



|-

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

*)


(* Sequent snapshot:


|-


*)



(* 22 *)  Axiom "DIST" [] ["a1*[a2+a3]=a1*a2+a1*a3"]; 
(* 23 *)  

(* 22

DIST:



|-

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

*)


(* Sequent snapshot:


|-


*)



(* 23 *)  Axiom "IPLUS" [] ["Real(a1)->a1+0=a1"]; 
(* 24 *)  

(* 23

IPLUS:



|-

1:  Real(a1) -> a1 + 0 = a1

*)


(* Sequent snapshot:


|-


*)



(* 24 *)  Axiom "ITIMES" [] ["Real(a1)-> a1*1=a1"]; 
(* 25 *)  

(* 24

ITIMES:



|-

1:  Real(a1) -> a1 * 1 = a1

*)


(* Sequent snapshot:


|-


*)



(* 25 *)  Definepredicate 2 "Equal" "x1 Equal x2" "x1+0=x2+0"; 
(* 26 *)  

(* 26 *)  Axiom "MINUS" [] ["a1+Minus(a1)=0"]; 
(* 27 *)  

(* 26

MINUS:



|-

1:  a1 + Minus(a1) = 0

*)


(* Sequent snapshot:


|-


*)



(* 27 *)  Axiom "INV" [] ["a1 Equal 0 v a1*Inv(a1)=1"]; 
(* 28 *)  

(* 27

INV:



|-

1:  a1 Equal 0 v a1 * Inv(a1) = 1

*)


(* Sequent snapshot:


|-


*)



(* 28 *)  Axiom "NONTRIV" [] ["~0 Equal 1"]; 
(* 29 *)  

(* 28

NONTRIV:



|-

1:  ~0 Equal 1

*)


(* Sequent snapshot:


|-


*)



(* 29 *)  Axiom "IRR" [] ["~a1 < a1"]; 
(* 30 *)  

(* 29

IRR:



|-

1:  ~a1 < a1

*)


(* Sequent snapshot:


|-


*)



(* 30 *)  Axiom "TRI" [] ["a1 Equal a2 v a1 < a2 v a2<a1"]; 
(* 31 *)  

(* 30

TRI:



|-

1:  a1 Equal a2 v a1 < a2 v a2 < a1

*)


(* Sequent snapshot:


|-


*)



(* 31 *)  Axiom "TRANS" [] ["a1 < a2 & a2 < a3 -> a1 < a3"]; 
(* 32 *)  

(* 31

TRANS:



|-

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

*)


(* Sequent snapshot:


|-


*)



(* 32 *)  Axiom "MPLUS0" [] ["a1<a2==a1+a3<a2+a3"]; 
(* 33 *)  

(* 32

MPLUS0:



|-

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

*)


(* Sequent snapshot:


|-


*)



(* 33 *)  StartSequent [] ["a1<a2 -> a1+a3<a2+a3"]; 
(* 34 *)  ThmCut "MPLUS0"; 
(* 35 *)  l(); Done(); 
(* 37 *)  NameSequent 1 "MPLUS"; 
(* 38 *)  

(* 37

MPLUS:



|-

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

*)



(* 38 *)  Axiom "MTIMES" [] ["0<a3 & a1<a2 -> a1*a3<a2*a3"]; 
(* 39 *)  

(* 38

MTIMES:



|-

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

*)



(* 39 *)  Definepredicate 2 "<=" "x1<=x2" "x1 Equal x2 v x1 < x2"; 
(* 40 *)  

(* 40 *)  Axiom "SUP1" [] ["(Ex1.x1 E a1) & (Ax1.x1Ea1->x1 <= a2)-> Sup(a1) <= a2"]; 
(* 41 *)  

(* 40

SUP1:



|-

1:  (Ex1.x1 E a1)
      & (Ax1.x1 E a1 -> x1 <= a2)
      -> Sup(a1) <= a2

*)



(* 41 *)  Axiom "SUP2" [] ["(Ax1.x1Ea1->x1 <= a2) -> (Ax1.x1Ea1->x1 <= Sup(a1))"]; 
(* 42 *)  

(* 41

SUP2:



|-

1:  (Ax1.x1 E a1 -> x1 <= a2) -> (Ax1.
     x1 E a1 -> x1 <= Sup(a1))

*)



(* 42 *)  StartSequent [] ["Real(a1)&Real(a2)->(a1+a2=a1==a2=0)"]; 
(* 43 *)  r(); r(); Cut "[a1+a2]+Minus(a1)=a1+Minus(a1)"; 
(* 46 *)  gl 2; l(); gl 3; rwr 1; r(); ThmCut "CPLUS"; 
(* 52 *)  rwl 2; gl 4; l(); gl 4; ThmCut "APLUS"; 
(* 57 *)  rwl 1; ThmCut "MINUS"; 
(* 59 *)  gl2 3; rwl ~1; ThmCut "IPLUS"; 
(* 62 *)  l(); gl 5; gr 1; Done(); 
(* 66 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 71 *)  rwr 1; gl 2; l(); ThmCut "IPLUS"; 
(* 75 *)  l(); Done(); 
(* 77 *)  Done(); 
(* 78 *)  NameSequent 1 "NULLADD"; 
(* 79 *)  

(* 78

NULLADD:



|-

1:  Real(a1) & Real(a2) -> (
     a1 + a2 = a1 == a2 = 0)

*)



(* 79 *)  StartSequent ["Real(a1)"] ["a1+0=a1"]; 
(* 80 *)  ThmCut "IPLUS"; 
(* 81 *)  l(); Done(); 
(* 83 *)  Done(); 
(* 84 *)  NameSequent 1 "IPLUSa"; 
(* 85 *)  

(* 84

IPLUSa:



1:  Real(a1)

|-

1:  a1 + 0 = a1

*)



(* 85 *)  StartSequent [] ["a1=a1"]; 
(* 86 *)  r(); NameSequent 1 "TRIV"; 
(* 88 *)  

(* 87

TRIV:



|-

1:  a1 = a1

*)



(* 88 *)  StartSequent ["P1","P1->P2"] ["P2"]; 
(* 89 *)  gl 2; l(); Done(); 
(* 92 *)  Done(); 
(* 93 *)  NameSequent 1 "MP"; 
(* 94 *)  

(* 93

MP:



1:  P1 -> P2

2:  P1

|-

1:  P2

*)



(* 94 *)  StartSequent [] ["Real(0)"]; 
(* 95 *)  ThmCut "MINUS"; 
(* 96 *)  crwr 1; UseThm "RPLUS" [] [1]; 
(* 98 *)  NameSequent 1 "RZERO"; 
(* 99 *)  

(* 98

RZERO:



|-

1:  Real(0)

*)



(* 99 *)  StartSequent [] ["a1*0=0"]; 
(* 100 *)  Cut "a1*0+a1*0 = a1*0"; 
(* 101 *)  ThmCut "DIST"; 
(* 102 *)  crwr 1; ThmCut "IPLUSa"; 
(* 104 *)  NextGoal(); 
(* 105 *)  NextGoal(); 
(* 106 *)  rwr 1; r(); UseThm "RZERO" [] [1]; 
(* 109 *)  ThmCut "NULLADD"; 
(* 110 *)  l(); NextGoal(); 
(* 112 *)  l(); l(); gl 2; gr 1; Done(); 
(* 117 *)  Done(); 
(* 118 *)  r(); UseThm "RTIMES" [] [1]; 
(* 120 *)  UseThm "RTIMES" [] [1]; 
(* 121 *)  NameSequent 1 "MZERO"; 
(* 122 *)  

(* 121

MZERO:



|-

1:  a1 * 0 = 0

*)



(* 122 *)  StartSequent ["a1=a2"] ["a1+a3=a2+a3"]; 
(* 123 *)  rwr 1; r(); NameSequent 1 "BOTHSIDESPLUS"; 
(* 126 *)  

(* 125

BOTHSIDESPLUS:



1:  a1 = a2

|-

1:  a1 + a3 = a2 + a3

*)



(* 126 *)  StartSequent ["Real(a2)","a1+a2=0"] ["a2=Minus(a1)"]; 
(* 127 *)  ThmCut "BOTHSIDESPLUS"; 
(* 128 *)  gl 2; gr 1; Done(); 
(* 131 *)  w 1 "Minus(a1)"; 
(* 132 *)  ThmCut "CPLUS"; 
(* 133 *)  rwl 2; ThmCut "APLUS"; 
(* 135 *)  gl2 3; rwl 1; ThmCut "MINUS"; 
(* 138 *)  gl2 3; rwl 1; ThmCut "CPLUS"; 
(* 141 *)  gl2 3; rwl 2; ThmCut "IPLUSa"; 
(* 144 *)  gl 3; gr 1; Done(); 
(* 147 *)  gl2 3; rwl 1; ThmCut "IPLUSa"; 
(* 150 *)  NextGoal(); 
(* 151 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 156 *)  UseThm "RMINUS" [] [1]; 
(* 157 *)  NameSequent 1 "UINV"; 
(* 158 *)  

(* 157

UINV:



1:  Real(a2)

2:  a1 + a2 = 0

|-

1:  a2 = Minus(a1)

*)



(* 158 *)  StartSequent ["Real(a1)"] ["0+a1=a1"]; 
(* 159 *)  ThmCut "IPLUSa"; 
(* 160 *)  Done(); 
(* 161 *)  crwr 2; UseThm "CPLUS" [] [1]; 
(* 163 *)  NameSequent 1 "IPLUSb"; 
(* 164 *)  

(* 163

IPLUSb:



1:  Real(a1)

|-

1:  0 + a1 = a1

*)



(* 164 *)  StartSequent [] ["Minus(a1)+a1=0"]; 
(* 165 *)  ThmCut "CPLUS"; 
(* 166 *)  rwr 1; UseThm "MINUS" [] [1]; 
(* 168 *)  NameSequent 1 "MINUS2"; 
(* 169 *)  

(* 168

MINUS2:



|-

1:  Minus(a1) + a1 = 0

*)



(* 169 *)  StartSequent [] ["a1 < a2 == Minus(a2) < Minus(a1)"]; 
(* 170 *)  r(); ThmCut "MPLUS"; 
(* 172 *)  l(); Done(); 
(* 174 *)  w 1 "Minus(a1)+Minus(a2)"; 
(* 175 *)  ThmCut "APLUS"; 
(* 176 *)  crwl 1; gl 2; ThmCut "MINUS"; 
(* 179 *)  rwl 1; ThmCut "IPLUSb"; 
(* 181 *)  w 1 "Minus(a2)"; 
(* 182 *)  UseThm "RMINUS" [] [1]; 
(* 183 *)  gl2 3; rwl 1; ThmCut "CPLUS"; 
(* 186 *)  gl2 3; rwl 1; ThmCut "APLUS"; 
(* 189 *)  gl2 3; rwl 1; ThmCut "MINUS2"; 
(* 192 *)  gl2 3; rwl 1; ThmCut "IPLUSa"; 
(* 195 *)  w 1 "Minus(a1)"; 
(* 196 *)  UseThm "RMINUS" [] [1]; 
(* 197 *)  gl2 3; rwl 1; gl 2; gr 1; Done(); 
(* 202 *)  ThmCut "MPLUS"; 
(* 203 *)  l(); Done(); 
(* 205 *)  w 1 "a1+a2"; 
(* 206 *)  ThmCut "CPLUS"; 
(* 207 *)  rwl 1; undo(); undo(); undo(); rwl 2; undo(); undo(); rwl 1; undo(); undo(); undo(); undo(); rwl 4; undo(); undo(); undo(); rwl 1; gl 2; ThmCut "APLUS"; 
(* 226 *)  rwl 1; ThmCut "MINUS"; 
(* 228 *)  gl2 3; rwl 1; ThmCut "APLUS"; 
(* 231 *)  crwl 1; undo(); gl2 3; crwl 1; ThmCut "MINUS2"; 
(* 236 *)  gl2 3; rwl 1; ThmCut "CPLUS"; 
(* 239 *)  gl2 3; rwl 2; ThmCut "MPLUS0"; 
(* 242 *)  l(); gl 2; l(); gl 2; gr 1; Done(); 
(* 248 *)  Done(); 
(* 249 *)  NameSequent 1 "MINUSLESS"; 
(* 250 *)  

(* 249

MINUSLESS:



|-

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

*)



(* 250 *)  StartSequent ["a1<0"] ["0<Minus(a1)"]; 
(* 251 *)  ThmCut "MPLUS"; 
(* 252 *)  l(); Done(); 
(* 254 *)  w 1 "Minus(a1)"; 
(* 255 *)  ThmCut "MINUS"; 
(* 256 *)  rwl 1; gl 2; ThmCut "IPLUSb"; 
(* 259 *)  w 1 "Minus(a1)"; 
(* 260 *)  UseThm "RMINUS" [] [1]; 
(* 261 *)  rwl 1; gl 2; gr 1; Done(); 
(* 265 *)  NameSequent 1 "NEGINEQ"; 
(* 266 *)  

(* 265

NEGINEQ:



1:  a1 < 0

|-

1:  0 < Minus(a1)

*)



(* 266 *)  StartSequent [] ["a1*Minus(a2)=Minus(a1*a2)"]; 
(* 267 *)  ThmCut "TRIV"; 
(* 268 *)  w 1 "a1*Minus(a2)"; 
(* 269 *)  ThmCut "BOTHSIDESPLUS"; 
(* 270 *)  Done(); 
(* 271 *)  w 1 "a1*a2+Minus(a1*a2)"; 
(* 272 *)  ThmCut "MINUS"; 
(* 273 *)  rwl 1; ThmCut "IPLUSa"; 
(* 275 *)  w 1 "a1*Minus(a2)"; 
(* 276 *)  UseThm "RTIMES" [] [1]; 
(* 277 *)  gl2 3; rwl 1; gl 2; ThmCut "APLUS"; 
(* 281 *)  crwl 1; gl 2; ThmCut "DIST"; 
(* 284 *)  crwl 1; ThmCut "MINUS2"; 
(* 286 *)  gl2 3; rwl 1; ThmCut "MZERO"; 
(* 289 *)  gl2 3; rwl 1; gl 2; ThmCut "IPLUSb"; 
(* 293 *)  w 1 "Minus(a1*a2)"; 
(* 294 *)  UseThm "RMINUS" [] [1]; 
(* 295 *)  rwl 1; gl 2; gr 1; Done(); 
(* 299 *)  NameSequent 1 "NEGCOMM"; 
(* 300 *)  

(* 299

NEGCOMM:



|-

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

*)