Nuprl Lemma : Memory2-functional

[Info,A1,A2,S:Type]. ∀[init:Id ─→ S]. ∀[tr1:Id ─→ A1 ─→ S ─→ S]. ∀[X1:EClass(A1)]. ∀[tr2:Id ─→ A2 ─→ S ─→ S].
[X2:EClass(A2)].
  ∀es:EO+(Info)
    (single-valued-classrel(es;X1;A1)
     single-valued-classrel(es;X2;A2)
     disjoint-classrel(es;A1;X1;A2;X2)
     Memory2(init;tr1;X1;tr2;X2) is functional)


Proof




Definitions occuring in Statement :  Memory2: Memory2(init;tr1;X1;tr2;X2) es-functional-class: is functional single-valued-classrel: single-valued-classrel(es;X;T) disjoint-classrel: disjoint-classrel(es;A;X;B;Y) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uall: [x:A]. B[x] all: x:A. B[x] implies:  Q function: x:A ─→ B[x] universe: Type
Lemmas :  Memory-loc-class-functional single-bag_wf disjoint-union-tr_wf disjoint-union-comb_wf bag_size_single_lemma false_wf single-valued-bag-single disjoint-union-comb-single-val disjoint-classrel_wf single-valued-classrel_wf event-ordering+_wf classrel_wf Memory2_wf es-E_wf event-ordering+_subtype less_than_wf bag-size_wf class-ap_wf nat_wf eclass_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)].
    \mforall{}es:EO+(Info)
        (single-valued-classrel(es;X1;A1)
        {}\mRightarrow{}  single-valued-classrel(es;X2;A2)
        {}\mRightarrow{}  disjoint-classrel(es;A1;X1;A2;X2)
        {}\mRightarrow{}  Memory2(init;tr1;X1;tr2;X2)  is  functional)



Date html generated: 2015_07_22-PM-00_19_57
Last ObjectModification: 2015_01_28-AM-10_13_39

Home Index