% Language Options op(500, infix, "\/"). op(500, infix, "/\"). op(300, postfix, "'"). op(450, infix, "*"). op(300, postfix, "^"). formulas(assumptions). % axioms of Boolean algebra %%%%%%%%%%%%%%%%%%%%%% %commutativity x \/ y = y \/ x. x /\ y = y /\ x. %associativity x \/ (y \/ z) = (x \/ y) \/ z. x /\ (y /\ z) = (x /\ y) /\ z. %absorpotion x \/ (y /\ x) = x. x /\ (y \/ x) = x. % ordering x <= y <-> x \/ y = y. x <= y <-> x /\ y = x. %distributivity x /\ (y \/ z) = (x /\ y) \/ (x /\ z). x \/ (y /\ z) = (x \/ y) /\ (x \/ z). %constants L = x \/ x'. O = x /\ x'. % composition %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% x * (y * z) = (x * y) * z. x * I = x. I * x = x. % Schroeder/Dedekind %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% x*y /\ z <= (x /\ z*y^) * (y /\ x^*z). x*y <= z <-> x^ * z' <= y'. x*y <= z <-> z' * y^ <= x'. % standard axioms for finite iteration (star) %%%%%%%%% %unfold laws I \/ x*rtc(x) = rtc(x). I \/ rtc(x)*x = rtc(x). %induction x*y \/ z <= y -> rtc(x)*z <= y. y*x \/ z <= y -> z*rtc(x) <= y. %aux lemma (proven before) x<=y -> x*z <= y*z. x<=y -> z*x <= z*y. %aux lemmas (proven before) %to get a suitable set of axioms (x \/ y)*z = x*z \/ y*z. z*(x \/ y) = z*x \/ z*y. (x * y)^ = y^ * x^. (x \/ y)^ = x^ \/ y^. (x /\ y)^ = x^ /\ y^. x<=y -> x*z<= y*z. x<=y -> z*x<= z*y. x<=y -> x\/z<= y\/z. x<=y -> x/\z<= y/\z. x^^=x. O<=x. x<=L. O*x=O. x*O=O. x<=y -> x*z <= y*z. x<=y -> z*x <= z*y. % point/atom point(x) <-> (x*L = x & L*x = L & x*x^ <= I). %special properties y*(L*y) <=y -> rtc(x \/ y) <= rtc(x) \/ rtc(x)*(y*rtc(x)). point(y) -> (R /\ y*L)*(L*(R /\ y*L)) <= (R /\ y*L). point(y) -> R /\ y*L = (y*y^)*R. % invariants %%%%%% Inv0(x,y) <-> x=rtc(R /\ y*L). Inv1(y) <-> y = y*L. end_of_list. formulas(goals). Inv0(x,y) & point(p ) & p<=R*L /\ y' -> Inv0(x \/ x*(((p*p^)*R)*x) , y \/ p). % end_of_list.