[<A HREF="RelationPredicates.ps">PostScript</A>]

<PRE>
RelationPredicates: <b>trait</b>
  % Tests for useful properties
  % of individual relations.
  <b>assumes</b>
    <A HREF="RelationBasics.html">RelationBasics</A>,
    <A HREF="RelationOps.html">RelationOps</A>
  <b>introduces</b>
    antisymmetric, asymmetric, equivalence,
      functional, irreflexive, oneToOne, reflexive,
      symmetric, total, transitive: R -&gt; Bool
    into, onto: R, R -&gt; Bool
  <b>asserts</b>
    <b>forall</b> r, r1, r2: R
      antisymmetric(r) == (r \I (r\inv)) \subseteq I;
      asymmetric(r) == r \I (r\inv) = \bot;
      equivalence(r) ==
        reflexive(r) /\ symmetric(r) /\ transitive(r);
      functional(r) == ((r\inv) \circ r) \subseteq I;
      irreflexive(r) == r \I I = \bot;
      oneToOne(r) == r \circ (r\inv) = I;
      reflexive(r) == I \subseteq r;
      symmetric(r) == r = r\inv;
      total(r) == dom(r) = I;
      transitive(r) == r = r\superplus;
      into(r1, r2) == range(r1) \subseteq set(r2);
      onto(r1, r2) == set(r2) \subseteq range(r1);
  <b>implies</b> <b>converts</b>
    antisymmetric, asymmetric, equivalence,
    functional, irreflexive, oneToOne, reflexive,
    symmetric, total, transitive, into, onto
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]