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)