Proof of Nuprl Lemma : es-pstar-q-partition

Step * 2 of Lemma es-pstar-q-partition

1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. b : E@i
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. (e1 <loc b)@i
8. b ≤loc e2 @i
9. m1 : ℕ⁺@i
10. f1 : ℕm1 ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
11. (f1 0) = e1 ∈ E@i
12. f1 (m1 - 1) ≤loc pred(b) @i
13. ∀i:ℕm1 - 1. (f1 i <loc f1 (i + 1))@i
14. ∀i:ℕm1 - 1. P[f1 i;pred(f1 (i + 1))]@i
15. P[f1 (m1 - 1);pred(b)]@i
16. m : ℕ⁺@i
17. f : ℕm ─→ {e:E| loc(e) = loc(b) ∈ Id} @i
18. (f 0) = b ∈ E@i
19. f (m - 1) ≤loc e2 @i
20. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
21. ∀i:ℕm - 1. P[f i;pred(f (i + 1))]@i
22. Q[f (m - 1);e2]@i
⊢ ∃f:ℕm1 + m ─→ {e:E| loc(e) = loc(e1) ∈ Id}
   ((((f 0) = e1 ∈ E) c∧ f ((m1 + m) - 1) ≤loc e2 )

   c∧ ((∀i:ℕ(m1 + m) - 1. (f i <loc f (i + 1))) c∧ (∀i:ℕ(m1 + m) - 1. P[f i;pred(f (i + 1))]))

   c∧ Q[f ((m1 + m) - 1);e2])
BY
{ InstConcl [λi.if i <z m1 then f1 i else f (i - m1) fi ]⋅ }

1
.....wf.....
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. b : E@i
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. (e1 <loc b)@i
8. b ≤loc e2 @i
9. m1 : ℕ⁺@i
10. f1 : ℕm1 ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
11. (f1 0) = e1 ∈ E@i
12. f1 (m1 - 1) ≤loc pred(b) @i
13. ∀i:ℕm1 - 1. (f1 i <loc f1 (i + 1))@i
14. ∀i:ℕm1 - 1. P[f1 i;pred(f1 (i + 1))]@i
15. P[f1 (m1 - 1);pred(b)]@i
16. m : ℕ⁺@i
17. f : ℕm ─→ {e:E| loc(e) = loc(b) ∈ Id} @i
18. (f 0) = b ∈ E@i
19. f (m - 1) ≤loc e2 @i
20. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
21. ∀i:ℕm - 1. P[f i;pred(f (i + 1))]@i
22. Q[f (m - 1);e2]@i

⊢ λi.if i <z m1 then f1 i else f (i - m1) fi  ∈ ℕm1 + m ─→ {e:E| loc(e) = loc(e1) ∈ Id}

2
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. b : E@i
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. (e1 <loc b)@i
8. b ≤loc e2 @i
9. m1 : ℕ⁺@i
10. f1 : ℕm1 ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
11. (f1 0) = e1 ∈ E@i
12. f1 (m1 - 1) ≤loc pred(b) @i
13. ∀i:ℕm1 - 1. (f1 i <loc f1 (i + 1))@i
14. ∀i:ℕm1 - 1. P[f1 i;pred(f1 (i + 1))]@i
15. P[f1 (m1 - 1);pred(b)]@i
16. m : ℕ⁺@i
17. f : ℕm ─→ {e:E| loc(e) = loc(b) ∈ Id} @i
18. (f 0) = b ∈ E@i
19. f (m - 1) ≤loc e2 @i
20. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
21. ∀i:ℕm - 1. P[f i;pred(f (i + 1))]@i
22. Q[f (m - 1);e2]@i
⊢ ((((λi.if i <z m1 then f1 i else f (i - m1) fi ) 0) = e1 ∈ E)
  c∧ (λi.if i <z m1 then f1 i else f (i - m1) fi ) ((m1 + m) - 1) ≤loc e2 )
c∧ ((∀i:ℕ(m1 + m) - 1

       ((λi.if i <z m1 then f1 i else f (i - m1) fi ) i <loc (λi.if i <z m1 then f1 i else f (i - m1) fi ) (i + 1)))

c∧ (∀i:ℕ(m1 + m) - 1

         P[(λi.if i <z m1 then f1 i else f (i - m1) fi ) i;pred((λi.if i <z m1 then f1 i else f (i - m1) fi )

                                                                (i + 1))]))

c∧ Q[(λi.if i <z m1 then f1 i else f (i - m1) fi ) ((m1 + m) - 1);e2]

3
.....wf.....
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. b : E@i
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. (e1 <loc b)@i
8. b ≤loc e2 @i
9. m1 : ℕ⁺@i
10. f1 : ℕm1 ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
11. (f1 0) = e1 ∈ E@i
12. f1 (m1 - 1) ≤loc pred(b) @i
13. ∀i:ℕm1 - 1. (f1 i <loc f1 (i + 1))@i
14. ∀i:ℕm1 - 1. P[f1 i;pred(f1 (i + 1))]@i
15. P[f1 (m1 - 1);pred(b)]@i
16. m : ℕ⁺@i
17. f : ℕm ─→ {e:E| loc(e) = loc(b) ∈ Id} @i
18. (f 0) = b ∈ E@i
19. f (m - 1) ≤loc e2 @i
20. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
21. ∀i:ℕm - 1. P[f i;pred(f (i + 1))]@i
22. Q[f (m - 1);e2]@i
23. f2 : ℕm1 + m ─→ {e:E| loc(e) = loc(e1) ∈ Id}
⊢ (((f2 0) = e1 ∈ E) c∧ f2 ((m1 + m) - 1) ≤loc e2 )

  c∧ ((∀i:ℕ(m1 + m) - 1. (f2 i <loc f2 (i + 1))) c∧ (∀i:ℕ(m1 + m) - 1. P[f2 i;pred(f2 (i + 1))]))

c∧ Q[f2 ((m1 + m) - 1);e2] ∈ ℙ

Latex:

1. es : EO@i' 2. e1 : E@i 3. e2 : E@i 4. b : E@i 5. [Q] : \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \mBbbP{} 6. [P] : \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \mBbbP{} 7. (e1 <loc b)@i 8. b \mleq{}loc e2 @i 9. m1 : \mBbbN{}\msupplus{}@i 10. f1 : \mBbbN{}m1 {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} @i 11. (f1 0) = e1@i 12. f1 (m1 - 1) \mleq{}loc pred(b) @i 13. \mforall{}i:\mBbbN{}m1 - 1. (f1 i <loc f1 (i + 1))@i 14. \mforall{}i:\mBbbN{}m1 - 1. P[f1 i;pred(f1 (i + 1))]@i 15. P[f1 (m1 - 1);pred(b)]@i 16. m : \mBbbN{}\msupplus{}@i 17. f : \mBbbN{}m {}\mrightarrow{} \{e:E| loc(e) = loc(b)\} @i 18. (f 0) = b@i 19. f (m - 1) \mleq{}loc e2 @i 20. \mforall{}i:\mBbbN{}m - 1. (f i <loc f (i + 1))@i 21. \mforall{}i:\mBbbN{}m - 1. P[f i;pred(f (i + 1))]@i 22. Q[f (m - 1);e2]@i \mvdash{} \mexists{}f:\mBbbN{}m1 + m {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} ((((f 0) = e1) c\mwedge{} f ((m1 + m) - 1) \mleq{}loc e2 ) c\mwedge{} ((\mforall{}i:\mBbbN{}(m1 + m) - 1. (f i <loc f (i + 1))) c\mwedge{} (\mforall{}i:\mBbbN{}(m1 + m) - 1. P[f i;pred(f (i + 1))])) c\mwedge{} Q[f ((m1 + m) - 1);e2]) By InstConcl [\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ]\mcdot{} Home Index