Nuprl Lemma : Memory2_wf

[Info,A1,A2,S:Type]. ∀[init:Id ─→ S]. ∀[tr1:Id ─→ A1 ─→ S ─→ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ─→ A2 ─→ S ─→ S].
[X2:EClass(A2)].
  (Memory2(init;tr1;X1;tr2;X2) ∈ EClass(S))


Proof




Definitions occuring in Statement :  Memory2: Memory2(init;tr1;X1;tr2;X2) eclass: EClass(A[eo; e]) Id: Id uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  Memory-loc-class_wf disjoint-union-tr_wf single-bag_wf disjoint-union-comb_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf Id_wf

Latex:
\mforall{}[Info,A1,A2,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  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)].
    (Memory2(init;tr1;X1;tr2;X2)  \mmember{}  EClass(S))



Date html generated: 2015_07_22-PM-00_19_55
Last ObjectModification: 2015_01_28-AM-10_13_18

Home Index