% original version at http://www.ii.uib.no/~bezem/GL/dpe.in
% DP(r) => DP(re), i.e., 
% the diamond property is preserved under reflexive closure

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

:- dynamic(e/2).
:- dynamic(r/2).
:- dynamic(re/2).
:- dynamic(dom/1).
:- dynamic(answer/1).

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

% domain elements a,b,c
dom(a). dom(b). dom(c).

[assumption]             := true => re(a,b),re(a,c).
[goal_axiom,X]           := re(b,X),re(c,X) => answer((re(b,X),re(c,X))).
[]                       := answer(_) => goal.

% equality axioms
[reflexivity_of_e,X]     := dom(X) => e(X,X).
[symmetry_of_e,X,Y]      := e(X,Y) => e(Y,X).
[left_congr_of_e,X,Y,Z]  := e(X,Y),re(Y,Z) => re(X,Z).

% basic facts on re
[re_contains_e,X,Y]      := e(X,Y) => re(X,Y).
[re_contains_r,X,Y]      := r(X,Y) => re(X,Y).
[re_elimination,X,Y]     := re(X,Y) => e(X,Y);r(X,Y).

% DP
[diam_prop_of_r,X,Y,Z]   := r(X,Y),r(X,Z) => dom(U),r(Y,U),r(Z,U).