---

{ [Info:Type]. [es:EO+(Info)]. [A:Type]. [X:EClass(A)]. [e:E].
    (X(<e)
    = if e  prior(X) then X(<prior(X)(e)) @ [X(prior(X)(e))] else [] fi ) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-interface: prior(X),  es-prior-interface-vals: X(<e),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  append: as @ bs,  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  cons: [car / cdr],  nil: [],  list: type List,  universe: Type,  equal: s = t
Definitions :  false: False,  not: A,  implies: P  Q
Lemmas :  member-es-before,  uiff_inversion,  es-locl_wf,  Id_wf,  l_all_wf,  filter_is_nil,  length_wf_nat,  es-is-prior-interface-pred,  false_wf,  bool_subtype_base,  eclass-val_wf2,  ifthenelse_wf,  es-pred-causl,  append-nil,  subtype_base_sq,  es-prior-interface-vals_wf,  map_wf,  true_wf,  squash_wf,  iff_wf,  rev_implies_wf,  es-prior-interface-val-pred,  mapfilter_wf,  es-pred_wf,  eclass-val_wf,  append_wf,  es-before_wf,  l_member_wf,  mapfilter-append,  es-is-prior-interface,  btrue_neq_bfalse,  assert_elim,  es-locl-first,  es-first_wf,  nat_wf,  ge_wf,  nat_properties,  es-causl-swellfnd,  le_wf,  member_wf,  es-causl_wf,  bool_wf,  assert_wf,  iff_weakening_uiff,  eqtt_to_assert,  not_wf,  uiff_transitivity,  eqff_to_assert,  assert_of_bnot,  in-eclass_wf,  es-prior-interface_wf1,  es-prior-interface_wf,  es-interface-top,  es-E-interface_wf,  subtype_rel_self,  es-interface-subtype_rel2,  top_wf,  subtype_rel_wf,  bnot_wf,  eclass_wf,  event-ordering+_wf,  es-E_wf,  event-ordering+_inc

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (X(<e)  =  if  e  \mmember{}\msubb{}  prior(X)  then  X(<prior(X)(e))  @  [X(prior(X)(e))]  else  []  fi  )


Date html generated: 2011_08_16-PM-05_01_06
Last ObjectModification: 2011_06_20-AM-01_08_57

Home Index