% Problem 5 for lattices

use(lattice).

%not D
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(X,j(Y,Z)),j(m(X,Y),m(X,Z)))=m(X,j(Y,Z)).