Step
*
1
2
of Lemma
loop-class-memory-exists
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e)
⇒ uiff(0 < #(init loc(e1));↓∃v:B. v ∈ loop-class-memory(X;init)(e1)))
8. 0 < #(init loc(e))
9. ¬↑first(e)
⊢ ↓∃v:B. v ∈ loop-class-memory(X;init)(e)
BY
{ ((InstHyp [⌈pred(e)⌉] (-3)⋅ THENA Auto)
THEN D (-1)
THEN Thin (-1)
THEN (D (-1) THENA (RWO "es-loc-pred" 0 THEN Auto))
THEN SquashExRepD
THEN (Decide ⌈↑pred(e) ∈b X⌉⋅ THENA Auto)) }
1
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e)
⇒ uiff(0 < #(init loc(e1));↓∃v:B. v ∈ loop-class-memory(X;init)(e1)))
8. 0 < #(init loc(e))
9. ¬↑first(e)
10. v : B
11. v ∈ loop-class-memory(X;init)(pred(e))
12. ↑pred(e) ∈b X
⊢ ↓∃v:B. v ∈ loop-class-memory(X;init)(e)
2
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e)
⇒ uiff(0 < #(init loc(e1));↓∃v:B. v ∈ loop-class-memory(X;init)(e1)))
8. 0 < #(init loc(e))
9. ¬↑first(e)
10. v : B
11. v ∈ loop-class-memory(X;init)(pred(e))
12. ¬↑pred(e) ∈b X
⊢ ↓∃v:B. v ∈ loop-class-memory(X;init)(e)
Latex:
Latex:
1. Info : Type
2. B : Type
3. X : EClass(B {}\mrightarrow{} B)
4. init : Id {}\mrightarrow{} bag(B)
5. es : EO+(Info)
6. e : E@i
7. \mforall{}e1:E. ((e1 < e) {}\mRightarrow{} uiff(0 < \#(init loc(e1));\mdownarrow{}\mexists{}v:B. v \mmember{} loop-class-memory(X;init)(e1)))
8. 0 < \#(init loc(e))
9. \mneg{}\muparrow{}first(e)
\mvdash{} \mdownarrow{}\mexists{}v:B. v \mmember{} loop-class-memory(X;init)(e)
By
Latex:
((InstHyp [\mkleeneopen{}pred(e)\mkleeneclose{}] (-3)\mcdot{} THENA Auto)
THEN D (-1)
THEN Thin (-1)
THEN (D (-1) THENA (RWO "es-loc-pred" 0 THEN Auto))
THEN SquashExRepD
THEN (Decide \mkleeneopen{}\muparrow{}pred(e) \mmember{}\msubb{} X\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index