Step
*
1
2
1
1
1
of Lemma
State-loc-comb-classrel-non-loc
1. Info : Type
2. B : Type
3. A : Type
4. f : Id ─→ A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. ∀e':E. ((e' < e)
⇒ (∀v:B. (v ∈ State-loc-comb(init;f;X)(e')
⇐⇒ v ∈ State-comb(init;f loc(e');X)(e'))))
10. v : B@i
11. x : A
12. x ↓∈ X es e
13. x@0 : B
14. e' : E
15. (e' <loc e)
16. ∃w:B. w ∈ λl,x,s. if bag-null(x) then s else ∪x1∈x.∪x1@0∈s.{f l x1 x1@0} fi |Loc, X, Prior(self)?init|(e')
17. ∀e'':E
((e'' <loc e)
⇒ (e' <loc e'')
⇒ (¬↓∃w:B. w ∈ λl,x,s. if bag-null(x) then s else ∪x1∈x.∪x1@0∈s.{f l x1 x1@0} fi |Loc, X, Prior(self)?init|(e''))\000C)
18. x@0 ∈ λl,x,s. if bag-null(x) then s else ∪x1∈x.∪x1@0∈s.{f l x1 x1@0} fi |Loc, X, Prior(self)?init|(e')
19. v ↓∈ {f loc(e) x x@0}
20. ¬((X es e) = {} ∈ bag(A))
21. ¬((X es e) = {} ∈ bag(A))
22. x ↓∈ X es e
23. (e' <loc e)
⊢ ↓∃w:B. w ∈ λx,s. if bag-null(x) then s else ∪x1∈x.∪x1@0∈s.{f loc(e) x1 x1@0} fi |X,Prior(self)?init|(e')
BY
{ (RepeatFor 2 (Thin (-1))
THEN SquashExRepD⋅
THEN (InstHyp [⌈e'⌉;⌈w⌉] (-14)⋅ THENA Auto)
THEN RepUR ``State-loc-comb State-comb lifting-loc-2 lifting-2 lifting2-loc lifting2`` (-1)
THEN RepUR ``lifting-loc-gen-rev lifting-gen-rev`` (-1)
THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` (-1) THEN Reduce (-1)))
THEN D (-1)
THEN (D (-2) THENA Auto)
THEN D 0
THEN (InstConcl [⌈w⌉]⋅ THENA Auto)
THEN Subst ⌈loc(e) = loc(e') ∈ Id⌉ 0⋅
THEN MaAuto) }
Latex:
Latex:
1. Info : Type
2. B : Type
3. A : Type
4. f : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B
5. init : Id {}\mrightarrow{} bag(B)
6. X : EClass(A)@i'
7. es : EO+(Info)@i'
8. e : E@i
9. \mforall{}e':E
((e' < e)
{}\mRightarrow{} (\mforall{}v:B. (v \mmember{} State-loc-comb(init;f;X)(e') \mLeftarrow{}{}\mRightarrow{} v \mmember{} State-comb(init;f loc(e');X)(e'))))
10. v : B@i
11. x : A
12. x \mdownarrow{}\mmember{} X es e
13. x@0 : B
14. e' : E
15. (e' <loc e)
16. \mexists{}w:B
w \mmember{} \mlambda{}l,x,s. if bag-null(x) then s else \mcup{}x1\mmember{}x.\mcup{}x1@0\mmember{}s.\{f l x1 x1@0\} fi |Loc, X, Prior(self)?init\000C|(e')
17. \mforall{}e'':E
((e'' <loc e)
{}\mRightarrow{} (e' <loc e'')
{}\mRightarrow{} (\mneg{}\mdownarrow{}\mexists{}w:B
w \mmember{} \mlambda{}l,x,s. if bag-null(x)
then s
else \mcup{}x1\mmember{}x.\mcup{}x1@0\mmember{}s.\{f l x1 x1@0\}
fi |Loc, X, Prior(self)?init|(e'')))
18. x@0 \mmember{} \mlambda{}l,x,s. if bag-null(x) then s else \mcup{}x1\mmember{}x.\mcup{}x1@0\mmember{}s.\{f l x1 x1@0\} fi |Loc, X, Prior(self)?ini\000Ct|(e')
19. v \mdownarrow{}\mmember{} \{f loc(e) x x@0\}
20. \mneg{}((X es e) = \{\})
21. \mneg{}((X es e) = \{\})
22. x \mdownarrow{}\mmember{} X es e
23. (e' <loc e)
\mvdash{} \mdownarrow{}\mexists{}w:B
w \mmember{} \mlambda{}x,s. if bag-null(x) then s else \mcup{}x1\mmember{}x.\mcup{}x1@0\mmember{}s.\{f loc(e) x1 x1@0\} fi |X,Prior(self)?init|(e'\000C)
By
Latex:
(RepeatFor 2 (Thin (-1))
THEN SquashExRepD\mcdot{}
THEN (InstHyp [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}] (-14)\mcdot{} THENA Auto)
THEN RepUR ``State-loc-comb State-comb lifting-loc-2 lifting-2 lifting2-loc lifting2`` (-1)
THEN RepUR ``lifting-loc-gen-rev lifting-gen-rev`` (-1)
THEN RepeatFor 3 ((RecUnfold `lifting-gen-list-rev` (-1) THEN Reduce (-1)))
THEN D (-1)
THEN (D (-2) THENA Auto)
THEN D 0
THEN (InstConcl [\mkleeneopen{}w\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Subst \mkleeneopen{}loc(e) = loc(e')\mkleeneclose{} 0\mcdot{}
THEN MaAuto)
Home
Index