DeclarePredicate "Real" [0];


Axiom "zero" [] ["Real(0)"];

DeclareFunction "+" [0,0,0];

DeclareFunction "*" [0,0,0];

DeclareFunction "-" [0,0];

setprecrightabove "*" "+";

DeclarePredicate "<=" [0,0];

DeclareFunction "/" [0,0];

DeclarePredicate "<" [0,0];


Axiom "one" [] ["Real(1)"];

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

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

Axiom "rminus" []["Real(-(a1))"];

Axiom "rinv" [] ["Real( /(a1))"];

Axiom "acom" [] ["a1+a2=a2+a1"];

Axiom "aas" [] ["[a1+a2]+a3=a1+a2+a3"];

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

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

DefineFunction 2 "--" "x1--x2" "x1+ -(x2)";

DefinePredicate 2 "eq" "x1 eq x2" "x1+0=x2+0";

Axiom "mas" [] ["[a1*a2]*a3=a1*a2*a3"];

Axiom "mcom" [] ["a1*a2=a2*a1"];

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

Axiom "minv" [] ["~(a1 eq 0)-> (a1* /(a1) = 1)"];

Axiom "dist" [] ["a1*[a2+a3]=a1*a2+a1*a3"];

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

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

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

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

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

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

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

(* The following are the proofs for the three properties *)
(*   of an Equality Relation *)

  StartSequent [] ["a1=a1"];
  r(); NameSequent 1 "reflx";

  StartSequent [] ["a1=a2 -> a2=a1"];
  r(); crwr []; ThmCut "reflx";
  su 3 "a1";
  Done();
  NameSequent 1 "symm";

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

(*The following are properties of equality for "+" and "*". *)

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

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

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

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

(* This is another version of the Distribution axiom *)

  StartSequent [] ["[a1+a2]*a3 = a1*a3 + a2*a3"];
  ThmCut "dist";
  su 4 "a3";
  su 5 "a1"; 
  su 6 "a2"; 
  ThmCut "mcom"; 
  su 6 "a3"; 
  su 7 "[a1+a2]"; 
  rwl []; pl 1; ThmCut "mcom"; 
  su 7 "a3"; 
  su 8 "a1"; 
  rwl []; pl 1; ThmCut "mcom"; 
  su 8 "a3"; 
  su 9 "a2"; 
  rwl []; gl 2; gr 1; Done(); 
  NameSequent 1 "distr";

(* End of Field Axioms file.  Ready to start proofs. *)