---

{ [Info:Type]
    es:EO+(Info)
      [A:Type]
        X:EClass(A List). e:E.
          (0 < ||es-interface-history(es;X;e)||
           e':E. (((e'  X)  e' loc e )  (0 < ||X(e')||))) }

{ Proof }

---

Definitions occuring in Statement :  es-interface-history: es-interface-history(es;X;e),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-E: E,  length: ||as||,  assert: b,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  and: P  Q,  less_than: a < b,  list: type List,  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  exists: x:A. B[x],  and: P  Q,  assert: b,  implies: P  Q,  rev_implies: P  Q,  member: t  T,  cand: A c B,  prop: ,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  uiff: uiff(P;Q),  subtype: S  T
Lemmas :  length_wf1,  es-interface-history_wf,  es-E_wf,  assert_wf,  in-eclass_wf,  es-le_wf,  eclass-val_wf,  event-ordering+_inc,  event-ordering+_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  eclass_wf,  assert_elim,  member_exists,  iff_weakening_uiff,  not_wf,  ge_wf,  length_of_not_nil,  member-es-interface-history,  assert_witness,  es-interface-top,  pos_length2,  member_null,  uiff_inversion,  member-exists,  member-exists2,  l_member_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type]
            \mforall{}X:EClass(A  List).  \mforall{}e:E.
                (0  <  ||es-interface-history(es;X;e)||
                \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (((\muparrow{}e'  \mmember{}\msubb{}  X)  \mwedge{}  e'  \mleq{}loc  e  )  \mwedge{}  (0  <  ||X(e')||)))


Date html generated: 2011_08_16-PM-04_38_55
Last ObjectModification: 2011_06_20-AM-01_01_19

Home Index