---

{ [Info:Type]. [es:EO+(Info)]. [A:Type]. [X:EClass(A)]. [e1,e2:E].
    X[e1;e2]
    = (if e1 <loc e2  e1  X then [X(e1)] else [] fi 
      @ X(e1, e2)
      @ if e2  X then [X(e2)] else [] fi ) 
    supposing e1 loc e2  }

{ Proof }

---

Definitions occuring in Statement :  es-closed-interval-vals: X[e1;e2],  es-prior-interval-vals: X(e1, e2),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-bless: e <loc e',  es-le: e loc e' ,  es-E: E,  append: as @ bs,  band: p  q,  ifthenelse: if b then t else f fi ,  uimplies: b supposing a,  uall: [x:A]. B[x],  cons: [car / cdr],  nil: [],  list: type List,  universe: Type,  equal: s = t
Definitions :  es-closed-interval-vals: X[e1;e2],  append: as @ bs,  ifthenelse: if b then t else f fi ,  band: p  q,  member: t  T,  implies: P  Q,  all: x:A. B[x],  btrue: tt,  prop: ,  bfalse: ff,  so_lambda: x y.t[x; y],  mapfilter: mapfilter(f;P;L),  top: Top,  subtype: S  T,  map: map(f;as),  filter: filter(P;l),  reduce: reduce(f;k;as),  ycomb: Y,  and: P  Q,  assert: b,  squash: T,  true: True,  uall: [x:A]. B[x],  uimplies: b supposing a,  bool: ,  unit: Unit,  iff: P  Q,  so_apply: x[s1;s2],  not: A,  false: False,  sq_type: SQType(T),  guard: {T},  it: ,  es-prior-interval-vals: X(e1, e2)
Lemmas :  es-interval-open-interval,  es-bless_wf,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  es-le_wf,  event-ordering+_inc,  es-E_wf,  eclass_wf,  event-ordering+_wf,  es-interval_wf,  append_wf,  es-open-interval_wf,  in-eclass_wf,  es-interface-top,  length_wf_nat,  es-interval_wf2,  top_wf,  Id_wf,  es-loc_wf,  nat_wf,  mapfilter_wf,  eclass-val_wf,  es-prior-interval-vals_wf,  member_wf,  l_member_wf,  assert_elim,  mapfilter-append,  subtype_base_sq,  bool_subtype_base,  squash_wf,  true_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e1,e2:E].
    X[e1;e2]
    =  (if  e1  <loc  e2  \mwedge{}\msubb{}  e1  \mmember{}\msubb{}  X  then  [X(e1)]  else  []  fi 
        @  X(e1,  e2)
        @  if  e2  \mmember{}\msubb{}  X  then  [X(e2)]  else  []  fi  ) 
    supposing  e1  \mleq{}loc  e2 


Date html generated: 2011_08_16-PM-04_09_19
Last ObjectModification: 2011_06_20-AM-00_42_42

Home Index