%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 -> z;x<= z;y. % standard axioms for finite iteration (star) %%%%%%%%% %unfold laws % 1+x;x* = x*. %induction % (x;y+z)<=y -> x*;z<=y. % standard axioms for infinite iteration (omega) %%%%%% %unfold laws % x;x^= x^. %Co-induction % y<=x;y+z -> y<=x^+x*;z. %simple Induction % y<=x;y -> y<=x^. %<= props x<=x. x<=y & y<=z -> x<=z. x<=y -> x;z <= y;z. x<=y -> x+z<=y+z. % x<=y -> x* <= y*. x<=y -> x^ <= y^. (x;y)^ <= (x+y)^. (x;y;z)^ <= (x+y+z)^. all p(p<=1 & p;p=p -> p;(p;x)^ = (p;x)^ ). % all p(p<=1 & p;p=p -> (p;x)^ = (p;x;p)^ ). x^<=(x+y)^. end_of_list. formulas(goals). all p all q all r (p<=1 & p;p=p & q<=1 & q;q=q & r<=1 & r;r=r -> (p;x;q;y;r;z)^ <= p;(p;x;q+q;y;r+r;z)^ ) & all p all q all r (p<=1 & p;p=p & q<=1 & q;q=q & r<=1 & r;r=r -> (p;x;q+q;y;r+r;z)^<=(p;x;q+q;x;p+q;y;r+r;y;q+r;z)^ ). end_of_list.