%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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). all p(p+1=1 & p;p=p -> (p;x)^+(p;x;p)^=(p;x;p)^ ). end_of_list.