---

Step * of Lemma state-class1-state1-eq

∀[Info,B,A:Type]. ∀[f:Id ⟶ A ⟶ B ⟶ B]. ∀[init:Id ⟶ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (State1(init;f;X)(e) = state-class1(init;f;X)(e) ∈ bag(B))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN VrCausalInd'
   THEN Auto
   THEN RepUR ``State1 State-loc-comb rec-combined-loc-class-opt-1`` 0
   THEN RecUnfold `rec-comb` 0
   THEN RepUR ``class-ap`` 0
   THEN Fold `class-ap` 0
   THEN (Subst ⌜rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-loc-2(f)(w 0) s fi ;λloc.{init loc}) 
                ~ λl,x,s. if bag-null(x) then s else lifting-loc-2(f) l x s fi |Loc, X, Prior(self)?λloc.{init loc}|⌝ 0⋅
         THENA (RepUR ``rec-combined-loc-class-opt-1 class-ap`` 0 THEN Auto)
         )
   THEN Fold `State-loc-comb` 0
   THEN Fold `State1` 0
   THEN RepUR ``state-class1`` 0
   THEN RecUnfold `loop-class-state` 0
   THEN RepUR ``eclass-cond`` 0
   THEN Fold `state-class1` 0
   THEN RepUR ``class-ap`` 0
   THEN Fold `class-ap` 0
   THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (State1(init;f;X)(e)  =  state-class1(init;f;X)(e))


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  VrCausalInd'
  THEN  Auto
  THEN  RepUR  ``State1  State-loc-comb  rec-combined-loc-class-opt-1``  0
  THEN  RecUnfold  `rec-comb`  0
  THEN  RepUR  ``class-ap``  0
  THEN  Fold  `class-ap`  0
  THEN  (Subst  \mkleeneopen{}rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s.  if  bag-null(w  0)
                                                                                then  s
                                                                                else  lifting-loc-2(f)(w  0)  s
                                                                                fi  ;\mlambda{}loc.\{init  loc\})  \msim{}  \mlambda{}l,x,s.  if  bag-null(x)
                                                                                                                                then  s
                                                                                                                                else  lifting-loc-2(f)  l  x  s
                                                                                                                                fi  |Loc,  X,  Prior(self)?\mlambda{}loc.\{init  l\000Coc\}|\mkleeneclose{}
                0\mcdot{}
              THENA  (RepUR  ``rec-combined-loc-class-opt-1  class-ap``  0  THEN  Auto)
              )
  THEN  Fold  `State-loc-comb`  0
  THEN  Fold  `State1`  0
  THEN  RepUR  ``state-class1``  0
  THEN  RecUnfold  `loop-class-state`  0
  THEN  RepUR  ``eclass-cond``  0
  THEN  Fold  `state-class1`  0
  THEN  RepUR  ``class-ap``  0
  THEN  Fold  `class-ap`  0
  THEN  Repeat  (AutoSplit))

---

Home Index