Step
*
2
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. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
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
{ (InstLemma `iterated-classrel-trans`
[⌈Info⌉;⌈A⌉;⌈B⌉;⌈init⌉;⌈f⌉;⌈R⌉;⌈X⌉;⌈es⌉;⌈pred(e1)⌉;⌈pred(e2)⌉;⌈v1⌉;⌈v2⌉]⋅
THEN Auto
THEN Try (Complete ((BLemma `es-locl-pred`⋅ THEN Auto)))) }
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. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
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@i
24. e : E@i
25. (pred(e1) <loc e)@i
26. e ≤loc pred(e2) @i
27. a ∈ X(e)@i
28. s : B@i
29. iterated-classrel(es;B;A;f;init;X;pred(e);s)@i
⊢ R[s;f a s]
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. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
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. (∃e:E. ((pred(e1) <loc e) ∧ e ≤loc pred(e2) ∧ (∃a:A. a ∈ X(e)))) ⇒ R[v1;v2]
24. (∀e:E. ((pred(e1) <loc e) ⇒ e ≤loc pred(e2) ⇒ (∀a:A. (¬a ∈ X(e))))) ⇒ (v1 = v2 ∈ B)
⊢ 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. \mneg{}\muparrow{}first(e1)
18. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
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:
(InstLemma `iterated-classrel-trans`
[\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}pred(e1)\mkleeneclose{};\mkleeneopen{}pred(e2)\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
THEN Auto
THEN Try (Complete ((BLemma `es-locl-pred`\mcdot{} THEN Auto))))
Home
Index