---

Step * of Lemma alle-between1-not-first-since

∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].
  uiff(∀e∈[e1,e2).¬e = first e ≥ e1.p[e];∀e∈[e1,e2).¬p[e])
BY
{ (Auto THEN ParallelLast) }

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}  ─→ ℙ
5. ∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (¬e = first e ≥ e1.p[e]))
⊢ ∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (¬p[e]))

2
1. es : EO
2. e1 : E
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} 
4. p : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. ∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (¬p[e]))
⊢ ∀e:E. (e1 ≤loc e  ⇒ (e <loc e2) ⇒ (¬e = first e ≥ e1.p[e]))

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1:E].  \mforall{}[e2:\{e:E|  loc(e)  =  loc(e1)\}  ].  \mforall{}[p:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
    uiff(\mforall{}e\mmember{}[e1,e2).\mneg{}e  =  first  e  \mgeq{}  e1.p[e];\mforall{}e\mmember{}[e1,e2).\mneg{}p[e])


By

(Auto  THEN  ParallelLast)

---

Home Index