[defMonoid]. semiGroup(symm). %1 leftMonoid(circ,id). %2 commMonoid(int,u). %3 subseteq( circ( symm(P,Q), R ), un( circ(Q,R), circ(P,R) ) ). [ subseteq(P,Q) ] -> subseteq( circ(P,R), circ(Q,R) ). %4 %------- equiv( symm(int(P,symm(Q,R)),int(P,Q)), int(P,R) ). %------- % convolutory laws: equiv( rev(rev(P)), P ). equiv( rev(int(P,Q)), int(rev(Q),rev(P)) ). equiv( rev(circ(P,Q)), circ(rev(Q),rev(P)) ). %------- % Schroeder's cycle law: [ equiv( int( circ(P,Q), R ), z ) ] -> equiv( int( circ( rev(P), R), Q ), z ). %-------