Nuprl Lemma : state-class2-fun-eq

∀[Info,B,A1,A2:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[tr2:Id ─→ A2 ─→ B ─→ B]. ∀[X1:EClass(A1)].
∀[X2:EClass(A2)]. ∀[es:EO+(Info)]. ∀[e:E].
  (state-class2(init;tr1;X1;tr2;X2)(e)
     = if e ∈b X1
         then if first(e)
              then tr1 loc(e) X1@e (init loc(e))
              else tr1 loc(e) X1@e state-class2(init;tr1;X1;tr2;X2)(pred(e))
              fi 
       if e ∈b X2
         then if first(e)
              then tr2 loc(e) X2@e (init loc(e))
              else tr2 loc(e) X2@e state-class2(init;tr1;X1;tr2;X2)(pred(e))
              fi 
       if first(e) then init loc(e)
       else state-class2(init;tr1;X1;tr2;X2)(pred(e))
       fi 
     ∈ B) supposing 
     (disjoint-classrel(es;A1;X1;A2;X2) and 
     single-valued-classrel(es;X1;A1) and 
     single-valued-classrel(es;X2;A2))


Proof



Definitions occuring in Statement :  state-class2: state-class2(init;tr1;X1;tr2;X2),  classfun-res: X@e,  classfun: X(e),  single-valued-classrel: single-valued-classrel(es;X;T),  disjoint-classrel: disjoint-classrel(es;A;X;B;Y),  member-eclass: e ∈b X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-first: first(e),  es-pred: pred(e),  es-loc: loc(e),  es-E: E,  Id: Id,  ifthenelse: if b then t else f fi ,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  apply: f a,  function: x:A ─→ B[x],  universe: Type,  equal: s = t ∈ T
Lemmas :  member-parallel-class-bool,  eclass1_wf,  event-ordering+_subtype,  member-eclass_wf,  bool_wf,  eqtt_to_assert,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  member-eclass-eclass1,  classfun-res-parallel-class-left,  eclass1-disjoint-classrel,  disjoint-classrel-symm,  classfun-res-eclass1,  es-loc_wf,  classfun-res_wf,  iff_weakening_equal,  loop-class-state-functional,  single-bag_wf,  Id_wf,  parallel-class_wf,  bag_size_single_lemma,  false_wf,  parallel-class-single-val,  eclass1-single-val,  single-valued-bag-single,  classfun_wf,  es-pred_wf,  classfun-res-parallel-class-right,  state-class2_wf
Latex:
\mforall{}[Info,B,A1,A2:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[tr1:Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[tr2:Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  B  {}\mrightarrow{}  B].
\mforall{}[X1:EClass(A1)].  \mforall{}[X2:EClass(A2)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (state-class2(init;tr1;X1;tr2;X2)(e)
          =  if  e  \mmember{}\msubb{}  X1
                  then  if  first(e)
                            then  tr1  loc(e)  X1@e  (init  loc(e))
                            else  tr1  loc(e)  X1@e  state-class2(init;tr1;X1;tr2;X2)(pred(e))
                            fi 
              if  e  \mmember{}\msubb{}  X2
                  then  if  first(e)
                            then  tr2  loc(e)  X2@e  (init  loc(e))
                            else  tr2  loc(e)  X2@e  state-class2(init;tr1;X1;tr2;X2)(pred(e))
                            fi 
              if  first(e)  then  init  loc(e)
              else  state-class2(init;tr1;X1;tr2;X2)(pred(e))
              fi  )  supposing 
          (disjoint-classrel(es;A1;X1;A2;X2)  and 
          single-valued-classrel(es;X1;A1)  and 
          single-valued-classrel(es;X2;A2))


Date html generated: 2015_07_23-AM-11_30_16
Last ObjectModification: 2015_02_04-PM-04_44_06

Home Index