Add binary relation attributes to the docs

[ozgurakgun]

Some notes from code comments:

    one BinRelAttr_Reflexive     = return [essence| forAll &xP           : &dom . &rel(&x,&x) |]
    one BinRelAttr_Irreflexive   = return [essence| forAll &xP           : &dom . !(&rel(&x,&x)) |]
    one BinRelAttr_Coreflexive   = return [essence| forAll &xP, &yP      : &dom . &rel(&x,&y) -> &x=&y |]
    one BinRelAttr_Symmetric     = return [essence| forAll &xP, &yP      : &dom . &rel(&x,&y) -> &rel(&y,&x) |]
    one BinRelAttr_AntiSymmetric = return [essence| forAll &xP, &yP      : &dom . &rel(&x,&y) /\ &rel(&y,&x) -> &x=&y |]
    one BinRelAttr_ASymmetric    = return [essence| forAll &xP, &yP      : &dom . &rel(&x,&y) -> !&rel(&y,&x) |]
    one BinRelAttr_Transitive    = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&y,&z) -> &rel(&x,&z) |]
    one BinRelAttr_Total         = return [essence| forAll &xP, &yP      : &dom . &rel(&x, &y) \/ &rel(&y, &x) |]
    one BinRelAttr_Connex        = return [essence| forAll &xP, &yP      : &dom . &rel(&x,&y) \/ &rel(&y,&x) \/ (&x = &y) |]
    one BinRelAttr_Euclidean     = return [essence| forAll &xP, &yP, &zP : &dom . &rel(&x,&y) /\ &rel(&x,&z) -> &rel(&y,&z) |]
    one BinRelAttr_LeftTotal     = return [essence| forAll &xP : &dom . exists &yP : &dom . &rel(&x,&y) |]
    one BinRelAttr_RightTotal    = return [essence| forAll &yP : &dom . exists &xP : &dom . &rel(&x,&y) |]

    one BinRelAttr_Serial             = one BinRelAttr_LeftTotal
    one BinRelAttr_Equivalence        = one BinRelAttr_Reflexive ++ one BinRelAttr_Symmetric     ++ one BinRelAttr_Transitive
    one BinRelAttr_LinearOrder        = one BinRelAttr_Total ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
    one BinRelAttr_WeakOrder          = one BinRelAttr_Total ++ one BinRelAttr_Transitive
    one BinRelAttr_PreOrder           = one BinRelAttr_Reflexive ++ one BinRelAttr_Transitive
    one BinRelAttr_PartialOrder       = one BinRelAttr_Reflexive ++ one BinRelAttr_AntiSymmetric ++ one BinRelAttr_Transitive
    one BinRelAttr_StrictPartialOrder = one BinRelAttr_Irreflexive ++ one BinRelAttr_ASymmetric ++ one BinRelAttr_Transitive

-- reflexive, the diagonal is full
-- irreflexive, the diagonal is empty
-- coreflexive, only the diagonal is full
-- symmetric, if R(x,y) then R(y,x)
-- anti-symmetric, both R(x,y) and R(y,x) are never full at the same time (we say nothing about the the diagonal)
-- a-symmetric, anti-symmetric + irreflexive
-- transitive xy + yz -> xz
-- total: either R(x,y) or R(y,x). implies reflexive
-- connex: total, but doesn't imply reflexive (we say nothing about the diagonal)
-- left-total: every x is related to some y -- R(x,y)
-- right-total: every y is related to some x -- R(x,y)
-- Euclidean: xy + xz -> yz

-- some properties
-- total implies reflexive. connex doesn't.
-- aSymmetric implies irreflexive and antiSymmetric

-- derived definitions
-- serial: left-total
-- equivalance: reflexive + symmetric + transitive
-- linearOrder: antiSymmetric + total + transitive
-- weakOrder; total + transitive
-- preOrder: reflexive + transitive
-- partialOrder: reflexive + antiSymmetric + transitive
-- strictPartialOrder: irreflexive + transitive (implied aSymmetric)