Step
*
1
2
1
1
of Lemma
Memory-classrel1
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
9. v : B
10. ↑first(e)
11. ↓(True ∧ v ↓∈ init loc(e))
∨ ((¬True)
∧ ((∃a:A. (a ∈ X(pred(e)) ∧ (∃b:B. (b ∈ Memory-class(f;init;X)(pred(e)) ∧ (v = (f a b) ∈ B)))))
∨ ((∀a:A. (¬a ∈ X(pred(e)))) ∧ v ∈ Memory-class(f;init;X)(pred(e)))))
⊢ v ↓∈ init loc(e)
BY
{ (SqExRepD THEN D -1 THEN Auto) }
Latex:
Latex:
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
9. v : B
10. \muparrow{}first(e)
11. \mdownarrow{}(True \mwedge{} v \mdownarrow{}\mmember{} init loc(e))
\mvee{} ((\mneg{}True)
\mwedge{} ((\mexists{}a:A. (a \mmember{} X(pred(e)) \mwedge{} (\mexists{}b:B. (b \mmember{} Memory-class(f;init;X)(pred(e)) \mwedge{} (v = (f a b))))))
\mvee{} ((\mforall{}a:A. (\mneg{}a \mmember{} X(pred(e)))) \mwedge{} v \mmember{} Memory-class(f;init;X)(pred(e)))))
\mvdash{} v \mdownarrow{}\mmember{} init loc(e)
By
Latex:
(SqExRepD THEN D -1 THEN Auto)
Home
Index