Nuprl Lemma : Memory3-functional

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


Proof



Definitions occuring in Statement :  Memory3: Memory3,  es-functional-class: X 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: P ⇒ 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-symm,  disjoint-union-comb-disjoint-classrel,  disjoint-classrel_wf,  single-valued-classrel_wf,  event-ordering+_wf,  classrel_wf,  Memory3_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,A3,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{}[tr3:Id  {}\mrightarrow{}  A3  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X3:EClass(A3)].
    \mforall{}es:EO+(Info)
        (single-valued-classrel(es;X1;A1)
        {}\mRightarrow{}  single-valued-classrel(es;X2;A2)
        {}\mRightarrow{}  single-valued-classrel(es;X3;A3)
        {}\mRightarrow{}  disjoint-classrel(es;A1;X1;A2;X2)
        {}\mRightarrow{}  disjoint-classrel(es;A1;X1;A3;X3)
        {}\mRightarrow{}  disjoint-classrel(es;A2;X2;A3;X3)
        {}\mRightarrow{}  Memory3(init;
                              tr1;X1;
                              tr2;X2;
                              tr3;X3)  is  functional)


Date html generated: 2015_07_22-PM-00_20_04
Last ObjectModification: 2015_01_28-AM-10_14_04

Home Index