Proof of Nuprl Lemma : es-pstar-q_functionality_wrt

Step * of Lemma es-pstar-q_functionality_wrt_implies

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q,p',q':{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇒ p'[a;b]}))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {q[a;b] ⇒ q'[a;b]}))
    ⇒ {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇒ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})
BY

{ (((((Unfold `guard` 0 THEN UnivCD) THENA Auto) THEN (InstLemma `es-pstar-q_wf` [⌈es⌉; ⌈e1⌉; ⌈e2⌉; ⌈p⌉; ⌈q⌉])⋅)

    THENA Auto
    )
   THEN (InstLemma `es-pstar-q_wf` [⌈es⌉; ⌈e1⌉; ⌈e2⌉; ⌈p'⌉; ⌈q'⌉])⋅
   THEN Auto
   THEN let T = Try (OnMember (AllHyps h.(((InstHyp [⌈i⌉] h)⋅ THENA Auto)

                                          THEN (MoveToConcl (-1) THEN GenConclAtAddr [1;3])

                                          THEN Complete (Auto)) )⋅) in
         ((MoveToHyp 0 (-3))
          THEN (Unfold `es-pstar-q` (-1))
          THEN (Reduce (-1))
          THEN Unfold `es-pstar-q` 0
          THEN Reduce 0
          THEN RepeatFor 2 ((ParallelLast THEN T))
          THEN ExRepD
          THEN Auto
          THEN BackThruSomeHyp
          THEN Auto
          THEN T)) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ⁺
13. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id}
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. i : ℕm - 1@i
⊢ (f i ∈ [e1, e2])

2
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ⁺
13. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id}
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. i : ℕm - 1@i
⊢ (pred(f (i + 1)) ∈ [e1, e2])

3
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ⁺
13. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id}
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. ∀i:ℕm - 1. p'[f i;pred(f (i + 1))]
⊢ (f (m - 1) ∈ [e1, e2])

4
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ⁺
13. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id}
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. ∀i:ℕm - 1. p'[f i;pred(f (i + 1))]
⊢ (e2 ∈ [e1, e2])

Latex:

\mforall{}es:EO. \mforall{}e1:E. \mforall{}e2:\{e:E| loc(e) = loc(e1)\} . \mforall{}[p,q,p',q':\{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \mBbbP{}]. ((\mforall{}a,b:\{e:E| loc(e) = loc(e1)\} . ((a \mmember{} [e1, e2]) {}\mRightarrow{} (b \mmember{} [e1, e2]) {}\mRightarrow{} \{p[a;b] {}\mRightarrow{} p'[a;b]\})) {}\mRightarrow{} (\mforall{}a,b:\{e:E| loc(e) = loc(e1)\} . ((a \mmember{} [e1, e2]) {}\mRightarrow{} (b \mmember{} [e1, e2]) {}\mRightarrow{} \{q[a;b] {}\mRightarrow{} q'[a;b]\})) {}\mRightarrow{} \{[e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b] {}\mRightarrow{} [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]\}) By (((((Unfold `guard` 0 THEN UnivCD) THENA Auto) THEN (InstLemma `es-pstar-q\_wf` [\mkleeneopen{}es\mkleeneclose{}; \mkleeneopen{}e1\mkleeneclose{}; \mkleeneopen{}e2\mkleeneclose{}; \mkleeneopen{}p\mkleeneclose{}; \mkleeneopen{}q\mkleeneclose{}])\mcdot{} ) THENA Auto ) THEN (InstLemma `es-pstar-q\_wf` [\mkleeneopen{}es\mkleeneclose{}; \mkleeneopen{}e1\mkleeneclose{}; \mkleeneopen{}e2\mkleeneclose{}; \mkleeneopen{}p'\mkleeneclose{}; \mkleeneopen{}q'\mkleeneclose{}])\mcdot{} THEN Auto THEN let T = Try (OnMember (AllHyps h.(((InstHyp [\mkleeneopen{}i\mkleeneclose{}] h)\mcdot{} THENA Auto) THEN (MoveToConcl (-1) THEN GenConclAtAddr [1;3]) THEN Complete (Auto)) )\mcdot{}) in ((MoveToHyp 0 (-3)) THEN (Unfold `es-pstar-q` (-1)) THEN (Reduce (-1)) THEN Unfold `es-pstar-q` 0 THEN Reduce 0 THEN RepeatFor 2 ((ParallelLast THEN T)) THEN ExRepD THEN Auto THEN BackThruSomeHyp THEN Auto THEN T)) Home Index