Step
*
of Lemma
es-pstar-q_wf
∀[es:EO]. ∀[e1:E]. ∀[e2:{e:E| loc(e) = loc(e1) ∈ Id} ]. ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id}
─→ {e:E| loc(e) = loc(e1) ∈ Id}
─→ ℙ].
([e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ)
BY
{ (Auto THEN Unfold `es-pstar-q` 0 THEN Unfold `and` 0 THEN Fold `cand` 0 THEN Auto THEN ExRepD) }
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
⊢ pred(f (i + 1)) ∈ {e:E| loc(e) = loc(e1) ∈ Id}
Latex:
\mforall{}[es:EO]. \mforall{}[e1:E]. \mforall{}[e2:\{e:E| loc(e) = loc(e1)\} ]. \mforall{}[p,q:\{e:E| loc(e) = loc(e1)\}
{}\mrightarrow{} \{e:E| loc(e) = loc(e1)\}
{}\mrightarrow{} \mBbbP{}].
([e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b] \mmember{} \mBbbP{})
By
(Auto THEN Unfold `es-pstar-q` 0 THEN Unfold `and` 0 THEN Fold `cand` 0 THEN Auto THEN ExRepD)
Home
Index