---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). f:E(X)  E(X).
      [R:E(X)  E(X)  ]
        (Trans(E(X);e',e.R[e';e])
         Refl(E(X);e',e.R[e';e])
         (x:E(X). R[f x;x])
         (e',e:E(X).  (e' is f*(e)  R[e';e]))) }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  trans: Trans(T;x,y.E[x; y]),  refl: Refl(T;x,y.E[x; y]),  uall: [x:A]. B[x],  top: Top,  prop: ,  so_apply: x[s1;s2],  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  fun-connected: y is f*(x)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  prop: ,  implies: P  Q,  so_apply: x[s1;s2],  uimplies: b supposing a,  not: A,  member: t  T,  so_lambda: x y.t[x; y],  false: False,  and: P  Q,  guard: {T},  refl: Refl(T;x,y.E[x; y]),  trans: Trans(T;x,y.E[x; y]),  subtype: S  T
Lemmas :  fun-connected-induction,  es-E-interface_wf,  fun-connected_wf,  not_wf,  refl_wf,  trans_wf,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).
        \mforall{}[R:E(X)  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}]
            (Trans(E(X);e',e.R[e';e])
            {}\mRightarrow{}  Refl(E(X);e',e.R[e';e])
            {}\mRightarrow{}  (\mforall{}x:E(X).  R[f  x;x])
            {}\mRightarrow{}  (\mforall{}e',e:E(X).    (e'  is  f*(e)  {}\mRightarrow{}  R[e';e])))


Date html generated: 2011_08_16-PM-04_05_39
Last ObjectModification: 2011_06_20-AM-00_40_01

Home Index