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

Step * 2 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
⊢ ((((λ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]
BY
{ (Reduce 0
   THEN SplitAndConcl
   THEN Try ((SplitOnConclITE THEN Auto' THEN Subst (m1 + m) - 1 - m1 ~ m - 1 0⋅ THEN Auto'))
   THEN Auto
   THEN RepeatFor 2 ((SplitOnConclITE THEN Auto'))
   THEN Try ((Subst (i + 1) - m1 ~ (i - m1) + 1 0⋅ THEN Auto))
   THEN Try ((BackThruSomeHyp THEN Auto'))
   THEN Subst (i - m1) + 1 ~ 0 0⋅
   THEN Auto'
   THEN (Subst i ~ m1 - 1 0⋅ THENL [(DVar `i' THEN Auto'); Id])
   THEN StrongHypSubst 18 0
   THEN Try (Trivial)) }

1
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. 0 < m1

24. ((f1 0) = e1 ∈ E) c∧ if (m1 + m) - 1 <z m1 then f1 ((m1 + m) - 1) else f ((m1 + m) - 1 - m1) fi  ≤loc e2

25. i : ℕ(m1 + m) - 1@i
26. i < m1
27. m1 ≤ (i + 1)
⊢ (f1 (m1 - 1) <loc b)

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{} ((((\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) 0) = e1) c\mwedge{} (\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) ((m1 + m) - 1) \mleq{}loc e2 ) c\mwedge{} ((\mforall{}i:\mBbbN{}(m1 + m) - 1 ((\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) i <loc (\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) (i + 1))) c\mwedge{} (\mforall{}i:\mBbbN{}(m1 + m) - 1 P[(\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) i;pred((\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) (i + 1))])) c\mwedge{} Q[(\mlambda{}i.if i <z m1 then f1 i else f (i - m1) fi ) ((m1 + m) - 1);e2] By (Reduce 0 THEN SplitAndConcl THEN Try ((SplitOnConclITE THEN Auto' THEN Subst (m1 + m) - 1 - m1 \msim{} m - 1 0\mcdot{} THEN Auto')) THEN Auto THEN RepeatFor 2 ((SplitOnConclITE THEN Auto')) THEN Try ((Subst (i + 1) - m1 \msim{} (i - m1) + 1 0\mcdot{} THEN Auto)) THEN Try ((BackThruSomeHyp THEN Auto')) THEN Subst (i - m1) + 1 \msim{} 0 0\mcdot{} THEN Auto' THEN (Subst i \msim{} m1 - 1 0\mcdot{} THENL [(DVar `i' THEN Auto'); Id]) THEN StrongHypSubst 18 0 THEN Try (Trivial)) Home Index