Step
*
1
of Lemma
Memory-class-trans2
1. Info : Type
2. B : Type
3. A : Type
4. R : B ─→ B ─→ ℙ@i'
5. f : A ─→ B ─→ B@i
6. init : Id ─→ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. v1 : B@i
12. v2 : B@i
13. Trans(B;x,y.R[x;y])@i
14. ∀a:A. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s])))@i
15. single-valued-classrel(es;X;A)@i
16. single-valued-bag(init loc(e1);B)@i
17. ↑first(e1)
18. v1 ↓∈ init loc(e1)
19. ¬↑first(e2)
20. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
21. (e1 <loc e2)@i
22. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ (∀a:A. (¬a ∈ X(e))))@i
⊢ v1 = v2 ∈ B
BY
{ ((InstHyp [⌈e1⌉] (-1)⋅ THENA MaAuto)
THEN (Assert ⌈iterated-classrel(es;B;A;f;init;X;e1;v1)⌉⋅
THENA (RecUnfold `iterated-classrel` 0 THEN InstConcl [⌈v1⌉]⋅ THEN MaAuto)
)
THEN InstLemma `es-pred_property` [⌈es⌉;⌈e2⌉]⋅
THEN Auto
THEN (InstHyp [⌈e1⌉] (-1)⋅ THENA Auto)
THEN D (-1)) }
1
1. Info : Type
2. B : Type
3. A : Type
4. R : B ─→ B ─→ ℙ@i'
5. f : A ─→ B ─→ B@i
6. init : Id ─→ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. v1 : B@i
12. v2 : B@i
13. Trans(B;x,y.R[x;y])@i
14. ∀a:A. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s])))@i
15. single-valued-classrel(es;X;A)@i
16. single-valued-bag(init loc(e1);B)@i
17. ↑first(e1)
18. v1 ↓∈ init loc(e1)
19. ¬↑first(e2)
20. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
21. (e1 <loc e2)@i
22. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ (∀a:A. (¬a ∈ X(e))))@i
23. ∀a:A. (¬a ∈ X(e1))
24. iterated-classrel(es;B;A;f;init;X;e1;v1)
25. loc(pred(e2)) = loc(e2) ∈ Id
26. (pred(e2) < e2)
27. ∀e':E. (e' < e2) ⇒ ((e' = pred(e2) ∈ E) ∨ (e' < pred(e2))) supposing loc(e') = loc(e2) ∈ Id
28. e1 = pred(e2) ∈ E
⊢ v1 = v2 ∈ B
2
1. Info : Type
2. B : Type
3. A : Type
4. R : B ─→ B ─→ ℙ@i'
5. f : A ─→ B ─→ B@i
6. init : Id ─→ bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. v1 : B@i
12. v2 : B@i
13. Trans(B;x,y.R[x;y])@i
14. ∀a:A. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ (∀s:B. (s ∈ Memory-class(f;init;X)(e) ⇒ R[s;f a s])))@i
15. single-valued-classrel(es;X;A)@i
16. single-valued-bag(init loc(e1);B)@i
17. ↑first(e1)
18. v1 ↓∈ init loc(e1)
19. ¬↑first(e2)
20. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
21. (e1 <loc e2)@i
22. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ (∀a:A. (¬a ∈ X(e))))@i
23. ∀a:A. (¬a ∈ X(e1))
24. iterated-classrel(es;B;A;f;init;X;e1;v1)
25. loc(pred(e2)) = loc(e2) ∈ Id
26. (pred(e2) < e2)
27. ∀e':E. (e' < e2) ⇒ ((e' = pred(e2) ∈ E) ∨ (e' < pred(e2))) supposing loc(e') = loc(e2) ∈ Id
28. (e1 < pred(e2))
⊢ v1 = v2 ∈ B
Latex:
Latex:
1. Info : Type
2. B : Type
3. A : Type
4. R : B {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}@i'
5. f : A {}\mrightarrow{} B {}\mrightarrow{} B@i
6. init : Id {}\mrightarrow{} bag(B)@i
7. X : EClass(A)@i'
8. es : EO+(Info)@i'
9. e1 : E@i
10. e2 : E@i
11. v1 : B@i
12. v2 : B@i
13. Trans(B;x,y.R[x;y])@i
14. \mforall{}a:A. \mforall{}e:E.
(e1 \mleq{}loc e
{}\mRightarrow{} (e <loc e2)
{}\mRightarrow{} a \mmember{} X(e)
{}\mRightarrow{} (\mforall{}s:B. (s \mmember{} Memory-class(f;init;X)(e) {}\mRightarrow{} R[s;f a s])))@i
15. single-valued-classrel(es;X;A)@i
16. single-valued-bag(init loc(e1);B)@i
17. \muparrow{}first(e1)
18. v1 \mdownarrow{}\mmember{} init loc(e1)
19. \mneg{}\muparrow{}first(e2)
20. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
21. (e1 <loc e2)@i
22. \mforall{}e:E. (e1 \mleq{}loc e {}\mRightarrow{} (e <loc e2) {}\mRightarrow{} (\mforall{}a:A. (\mneg{}a \mmember{} X(e))))@i
\mvdash{} v1 = v2
By
Latex:
((InstHyp [\mkleeneopen{}e1\mkleeneclose{}] (-1)\mcdot{} THENA MaAuto)
THEN (Assert \mkleeneopen{}iterated-classrel(es;B;A;f;init;X;e1;v1)\mkleeneclose{}\mcdot{}
THENA (RecUnfold `iterated-classrel` 0 THEN InstConcl [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{} THEN MaAuto)
)
THEN InstLemma `es-pred\_property` [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
THEN Auto
THEN (InstHyp [\mkleeneopen{}e1\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN D (-1))
Home
Index