Step
*
2
of Lemma
Memory-class-mem
1. [Info] : Type
2. [B] : Type
3. [A] : Type
4. R : A ⟶ 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. a : A@i
14. ∀a:A. ∀s:B. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s])@i
15. ∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
(e1 ≤loc e
⇒ (e <loc e')
⇒ (e' <loc e2)
⇒ a1 ∈ X(e)
⇒ s1 ∈ Memory-class(f;init;X)(e)
⇒ a2 ∈ X(e')
⇒ s2 ∈ Memory-class(f;init;X)(e')
⇒ R[a1;s1;s2]
⇒ R[a1;s1;f a2 s2])@i
16. single-valued-classrel(es;X;A)@i
17. single-valued-bag(init loc(e1);B)@i
18. (e1 <loc e2)@i
19. a ∈ X(e1)@i
20. ¬↑first(e1)
21. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
⊢ R[a;v1;v2]
BY
{ (InstLemma `iterated-classrel-mem` [⌜Info⌝;⌜A⌝;⌜B⌝;⌜init⌝;⌜f⌝;⌜X⌝;⌜es⌝;⌜R⌝;⌜e1⌝;⌜pred(e2)⌝;⌜v1⌝;⌜v2⌝;⌜a⌝]⋅
THEN Auto
) }
1
1. [Info] : Type
2. [B] : Type
3. [A] : Type
4. R : A ⟶ 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. a : A@i
14. ∀a:A. ∀s:B. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s])@i
15. ∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
(e1 ≤loc e
⇒ (e <loc e')
⇒ (e' <loc e2)
⇒ a1 ∈ X(e)
⇒ s1 ∈ Memory-class(f;init;X)(e)
⇒ a2 ∈ X(e')
⇒ s2 ∈ Memory-class(f;init;X)(e')
⇒ R[a1;s1;s2]
⇒ R[a1;s1;f a2 s2])@i
16. single-valued-classrel(es;X;A)@i
17. single-valued-bag(init loc(e1);B)@i
18. (e1 <loc e2)@i
19. a ∈ X(e1)@i
20. ¬↑first(e1)
21. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
24. a1 : A@i
25. s : B@i
26. e : E@i
27. e1 ≤loc e @i
28. e ≤loc pred(e2) @i
29. a1 ∈ X(e)@i
30. prior-iterated-classrel(es;A;B;s;X;f;init;e)@i
⊢ R[a1;s;f a1 s]
2
1. [Info] : Type
2. [B] : Type
3. [A] : Type
4. R : A ⟶ 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. a : A@i
14. ∀a:A. ∀s:B. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s])@i
15. ∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
(e1 ≤loc e
⇒ (e <loc e')
⇒ (e' <loc e2)
⇒ a1 ∈ X(e)
⇒ s1 ∈ Memory-class(f;init;X)(e)
⇒ a2 ∈ X(e')
⇒ s2 ∈ Memory-class(f;init;X)(e')
⇒ R[a1;s1;s2]
⇒ R[a1;s1;f a2 s2])@i
16. single-valued-classrel(es;X;A)@i
17. single-valued-bag(init loc(e1);B)@i
18. (e1 <loc e2)@i
19. a ∈ X(e1)@i
20. ¬↑first(e1)
21. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
24. a1 : A@i
25. a2 : A@i
26. s1 : B@i
27. s2 : B@i
28. e : E@i
29. e' : E@i
30. e1 ≤loc e @i
31. (e <loc e')@i
32. e' ≤loc pred(e2) @i
33. a1 ∈ X(e)@i
34. prior-iterated-classrel(es;A;B;s1;X;f;init;e)@i
35. a2 ∈ X(e')@i
36. iterated-classrel(es;B;A;f;init;X;pred(e');s2)@i
37. R[a1;s1;s2]@i
⊢ R[a1;s1;f a2 s2]
3
.....antecedent.....
1. [Info] : Type
2. [B] : Type
3. [A] : Type
4. R : A ⟶ 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. a : A@i
14. ∀a:A. ∀s:B. ∀e:E. (e1 ≤loc e ⇒ (e <loc e2) ⇒ a ∈ X(e) ⇒ s ∈ Memory-class(f;init;X)(e) ⇒ R[a;s;f a s])@i
15. ∀a1,a2:A. ∀s1,s2:B. ∀e,e':E.
(e1 ≤loc e
⇒ (e <loc e')
⇒ (e' <loc e2)
⇒ a1 ∈ X(e)
⇒ s1 ∈ Memory-class(f;init;X)(e)
⇒ a2 ∈ X(e')
⇒ s2 ∈ Memory-class(f;init;X)(e')
⇒ R[a1;s1;s2]
⇒ R[a1;s1;f a2 s2])@i
16. single-valued-classrel(es;X;A)@i
17. single-valued-bag(init loc(e1);B)@i
18. (e1 <loc e2)@i
19. a ∈ X(e1)@i
20. ¬↑first(e1)
21. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
⊢ prior-iterated-classrel(es;A;B;v1;X;f;init;e1)
Latex:
Latex:
1. [Info] : Type
2. [B] : Type
3. [A] : Type
4. R : A {}\mrightarrow{} 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. a : A@i
14. \mforall{}a:A. \mforall{}s:B. \mforall{}e:E.
(e1 \mleq{}loc e {}\mRightarrow{} (e <loc e2) {}\mRightarrow{} a \mmember{} X(e) {}\mRightarrow{} s \mmember{} Memory-class(f;init;X)(e) {}\mRightarrow{} R[a;s;f a s])@i
15. \mforall{}a1,a2:A. \mforall{}s1,s2:B. \mforall{}e,e':E.
(e1 \mleq{}loc e
{}\mRightarrow{} (e <loc e')
{}\mRightarrow{} (e' <loc e2)
{}\mRightarrow{} a1 \mmember{} X(e)
{}\mRightarrow{} s1 \mmember{} Memory-class(f;init;X)(e)
{}\mRightarrow{} a2 \mmember{} X(e')
{}\mRightarrow{} s2 \mmember{} Memory-class(f;init;X)(e')
{}\mRightarrow{} R[a1;s1;s2]
{}\mRightarrow{} R[a1;s1;f a2 s2])@i
16. single-valued-classrel(es;X;A)@i
17. single-valued-bag(init loc(e1);B)@i
18. (e1 <loc e2)@i
19. a \mmember{} X(e1)@i
20. \mneg{}\muparrow{}first(e1)
21. iterated-classrel(es;B;A;f;init;X;pred(e1);v1)
22. \mneg{}\muparrow{}first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
\mvdash{} R[a;v1;v2]
By
Latex:
(InstLemma `iterated-classrel-mem` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}pred(e2)\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}
;\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
THEN Auto
)
Home
Index