declarepredicate "Real" [0];

declarefunction "+" [0,0,0];

declarefunction "*" [0,0,0];

declarefunction "-" [0,0];

setprecrightabove "*" "+";

declarepredicate "<=" [0,0];

declarefunction "/" [0,0];

declarepredicate "<" [0,0];

Axiom "reflx" [] ["a1=a1"];

Axiom "symm" [] ["(a1=a2)->(a2=a1)"];

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

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 "aeq" [] ["(a1=a2)->(a1+a3=a2+a3)"];

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

Axiom "aid" [] ["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 "meq" [] ["(a1=a2)->(a1*a3=a2*a3)"];

Axiom "meql" [] ["(a1=a2)->(a3*a1=a3*a2)"];

Axiom "mid" [] ["a1*1=a1"];

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

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

Axiom "dstr" [] ["[a1+a2]*a3=a1*a3+a2*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))"];