logic CASL
spec LeftTotalRelation = 
sorts S, T
pred __R__ : S * T
pred __R : S

. forall s : S . exists t : T . s R t %(Ax1)%

. forall s : S . s R %(Ax1)%



logic CASL
spec RightUniqueRelation = 
sorts S, T
pred __R__ : S * T

. forall s : S, t1, t2 : T . s R t1 /\ s R t2 => t1 = t2 %(Ax_0)%

logic CASL
spec Function =
LeftTotalRelation and RightUniqueRelation