Step
*
2
2
2
of Lemma
State-comb-exists
.....falsecase.....
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E@i
9. ∀e':E. ((e' < e)
⇒ (#(init loc(e')) > 0)
⇒ (↓∃v:B. v ∈ State-comb(init;f;X)(e')))
10. #(init loc(e)) > 0@i
11. ¬↑first(e)
12. v : B
13. v ∈ State-comb(init;f;X)(pred(e))
14. #(X es e) > 0
15. 0 < #(X es e) supposing ↓∃x:A. x ↓∈ X es e
16. x : A
17. x ∈ X(e)
18. ¬((X es e) = {} ∈ bag(A))
⊢ f x v ↓∈ lifting-2(f) (X es e) (Prior(State-comb(init;f;X))?init es e)
BY
{ (BagMemberD 0
THEN D 0
THEN Try (Fold `classrel` 0)
THEN InstConcl [⌈x⌉;⌈v⌉]⋅
THEN Auto
THEN MaUseClassRel 0
THEN D 0
THEN (OrLeft THENA Auto)
THEN InstConcl [⌈pred(e)⌉]⋅
THEN Auto) }
1
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E@i
9. ∀e':E. ((e' < e)
⇒ (#(init loc(e')) > 0)
⇒ (↓∃v:B. v ∈ State-comb(init;f;X)(e')))
10. #(init loc(e)) > 0@i
11. ¬↑first(e)
12. v : B
13. v ∈ State-comb(init;f;X)(pred(e))
14. #(X es e) > 0
15. 0 < #(X es e) supposing ↓∃x:A. x ↓∈ X es e
16. x : A
17. x ∈ X(e)
18. ¬((X es e) = {} ∈ bag(A))
19. x ∈ X(e)
⊢ es-p-local-pred(es;λe'.(↓∃w:B. w ∈ State-comb(init;f;X)(e'))) e pred(e)
Latex:
Latex:
.....falsecase.....
1. Info : Type
2. B : Type
3. A : Type
4. f : A {}\mrightarrow{} B {}\mrightarrow{} B
5. init : Id {}\mrightarrow{} bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E@i
9. \mforall{}e':E. ((e' < e) {}\mRightarrow{} (\#(init loc(e')) > 0) {}\mRightarrow{} (\mdownarrow{}\mexists{}v:B. v \mmember{} State-comb(init;f;X)(e')))
10. \#(init loc(e)) > 0@i
11. \mneg{}\muparrow{}first(e)
12. v : B
13. v \mmember{} State-comb(init;f;X)(pred(e))
14. \#(X es e) > 0
15. 0 < \#(X es e) supposing \mdownarrow{}\mexists{}x:A. x \mdownarrow{}\mmember{} X es e
16. x : A
17. x \mmember{} X(e)
18. \mneg{}((X es e) = \{\})
\mvdash{} f x v \mdownarrow{}\mmember{} lifting-2(f) (X es e) (Prior(State-comb(init;f;X))?init es e)
By
Latex:
(BagMemberD 0
THEN D 0
THEN Try (Fold `classrel` 0)
THEN InstConcl [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
THEN Auto
THEN MaUseClassRel 0
THEN D 0
THEN (OrLeft THENA Auto)
THEN InstConcl [\mkleeneopen{}pred(e)\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index