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