%-------------------------------------------------------------------

set(auto).

assign(max_seconds,32700).

%-----------------------AXIOMS ON ORDERED GROUPS--------------------
%-------------------------------------------------------------------

formula_list(usable).

% abelian group axioms (think that minuz(X,Y)=pluz(X,rvz(Y)) by def.) 

all x y z ( pluz(pluz(x,y),z) = pluz(x,pluz(y,z))). % associativity

all x ( pluz(x,e) = x). % right unit

all x ( pluz(x,rvz(x)) = e). % right inverse

all x y ( pluz(x,y) = pluz(y,x) ). % commutativity

% ordering axioms (axioms concerning non-negativeness)

all x y ( (nneg(x) & nneg(y)) -> nneg(pluz(x,y)) ).

all x ( nneg(x) | nneg(rvz(x)) ).

all x ( (nneg(x) & nneg(rvz(x))) -> x=e ).

%-------------------------------------------------------------------

end_of_list.

%-----------------------DEFINITIONAL EXTENSIONS---------------------
%-------------------------------------------------------------------

formula_list(usable).

all x ( nneg(x) -> abs(x)=x ). % definition of the absolute value...

all x ( -(nneg(x)) -> abs(x)=rvz(x) ). % ...def.n of the absolute value

all x y ( leq(x,y) <-> nneg(pluz(y,rvz(x))) ). % def.n of comparison

%-------------------------------------------------------------------

end_of_list.

%-------------------------------------------------------------------

%-------------------------------------------------------------------


%-----------------------LEMMAS--------------------------------------
%-------------------------------------------------------------------

formula_list(usable). % laws concerning the relation "leq"
%% statements A1,Ba,Bb,B below proved without definitional extensions
( all x y z ( pluz(x,y)=pluz(x,z) -> y=z )). % A1: cancellation law
%%( all x y ( pluz(pluz(x,rvz(y)),pluz(y,rvz(x)))=e )). % Ba
%%( all x y ( pluz(pluz(x,rvz(y)),rvz(pluz(x,rvz(y))))=e )). % Bb
( all x y ( rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)) )). % B (from A1,Ba,Bb alone)
( all x y ( leq(x,y) | leq(y,x) )). % C: totality
( all x ( leq(x,x) ) ). % D: reflexivity
( all x y z ( (leq(x,y) & leq(y,z)) -> leq(x,z) )). % E: transitivity
( all x y z ( (leq(x,y) & x != y & leq(y,z)) -> x != z )). % E1: transitivity
( all x y z ( (leq(x,y) & leq(y,z) & y != z) -> x != z )). % E2: transitivity
( all x y z ( leq(x,y) -> leq(pluz(x,z),pluz(y,z)) )). % F: additivity
( all x y z ( pluz(x,z)=pluz(y,z) -> x=y )). % A2: cancellation law
( all x y z ( leq(x,y) & x != y ->  % F1, strict additivity
             pluz(x,z) != pluz(y,z) )).
end_of_list.

formula_list(usable). % laws concerning the operations "abs" and "nneg"
( all x ( abs(pluz(x,rvz(x)))=e )). %1
( all x ( leq(x,abs(x)) )). %2
( all x ( abs(abs(x))=abs(x) )). %3
( all x ( abs(x)=e <-> x=e )). %4
( all x ( abs(rvz(x))=abs(x) )). %5
( all x y ( leq(pluz(x,y),pluz(abs(x),abs(y))) )). %6
( all x y ( nneg(pluz(x,y)) -> leq(abs(pluz(x,y)),pluz(abs(x),abs(y))) )). %7a
( all x y ( -(nneg(pluz(x,y))) -> %7b
        nneg(pluz(rvz(x),rvz(y))) )).
( all x y ( -(nneg(pluz(x,y))) -> %7c (proved without earlier laws on "leq")
        leq(abs(pluz(rvz(x),rvz(y))),pluz(abs(rvz(x)),abs(rvz(y)))) )).
( all x y ( -(nneg(pluz(x,y))) -> %7d
        leq(abs(pluz(x,y)),pluz(abs(x),abs(y))) )). 
( all x y ( leq(abs(pluz(x,y)),pluz(abs(x),abs(y))) )). %7
( all x y z ( pluz(x,z)=pluz(pluz(x,rvz(y)),pluz(y,z)) )). %8a
( all x y z ( leq(abs(pluz(x,rvz(z))), %8 (proved without the axioms)
         pluz(abs(pluz(x,rvz(y))),abs(pluz(y,rvz(z))))) )).
( all x y ( -(nneg(x)) -> leq(x,abs(y)) & x != abs(y) )). %9
( all x y ( nneg(y) -> leq(pluz(x,rvz(y)),pluz(x,y)) )). %10
( all x y ( ( nneg(x) & -(nneg(y)) ) -> %11a
         leq(abs(pluz(abs(x),rvz(abs(y)))),abs(pluz(x,rvz(y)))) )).
( all x y ( ( nneg(x) & nneg(y) ) -> %11b
         abs(pluz(abs(x),rvz(abs(y))))=abs(pluz(x,rvz(y))) )).
( all x y ( ( -(nneg(x)) & -(nneg(y)) ) -> %11c
         abs(pluz(abs(rvz(x)),rvz(abs(rvz(y)))))=abs(pluz(rvz(x),y)) )). 
% to prove the next lemma, it turned out useful to temporarily inhibit:
% * all axioms save commutativity;
% * all definitional extensions;
% * all of the laws concerning "leq" save D (reflexivity) and B;
% * all of the laws concerning "abs" and "nneg" save 5 and 11a--11c
( all x y ( %11
         leq(abs(pluz(abs(x),rvz(abs(y)))),abs(pluz(x,rvz(y)))) )).
(all x y ( %12
         leq(pluz(abs(x),rvz(abs(pluz(abs(y),rvz(abs(x)))))),abs(y))
)).
end_of_list.

%-------------------------------------------------------------------