Proof of Nuprl Lemma : Memory-class-mem

Step * 1 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. v1 ↓∈ init loc(e1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
⊢ R[a;v1;v2]
BY
{ ((Assert ⌈prior-iterated-classrel(es;A;B;v1;X;f;init;e1)⌉⋅
    THENA (RepUR ``prior-iterated-classrel`` 0 THEN OrLeft THEN MaAuto)
    )
   THEN (Assert ⌈e1 ≤loc pred(e2) ⌉⋅ THENA MaAuto)

   THEN 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. v1 ↓∈ init loc(e1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
24. prior-iterated-classrel(es;A;B;v1;X;f;init;e1)
25. e1 ≤loc pred(e2)
26. a1 : A@i
27. s : B@i
28. e : E@i
29. e1 ≤loc e @i
30. e ≤loc pred(e2) @i
31. a1 ∈ X(e)@i
32. 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. v1 ↓∈ init loc(e1)
22. ¬↑first(e2)
23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2)
24. prior-iterated-classrel(es;A;B;v1;X;f;init;e1)
25. e1 ≤loc pred(e2)
26. a1 : A@i
27. a2 : A@i
28. s1 : B@i
29. s2 : B@i
30. e : E@i
31. e' : E@i
32. e1 ≤loc e @i
33. (e <loc e')@i
34. e' ≤loc pred(e2) @i
35. a1 ∈ X(e)@i
36. prior-iterated-classrel(es;A;B;s1;X;f;init;e)@i
37. a2 ∈ X(e')@i
38. iterated-classrel(es;B;A;f;init;X;pred(e');s2)@i
39. R[a1;s1;s2]@i
⊢ R[a1;s1;f a2 s2]

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. \muparrow{}first(e1) 21. v1 \mdownarrow{}\mmember{} init loc(e1) 22. \mneg{}\muparrow{}first(e2) 23. iterated-classrel(es;B;A;f;init;X;pred(e2);v2) \mvdash{} R[a;v1;v2] By Latex: ((Assert \mkleeneopen{}prior-iterated-classrel(es;A;B;v1;X;f;init;e1)\mkleeneclose{}\mcdot{} THENA (RepUR ``prior-iterated-classrel`` 0 THEN OrLeft THEN MaAuto) ) THEN (Assert \mkleeneopen{}e1 \mleq{}loc pred(e2) \mkleeneclose{}\mcdot{} THENA MaAuto) THEN 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