---

Step * 1 of Lemma es-pstar-q_wf


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

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\} 
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.  m  :  \mBbbN{}\msupplus{}@i
7.  f  :  \mBbbN{}m  {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}  @i
8.  (f  0)  =  e1
9.  f  (m  -  1)  \mleq{}loc  e2 
10.  \mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1))
11.  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