% transitivity: defFoAs(isTrans(P),subseteq(circ(P,P),P)). % symmetry: defFoAs(isSymm(P),is_rev(P)). % reflexivity: defFoAs(isRefl(P),subseteq(un(P,rev(P)),rA(int(id,P)))). % strictness: defFoAs(isStrict(P),z_diag(P)). % antisymmetry: defFoAs(isAntisymm(P),subseteq(int(P,rev(P)),id)). % trichotomy: defFoAs(isTrich(P),u_un([P,id,rev(P)])). % asymmetry (=isAntisymm+isStrict): defFoAs(isAsymm(P),z_int(P,rev(P))). % total reflexivity (=isRefl+Tot): defFoAs(isTotRefl(P),subseteq(id,P)). % connexity (=isTotRefl+isTrich): defFoAs(isConnex(P),u_un(P,rev(P))). % (cf. [SS93], p.12) % preorder relation: defThAs(isPreord(P),[isRefl(P),isTrans(P)]). % equivalence relation (a special case of preorder): defThAs(isEquiv(P),[isSymm(P),isTrans(P)]). % single-valuedness (property of a partial function) defFoAs('isFunc'(P),subseteq(bros(P),id)). % an equivalence relation is often characterized via % a choice of representatives: defThAs(isEquiv(P,Ch), ['isFunc'(Ch),is_circ(Ch,Ch),equiv(circ(Ch,rev(Ch)),P)]). % Galois' connection: defThAs(isGaloisCorr(F), [ subseteq( circ(F,F), id ), isStrict(F), subseteq( rev(F), rA( F ) ) ]). %======= % density (of a reflexive ordering): defFoAs( isDense(Le), subseteq( arcs(Le), circ(arcs(Le), arcs(Le)) )). % lack of endpoints: defFoAs( isWithoutEndPoints(Le), subseteq( id, link(arcs(Le), rev(arcs(Le))) )). % (Non-decreasing) monotonicity: defFoAs( isNDMonotonic( F, Le ), z_int( circ( Le, F ), circ( F, opp( Le ) ) )). % Bisimulation: defFoAs( isBisim( Bis, Oss ), z_un( lA( setminus( Bis, rev(Bis) ) ), setminus( circ( Oss, Bis ), circ( Bis, Oss ) ) ) ).