---

fpf-union-compatible(A;C;x.B[x];eq;R;f;g) ==
  x:A
    ((x  dom(g))
     (x  dom(f))
     (a:C
          ((((a  g(x))  ((R f(x) a)))  ((a  f(x))  ((R g(x) a))))
           (a':B[x]. ((a' = a)  (a'  f(x))  (a'  g(x)))))))

---

Definitions :  fpf-dom: x  dom(f),  all: x:A. B[x],  implies: P  Q,  or: P  Q,  not: A,  assert: b,  apply: f a,  exists: x:A. B[x],  equal: s = t,  and: P  Q,  l_member: (x  l),  fpf-ap: f(x)
FDL editor aliases :  fpf-union-compatible

---

fpf-union-compatible(A;C;x.B[x];eq;R;f;g)  ==
    \mforall{}x:A
        ((\muparrow{}x  \mmember{}  dom(g))
        {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))
        {}\mRightarrow{}  (\mforall{}a:C
                    ((((a  \mmember{}  g(x))  \mwedge{}  (\mneg{}\muparrow{}(R  f(x)  a)))  \mvee{}  ((a  \mmember{}  f(x))  \mwedge{}  (\mneg{}\muparrow{}(R  g(x)  a))))
                    {}\mRightarrow{}  (\mexists{}a':B[x].  ((a'  =  a)  \mwedge{}  (a'  \mmember{}  f(x))  \mwedge{}  (a'  \mmember{}  g(x)))))))


Date html generated: 2010_08_26-PM-11_44_46
Last ObjectModification: 2008_02_27-PM-09_37_39

Home Index