---

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

{ 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-fix: f**(e),  es-causle: e c e',  es-E: E,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  not: A,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  prop: ,  member: t  T,  implies: P  Q,  not: A,  all: x:A. B[x],  false: False
Lemmas :  last_wf

---

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


Date html generated: 2011_08_16-PM-05_45_27
Last ObjectModification: 2011_06_20-AM-01_32_49

Home Index