Step
*
2
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)
⊢ R[v1;v2]
BY
{ (InstLemma `iterated-classrel-trans`
[⌈Info⌉;⌈A⌉;⌈B⌉;⌈init⌉;⌈f⌉;⌈R⌉;⌈X⌉;⌈es⌉;⌈pred(e1)⌉;⌈pred(e2)⌉;⌈v1⌉;⌈v2⌉]⋅
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)) ∧ 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. a1 : A@i
28. e3 : E@i
29. (pred(e1) <loc e3)@i
30. e3 ≤loc pred(e2) @i
31. a1 ∈ X(e3)@i
32. s : B@i
33. iterated-classrel(es;B;A;f;init;X;pred(e3);s)@i
⊢ R[s;f a1 s]
2
.....antecedent.....
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)
⊢ (pred(e1) <loc pred(e2))
3
.....antecedent.....
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)
⊢ iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
4
.....antecedent.....
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)
⊢ iterated-classrel(es;B;A;f;init;X;pred(e2);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. \mneg{}\muparrow{}first(e1)
\mvdash{} R[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
)
Home
Index