%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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^.

 N = 1^ ;0.
 F+N = 1^.
 all x (x<=F & x<=N -> x=0).
 1<=F.
 F;F<=F. 
end_of_list.

formulas(sos). 
  %preconditions
  F<=(l1+l2+i)*.
end_of_list.

formulas(goals).
  F;l1 <= (l1+l2+i)*;(l1+l2+i).
end_of_list.