---

{ [Info:Type]. [es:EO+(Info)]. [Sys:EClass(Top)]. [f:E(Sys)  E(Sys)].
  [x,y:E(Sys)]. [i:Id].
    (x-f*-y goes thru i last  ) }

{ Proof }

---

Definitions occuring in Statement :  path-goes-thru-last: x-f*-y goes thru i last,  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  Id: Id,  uall: [x:A]. B[x],  top: Top,  prop: ,  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  path-goes-thru-last: x-f*-y goes thru i last,  exists: x:A. B[x],  and: P  Q,  cand: A c B,  so_lambda: x y.t[x; y],  es-E-interface: E(X),  so_apply: x[s1;s2],  all: x:A. B[x],  subtype: S  T
Lemmas :  es-E-interface_wf,  Id_wf,  es-loc_wf,  not_wf,  es-E-interface-subtype_rel,  fun-connected_wf,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_wf,  event-ordering+_inc

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Sys:EClass(Top)].  \mforall{}[f:E(Sys)  {}\mrightarrow{}  E(Sys)].  \mforall{}[x,y:E(Sys)].  \mforall{}[i:Id].
    (x-f*-y  goes  thru  i  last  \mmember{}  \mBbbP{})


Date html generated: 2011_08_16-PM-06_02_26
Last ObjectModification: 2011_06_20-AM-01_45_48

Home Index