---

{ es:EO. i:Id.  (loc-on-path(es;i;[])  False) }

{ Proof }

---

Definitions occuring in Statement :  loc-on-path: loc-on-path(es;i;L),  event_ordering: EO,  Id: Id,  all: x:A. B[x],  iff: P  Q,  false: False,  nil: []
Definitions :  all: x:A. B[x],  iff: P  Q,  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  member: t  T,  loc-on-path: loc-on-path(es;i;L),  false: False,  map: map(f;as),  ycomb: Y,  decidable: Dec(P),  or: P  Q,  guard: {T},  prop:
Lemmas :  loc-on-path_wf,  es-E_wf,  false_wf,  Id_wf,  event_ordering_wf,  decidable__false,  nil_member

---

\mforall{}es:EO.  \mforall{}i:Id.    (loc-on-path(es;i;[])  \mLeftarrow{}{}\mRightarrow{}  False)


Date html generated: 2011_08_16-AM-10_54_57
Last ObjectModification: 2010_09_24-PM-08_56_50

Home Index