% Problem 8 for lattices (we don't get that at present)

use(lattice).

%not Da
goal m(x,j(y,z))=j(m(x,y),m(x,z)) -> [].

% Db
%j(X,m(Y,Z))=m(j(X,Y),j(X,Z)).

%8
goal m(m(j(X,Y),m(j(Y,Z),j(Z,X))),j(m(X,Y),j(m(Y,Z),m(Z,X))))=m(j(X,Y),m(j(Y,Z),j(Z,X))).



precedence([m,j,x,y,z]).
:-option(term_size_weight).


/*


*/