%--------------------------------------------------------------------------
% File     : ElemRelns.ax
% Domain   : Basil Smith's Elementary Theory of Relations
% Problems : 
% Version  : 
% English  : 
% Refs     :  
% Source   : Definitions from Basil Smith's Elementary Theory of Relations (CAMELEON 08)
%            Formalization by C E Brown
% Names    : 
% Status   : 
% Rating   : 
% Syntax   : 
% Comments : 
%--------------------------------------------------------------------------

thf(cog,constant,(cog:$i>$i>$i>$o)).

thf(trans,definition,(trans:=(^[X:$i]: (![A:$i, B:$i, C:$i]: (((((cog @ A) @ X) @ B) & (((cog @ B) @ X) @ C)) => (((cog @ A) @ X) @ C)))))).

thf(sym,definition,(sym:=(^[X:$i]: (![A:$i, B:$i]: ((((cog @ A) @ X) @ B) => (((cog @ B) @ X) @ A)))))).

thf(antisym,definition,(antisym:=(^[X:$i]: (![A:$i, B:$i]: (((((cog @ A) @ X) @ B) & (((cog @ B) @ X) @ A)) => (A = B)))))).

thf(asym,definition,(asym:=(^[X:$i]: (![A:$i, B:$i]: ((((cog @ A) @ X) @ B) => (~ (((cog @ B) @ X) @ A))))))).

thf(refl,definition,(refl:=(^[X:$i]: (![A:$i, B:$i]: ((((cog @ A) @ X) @ B) => ((((cog @ A) @ X) @ A) & (((cog @ B) @ X) @ B))))))).

thf(op,definition,(op:=(^[X:$i]: (![A:$i, B:$i, C:$i, D:$i]: (((((cog @ A) @ X) @ B) & (((cog @ C) @ X) @ D)) => ((A = C) & (B = D))))))).

thf(sing,definition,(sing:=(^[X:$i]: (![A:$i, B:$i, C:$i, D:$i]: (((((cog @ A) @ X) @ B) & (((cog @ C) @ X) @ D)) => ((A = B) & (B = C))))))).

thf(prim,definition,(prim:=(^[X:$i]: (![A:$i, B:$i]: ((((cog @ A) @ X) @ B) => (~ (((cog @ A) @ X) @ B))))))).

thf(cls,definition,(cls:=(^[X:$i]: (![A:$i, B:$i, C:$i, D:$i]: (((((cog @ A) @ X) @ B) & (((cog @ C) @ X) @ D)) => (((cog @ B) @ X) @ C)))))).

thf(jec,definition,(jec:=(^[X:$i]: (![A:$i, B:$i, C:$i]: (((((cog @ A) @ X) @ B) & (((cog @ A) @ X) @ C)) => (B = C)))))).

thf(subeq,definition,(dsubeq:=(^[X:$i, Y:$i]: (![A:$i, B:$i]: ((((cog @ A) @ X) @ B) => (((cog @ A) @ Y) @ B)))))).