%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Prover9/Mace4 Code                                  %
%                                                     %
%                                                     %
% This file includes                                  %
%   - the standard axioms for left omega algebra      %
% and shows                                           %
%   - a lemma                                         %
%                                                     %
% (tested for PROGRAM_VERSION "April-2007)            %
% It can freely used under the                        %
% GNU GENERAL PUBLIC LICENSE Version 2.               %
%                                                     %
%                                                     %
%                                   (c)2007 P.Hoefner %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

op(500, infix_left, "+").  %choice
op(490, infix_left, ";").  %composition
op(480, postfix,    "*").  %finite iteration
op(450, postfix,    "^").  %infinite iteration (omega)

formulas(sos).
% standard axioms of i-semirings %%%%%%%%%%%%%%%%%%%%%%
  %commutative additive monoid
    x+y = y+x.
    x+0 = x.
    x+(y+z) = (x+y)+z.
  %multiplicative monoid
%    x;1 = x & 1;x = x.
    x;(y;z) = (x;y);z.
  %annihiltion laws
    0;x = 0.
  %idempotency
%    x+x = x.
  %distributivty
    (x+y);z = x;z+y;z.
  %isotony
    x<=y -> z;x<= z;y.
  %additional inequality-axioms
    x <= x.
    x<=y & y<=z -> x<=z.
    x<=y -> x+z<=y+z. 
    x<=y -> z+x<=z+y. 
    x<=y -> x;z<=y;z.
  %supremum property (proved)
    x+y<=z <-> x<=z & y<=z.
% standard axioms for finite iteration (star) %%%%%%%%%
%    1+x;x* = x*.
%    x;y+z<=y -> x*;z<=y.
  %isotonicity (proved)
%    x<=y -> x*<=y*.
  %unfold
    x;x^ = x^.
  %co-induction
%    y<=x;y+z -> y<=x^+x*;z.
   %simple Induction
    y<=x;y -> y<=x^.
  %isotonicity (proved)
    x<=y -> x^<=y^.
end_of_list.

formulas(sos). 
  all p (p;p=p & p<=1 -> p;(p;x)^=(p;x)^).
  all p (p;p=p & p<=1 -> (p;x)^=(p;x;p)^).
  all p (p;p=p & p<=1 -> (p;x)^<=(x;p)^).
  x<=1 ->  y;x;z<= y;z.
  x<=1 ->  x;z<= y;z.
  x<=1 ->  y;x<= y;x.

%% arithmetics
  a10 =a5;a5.
  a15 =a5;a5;a5.
  a20 =a5;a5;a5;a5.
  a25 =a5;a5;a5;a5;a5.
  a30 =a5;a5;a5;a5;a5;a5.

%%Preconditions
  atu<=1. %& atu;atu=atu.
  atd<=1. %& atd;atd=atd.
  atb<=1. %& atb;atb=atb.  
end_of_list.

formulas(goals).
  (atu;a5;atd;a10;atb;a15)^ <= (a30;atu)^.
  (atu;a5;atd;a10;atb;a15)^ <= (a30;atd)^.
  (atu;a5;atd;a10;atb;a15)^ <= (a30;atb)^.
end_of_list.