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

Step * of Lemma es-pstar-q-partition

∀es:EO. ∀e1,e2,b:E.
  ∀[Q,P:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].
    ((e1 <loc b)
    ⇒ b ≤loc e2
    ⇒ [e1;pred(b)]~([a,b].P[a;b])*[a,b].P[a;b]
    ⇒ [b;e2]~([a,b].P[a;b])*[a,b].Q[a;b]
    ⇒ [e1;e2]~([a,b].P[a;b])*[a,b].Q[a;b])
BY
{ (Auto
   THEN Auto
   THEN (All (Unfold `es-pstar-q`))
   THEN ExRepD
   THEN (InstConcl [m1 + m])⋅
   THEN Try ((Unfold `and` 0 THEN Fold `cand` 0 THEN Auto THEN ExRepD))) }

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
⊢ m1 + m ∈ ℕ⁺

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
⊢ ∃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])

3
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. m2 : ℕ⁺
24. f2 : ℕm2 ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
25. (f2 0) = e1 ∈ E
26. f2 (m2 - 1) ≤loc e2
27. ∀i:ℕm2 - 1. (f2 i <loc f2 (i + 1))
28. i : ℕm2 - 1@i
⊢ pred(f2 (i + 1)) ∈ {e:E| loc(e) = loc(e1) ∈ Id}

Latex:

\mforall{}es:EO. \mforall{}e1,e2,b:E. \mforall{}[Q,P:\{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \{e:E| loc(e) = loc(e1)\} {}\mrightarrow{} \mBbbP{}]. ((e1 <loc b) {}\mRightarrow{} b \mleq{}loc e2 {}\mRightarrow{} [e1;pred(b)]\msim{}([a,b].P[a;b])*[a,b].P[a;b] {}\mRightarrow{} [b;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 (Auto THEN Auto THEN (All (Unfold `es-pstar-q`)) THEN ExRepD THEN (InstConcl [m1 + m])\mcdot{} THEN Try ((Unfold `and` 0 THEN Fold `cand` 0 THEN Auto THEN ExRepD))) Home Index