---

{ [Info:Type]
    es:EO+(Info). Sys:EClass(Top). L:E(Sys) List. j:Id.
      (loc-on-path(es;j;L)
       (u:E(Sys)
           A,B:E(Sys) List
            ((loc(u) = j)  (L = (A @ [u / B]))  (loc-on-path(es;j;A))))) }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  loc-on-path: loc-on-path(es;i;L),  es-loc: loc(e),  Id: Id,  append: as @ bs,  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  exists: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  cons: [car / cdr],  list: type List,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  member: t  T,  so_lambda: x y.t[x; y],  implies: P  Q,  subtype: S  T,  exists: x:A. B[x],  and: P  Q,  append: as @ bs,  cand: A c B,  prop: ,  not: A,  so_apply: x[s1;s2],  iff: P  Q,  false: False,  es-E-interface: E(X),  or: P  Q,  decidable: Dec(P)
Lemmas :  es-E-interface_wf,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  loc-on-path-nil,  loc-on-path_wf,  Id_wf,  loc-on-path-cons,  decidable__equal_Id,  es-loc_wf,  append_wf,  not_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}Sys:EClass(Top).  \mforall{}L:E(Sys)  List.  \mforall{}j:Id.
        (loc-on-path(es;j;L)
        {}\mRightarrow{}  (\mexists{}u:E(Sys).  \mexists{}A,B:E(Sys)  List.  ((loc(u)  =  j)  \mwedge{}  (L  =  (A  @  [u  /  B]))  \mwedge{}  (\mneg{}loc-on-path(es;j;A)))))


Date html generated: 2011_08_16-PM-04_05_54
Last ObjectModification: 2011_06_20-AM-00_40_14

Home Index