(* 1 *)  StartSequent [] ["Real(0)"]; 
(* 2 *)  ThmCut "ainv"; 
(* 3 *)  crwr []; 

(* 3

nontriv:



|-

1:  ~0 eq 1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

rplus:



|-

1:  Real(a1 + a2)

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

rtimes:



|-

1:  Real(a1 * a2)

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

rminus:



|-

1:  Real(-(a1))

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

rinv:



|-

1:  Real(/(a1))

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

acom:



|-

1:  a1 + a2 = a2 + a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

aas:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

aid:



1:  Real(a1)

|-

1:  a1 + 0 = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

ainv:



|-

1:  a1 + -(a1) = 0

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

mas:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

mcom:



|-

1:  a1 * a2 = a2 * a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

mid:



1:  Real(a1)

|-

1:  a1 * 1 = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

minv:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

dist:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

totorder:



|-

1:  a1 <= a2 v a2 <= a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

eqbyord:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

ordtrans:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

ordadd:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

ordaddl:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

ordmult:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

reflx:



|-

1:  a1 = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

symm:



|-

1:  a1 = a2 -> a2 = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

trans:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

negeqsymm:



1:  ~a1 eq a2

|-

1:  ~a2 eq a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

zero:



|-

1:  Real(0)

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

one:



|-

1:  Real(1)

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

aeq:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

aeql:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

meq:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

meql:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

distr:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.i:



1:  Real(a1)

2:  Real(a2)

|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.ii:



1:  Real(0)

|-

1:  a1 * 0 = 0

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.iii:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.iv:



|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.v:



1:  Real(a1)

2:  Real(a2)

3:  a1 * a3 = a2 * a3

4:  ~a3 eq 0

|-

1:  a1 = a2

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.1.vi:



1:  Real(a1)

2:  a1 * a2 = 0

3:  ~a2 eq 0

|-

1:  a1 = 0 v a2 = 0

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.2.i:



1:  a1 <= a2

|-

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

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

zeros:



|-

1:  -(0) = 0

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

2neg:



1:  Real(a1)

|-

1:  -(-(a1)) = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.2.ii:



1:  a1 <= a2

2:  a3 <= 0

|-

1:  a2 * a3 <= a1 * a3

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.2.iii:



1:  0 <= a1

2:  0 <= a2

|-

1:  0 <= a1 * a2

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.2.iv:



|-

1:  0 <= a1 * a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

eqsymm:



1:  a1 eq a2

|-

1:  a2 eq a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

req:



1:  a1 eq a2

2:  Real(a1)

3:  Real(a2)

|-

1:  a1 = a2

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

lemma 1.1:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  ~/(a1) eq 0

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

thm 3.2.v:



1:  Real(1)

2:  ~0 eq 1

|-

1:  0 < 1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

lemma 1.2:



1:  Real(a1)

2:  ~a1 eq 0

|-

1:  /(/(a1)) = a1

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)



(* 3

3.2.vi:



1:  0 < a1

2:  ~0 eq 1

3:  Real(a1)

4:  Real(1)

5:  Real(0)

|-

1:  0 < /(a1)

*)


(* Sequent snapshot:


1:  U1 + -(U1) = 0

|-

1:  Real(U1 + -(U1))


*)

UseThm "rplus" [] [1]; 
(* 5 *)