Nuprl Lemma : State1-exists

[Info,A,B:Type]. ∀[init:B]. ∀[tr:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:B. v ∈ State1(λloc.init;tr;X)(e))


Proof




Definitions occuring in Statement :  State1: State1(init;tr;X) classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E Id: Id uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] squash: T lambda: λx.A[x] function: x:A ─→ B[x] universe: Type
Lemmas :  State-loc-comb-non-empty single-bag_wf assert_wf bag-null_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf Id_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:B].  \mforall{}[tr:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].
    \mforall{}es:EO+(Info).  \mforall{}e:E.    (\mdownarrow{}\mexists{}v:B.  v  \mmember{}  State1(\mlambda{}loc.init;tr;X)(e))



Date html generated: 2015_07_22-PM-00_25_01
Last ObjectModification: 2015_01_28-AM-10_08_28

Home Index