---

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

---

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

---

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


Date html generated: 2010_08_26-PM-11_46_18
Last ObjectModification: 2008_02_27-PM-09_39_09

Home Index