% original version at http://www.csupomona.edu/~jrfisher/www/geolog/latt_comm.in

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(lt/2).
:- dynamic(j/3).
:- dynamic(dom/1).
:- dynamic(answer/1).

flag(keywords).
flag(quiet).
flag(quick).

dom(x). dom(y). dom(z).

[assump] := true => j(x,y,z). 
[goal_ax,Z] := j(y,x,Z),lt(z,Z),lt(Z,z) => answer((j(y,x,Z),lt(z,Z),lt(Z,z))).           
[] := answer(_) => goal.

[lt_refl,X] := dom(X) => lt(X,X).
[lt_trans,X,Y,Z] := lt(X,Y),lt(Y,Z) => lt(X,Z).
[ub_join,X,Y,Z] := j(X,Y,Z) => lt(X,Z),lt(Y,Z).
[lub_join,X,Y,Z,U] := j(X,Y,Z),lt(X,U),lt(Y,U) => lt(Z,U).
[lt_j,X,Y] := lt(X,Y) => j(X,Y,Y).
[up_latt,X,Y] := dom(X),dom(Y) => dom(U),j(X,Y,U).