/* Set( derivation, hyperres ). */





refl(T,P) ==  all(X,T*X => P*p(X,X)).
trans(P) == all(X,all(Y,all(Z, P*p(X,Y) and P*p(Y,Z) => P*p(X,Z)))).
(equiv(P)*p(X,Y)) == ( P*p(X,Y) and P*p(Y, X) ). 



(pairs(T)*P) == exists(X,exists(Y,T*X and T*Y and P=p(X,Y))).


binrel(T,R) == (R*p(X,Y) => T*X and T*Y).

binrel(t,ord1).
refl(t,ord1).
trans(ord1).

binrel(t,ord2).
refl(t,ord2).
trans(ord2).

(ord*p(p(A1, B1), p(A2, B2))) == 
	(   
	   ( ord1*p(A1, A2) and ~(equiv(ord1)*p(A1, A2) )) or 
	   ( equiv(ord1)*p(A1, A2) and ord2*p(B1, B2)  )  
	). 


/*
equiv ==

	all( A1, all(B1, all(A2, all(B2,
          (
	   (  ord( p(A1, B1), p(A2, B2) ) and 
	      ord( p(A2, B2), p(A1, B1) )  )  ==
	      ( equiv2(B1, B2 ) and equiv1( A1, A2 ) )  
          ))))).

*/

top_predicates_precedence([trans,refl,equiv,binrel,pairs]).
precedence([ord,ord1,ord2,*,p,t]).

:-option(structural_expansion(on)).




goal refl(pairs(t),ord) -> [].