Nuprl Lemma : State2-exists

∀[Info,A1,A2,S:Type]. ∀[init:S]. ∀[tr1:Id ⟶ A1 ⟶ S ⟶ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ⟶ A2 ⟶ S ⟶ S].
∀[X2:EClass(A2)].
  ∀es:EO+(Info). ∀e:E.  (↓∃v:S. v ∈ State2(λloc.init;tr1;X1;tr2;X2)(e))


Proof



Definitions occuring in Statement :  State2: State2(init;tr1;X1;tr2;X2),  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
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  State2: State2(init;tr1;X1;tr2;X2),  subtype_rel: A ⊆r B,  top: Top,  implies: P ⇒ Q,  not: ¬A,  false: False,  assert: ↑b,  ifthenelse: if b then t else f fi ,  bag-null: bag-null(bs),  null: null(as),  single-bag: {x},  cons: [a / b],  bfalse: ff,  prop: ℙ,  squash: ↓T,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2]
Latex:
\mforall{}[Info,A1,A2,S:Type].  \mforall{}[init:S].  \mforall{}[tr1:Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X1:EClass(A1)].  \mforall{}[tr2:Id
                                                                                                                                                                        {}\mrightarrow{}  A2
                                                                                                                                                                        {}\mrightarrow{}  S
                                                                                                                                                                        {}\mrightarrow{}  S].
\mforall{}[X2:EClass(A2)].
    \mforall{}es:EO+(Info).  \mforall{}e:E.    (\mdownarrow{}\mexists{}v:S.  v  \mmember{}  State2(\mlambda{}loc.init;tr1;X1;tr2;X2)(e))


Date html generated: 2016_05_17-AM-10_05_26
Last ObjectModification: 2016_01_17-PM-11_02_49

Theory : classrel!lemmas


Home Index