Step
*
1
2
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. es-p-local-pred(es;λ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')))
e
e'
16. 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')
17. v ↓∈ {f loc(e) x x@0}
18. ¬((X es e) = {} ∈ bag(A))
19. ¬((X es e) = {} ∈ bag(A))
20. x ↓∈ X es e
⊢ ↓(∃e':E
((es-p-local-pred(es;λ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')))
e
e')
∧ x@0 ∈ λ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')))
∨ ((∀e':E
((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')))\000C))
∧ x@0 ↓∈ init loc(e))
BY
{ (D 0 THEN (OrLeft THENA Auto) THEN InstConcl [⌈e'⌉]⋅ THEN Auto) }
1
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. es-p-local-pred(es;λ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')))
e
e'
16. 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')
17. v ↓∈ {f loc(e) x x@0}
18. ¬((X es e) = {} ∈ bag(A))
19. ¬((X es e) = {} ∈ bag(A))
20. x ↓∈ X es e
⊢ es-p-local-pred(es;λ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\000C|(
e')))
e
e'
2
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. es-p-local-pred(es;λ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')))
e
e'
16. 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')
17. v ↓∈ {f loc(e) x x@0}
18. ¬((X es e) = {} ∈ bag(A))
19. ¬((X es e) = {} ∈ bag(A))
20. x ↓∈ X es e
21. es-p-local-pred(es;λ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)?in\000Cit|(
e')))
e
e'
⊢ x@0 ∈ λ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')
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. es-p-local-pred(es;\mlambda{}e'.(\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')))
e
e'
16. 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')
17. v \mdownarrow{}\mmember{} \{f loc(e) x x@0\}
18. \mneg{}((X es e) = \{\})
19. \mneg{}((X es e) = \{\})
20. x \mdownarrow{}\mmember{} X es e
\mvdash{} \mdownarrow{}(\mexists{}e':E
((es-p-local-pred(es;\mlambda{}e'.(\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')))
e
e')
\mwedge{} x@0 \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)?ini\000Ct|(
e')))
\mvee{} ((\mforall{}e':E
((e' <loc e)
{}\mRightarrow{} (\mforall{}w:B
(\mneg{}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')))))
\mwedge{} x@0 \mdownarrow{}\mmember{} init loc(e))
By
Latex:
(D 0 THEN (OrLeft THENA Auto) THEN InstConcl [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index