%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 lazy 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.
%annihilation laws
0;x = 0.
%idempotency
x+x = x.
%distributivity
(x+y);z = x;z+y;z.
%isotony
x+y=y -> z;x+z;y = z;y.
%standard axioms for finite iteration (star) %%%%%%%%%
%unfold laws
% 1+x;x* = x*.
%induction
% (x;y+z)+y=y -> x*;z+y=y.
%standard axioms for infinite iteration (omega) %%%%%%
%unfold laws
x;x^= x^.
%co-induction
% y+(x;y+z)=x;y+z -> y+(x^+x*;z)=x^+x*;z.
%simple Induction
y+(x;y)=x;y -> y+x^=x^.
end_of_list.
formulas(goals).
x;(y;x)^+(x;y)^=(x;y)^.
end_of_list.