---

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:

---

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

---

Latex:
(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