Nuprl Lemma : State1-prior

[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (Prior(State1(init;f;X))?λloc.{init loc}(e)
  if first(e) then {init loc(e)} else State1(init;f;X)(pred(e)) fi 
  ∈ bag(B))


Proof




Definitions occuring in Statement :  State1: State1(init;tr;X) primed-class-opt: Prior(X)?b class-ap: X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-first: first(e) es-pred: pred(e) es-loc: loc(e) es-E: E Id: Id ifthenelse: if then else fi  uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T single-bag: {x} bag: bag(T)
Lemmas :  es-local-pred_wf lt_int_wf bag-size_wf class-ap_wf State1_wf nat_wf or_wf sq_exists_wf es-locl_wf assert_wf all_wf not_wf eqtt_to_assert es-locl-first assert_elim btrue_neq_bfalse eqff_to_assert equal_wf bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot single-bag_wf es-loc_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf Id_wf es-pred_property es-pred-locl es-causl_weakening bag_wf iff_weakening_equal es-pred_wf es-loc-pred assert_of_lt_int bag-size-bag-member State1-loc-exists

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (Prior(State1(init;f;X))?\mlambda{}loc.\{init  loc\}(e)
    =  if  first(e)  then  \{init  loc(e)\}  else  State1(init;f;X)(pred(e))  fi  )



Date html generated: 2015_07_22-PM-00_25_07
Last ObjectModification: 2015_02_04-PM-04_38_47

Home Index