---

Step * 3 1 of Lemma es-pstar-q-trivial


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. e1 ≤loc e2 @i
7. q[e1;e2]@i
8. m : ℕ+
9. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
10. (f 0) = e1 ∈ E
11. f (m - 1) ≤loc e2 
12. ∀i:ℕm - 1. (f i <loc f (i + 1))
13. i : ℕm - 1@i
⊢ pred(f (i + 1)) ∈ {e:E| loc(e) = loc(e1) ∈ Id} 
BY
{ (InstHyp [⌈i⌉] (-2)⋅ THENA Auto) }

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. e1 ≤loc e2 @i
7. q[e1;e2]@i
8. m : ℕ+
9. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
10. (f 0) = e1 ∈ E
11. f (m - 1) ≤loc e2 
12. ∀i:ℕm - 1. (f i <loc f (i + 1))
13. i : ℕm - 1@i
14. (f i <loc f (i + 1))
⊢ pred(f (i + 1)) ∈ {e:E| loc(e) = loc(e1) ∈ Id} 

---

Latex:



1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  p  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
5.  q  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
6.  e1  \mleq{}loc  e2  @i
7.  q[e1;e2]@i
8.  m  :  \mBbbN{}\msupplus{}
9.  f  :  \mBbbN{}m  {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}  @i
10.  (f  0)  =  e1
11.  f  (m  -  1)  \mleq{}loc  e2 
12.  \mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1))
13.  i  :  \mBbbN{}m  -  1@i
\mvdash{}  pred(f  (i  +  1))  \mmember{}  \{e:E|  loc(e)  =  loc(e1)\} 


By

(InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)

---

Home Index