---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). f:E(X)  E(X).
      ((x:E(X). f x c x)
       (e,e':E(X).
            ((e'  prior-f-fixedpoints(e))
             prior-f-fixedpoints(e')  prior-f-fixedpoints(e)))) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-fixedpoints: prior-f-fixedpoints(e),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-causle: e c e',  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  iseg: l1  l2,  l_member: (x  l)
Definitions :  subtype: S  T,  member: t  T,  all: x:A. B[x],  implies: P  Q,  es-E-interface: E(X)
Lemmas :  es-E-interface-subtype_rel,  es-E_wf,  es-E-interface_wf,  es-prior-fixedpoints_wf,  es-prior-fixedpoints-fix

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).
        ((\mforall{}x:E(X).  f  x  c\mleq{}  x)
        {}\mRightarrow{}  (\mforall{}e,e':E(X).
                    ((e'  \mmember{}  prior-f-fixedpoints(e))  {}\mRightarrow{}  prior-f-fixedpoints(e')  \mleq{}  prior-f-fixedpoints(e))))


Date html generated: 2011_08_16-PM-05_44_41
Last ObjectModification: 2011_06_20-AM-01_32_25

Home Index