:: HIDDEN semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
mode set -> set ;
end;

definition
let x, y be set ;
pred x = y;
reflexivity
errorfrm ;
symmetry
errorfrm ;
end;

notation
end;

definition
let x, X be set ;
pred x in X;
asymmetry
errorfrm ;
end;