Step
*
1
1
of Lemma
Memory-class-trans1
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)) ∧ v1 ↓∈ init loc(e1)) ∨ ((¬↑first(e1)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e1);v1))
18. ↓((↑first(e2)) ∧ v2 ↓∈ init loc(e2)) ∨ ((¬↑first(e2)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e2);v2))
19. (e1 <loc e2)@i
20. e : E@i
21. e1 ≤loc e @i
22. (e <loc e2)@i
23. a : A@i
24. a ∈ X(e)@i
25. ¬↑first(e2)
26. ↑first(e1)
27. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
28. v : A
29. v ∈ X(e1)
⊢ R[v1;v2]
BY
{ ((Assert ⌈iterated-classrel(es;B;A;f;init;X;e1;f v v1)⌉⋅
THENA (Unsquash
THEN SplitOrHyps
THEN Auto
THEN RecUnfold `iterated-classrel` 0
THEN InstConcl [⌈v1⌉]⋅
THEN MaAuto
THEN (OrLeft THENA Auto)
THEN InstConcl [⌈v⌉]⋅
THEN Auto)
)
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)) ∧ v1 ↓∈ init loc(e1)) ∨ ((¬↑first(e1)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e1);v1))
18. ↓((↑first(e2)) ∧ v2 ↓∈ init loc(e2)) ∨ ((¬↑first(e2)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e2);v2))
19. (e1 <loc e2)@i
20. e : E@i
21. e1 ≤loc e @i
22. (e <loc e2)@i
23. a : A@i
24. a ∈ X(e)@i
25. ¬↑first(e2)
26. ↑first(e1)
27. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
28. v : A
29. v ∈ X(e1)
30. iterated-classrel(es;B;A;f;init;X;e1;f v v1)
31. loc(pred(e2)) = loc(e2) ∈ Id
32. (pred(e2) < e2)
33. ∀e':E. (e' < e2) ⇒ ((e' = pred(e2) ∈ E) ∨ (e' < pred(e2))) supposing loc(e') = loc(e2) ∈ Id
34. e1 = pred(e2) ∈ E
⊢ R[v1;v2]
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)) ∧ v1 ↓∈ init loc(e1)) ∨ ((¬↑first(e1)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e1);v1))
18. ↓((↑first(e2)) ∧ v2 ↓∈ init loc(e2)) ∨ ((¬↑first(e2)) ∧ iterated-classrel(es;B;A;f;init;X;pred(e2);v2))
19. (e1 <loc e2)@i
20. e : E@i
21. e1 ≤loc e @i
22. (e <loc e2)@i
23. a : A@i
24. a ∈ X(e)@i
25. ¬↑first(e2)
26. ↑first(e1)
27. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
28. v : A
29. v ∈ X(e1)
30. iterated-classrel(es;B;A;f;init;X;e1;f v v1)
31. loc(pred(e2)) = loc(e2) ∈ Id
32. (pred(e2) < e2)
33. ∀e':E. (e' < e2) ⇒ ((e' = pred(e2) ∈ E) ∨ (e' < pred(e2))) supposing loc(e') = loc(e2) ∈ Id
34. (e1 < pred(e2))
⊢ R[v1;v2]
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. \mdownarrow{}((\muparrow{}first(e1)) \mwedge{} v1 \mdownarrow{}\mmember{} init loc(e1))
\mvee{} ((\mneg{}\muparrow{}first(e1)) \mwedge{} iterated-classrel(es;B;A;f;init;X;pred(e1);v1))
18. \mdownarrow{}((\muparrow{}first(e2)) \mwedge{} v2 \mdownarrow{}\mmember{} init loc(e2))
\mvee{} ((\mneg{}\muparrow{}first(e2)) \mwedge{} iterated-classrel(es;B;A;f;init;X;pred(e2);v2))
19. (e1 <loc e2)@i
20. e : E@i
21. e1 \mleq{}loc e @i
22. (e <loc e2)@i
23. a : A@i
24. a \mmember{} X(e)@i
25. \mneg{}\muparrow{}first(e2)
26. \muparrow{}first(e1)
27. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
28. v : A
29. v \mmember{} X(e1)
\mvdash{} R[v1;v2]
By
Latex:
((Assert \mkleeneopen{}iterated-classrel(es;B;A;f;init;X;e1;f v v1)\mkleeneclose{}\mcdot{}
THENA (Unsquash
THEN SplitOrHyps
THEN Auto
THEN RecUnfold `iterated-classrel` 0
THEN InstConcl [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
THEN MaAuto
THEN (OrLeft THENA Auto)
THEN InstConcl [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
THEN Auto)
)
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