---

Step * of Lemma es-pstar-q-trivial

∀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 ≤loc e2  ⇒ q[e1;e2] ⇒ [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b])
BY
{ (Auto THEN Unfold `es-pstar-q` 0 THEN (InstConcl [⌜1⌝])⋅) }

1
.....wf..... 
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
⊢ 1 ∈ ℕ+

2
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
⊢ ∃f:ℕ1 ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
   ((((f 0) = e1 ∈ E) ∧ f (1 - 1) ≤loc e2 )
   ∧ ((∀i:ℕ1 - 1. (f i <loc f (i + 1))) ∧ (∀i:ℕ1 - 1. p[f i;pred(f (i + 1))]))
   ∧ q[f (1 - 1);e2])

3
.....wf..... 
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 : ℕ+
⊢ ∃f:ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
   ((((f 0) = e1 ∈ E) ∧ f (m - 1) ≤loc e2 )
   ∧ ((∀i:ℕm - 1. (f i <loc f (i + 1))) ∧ (∀i:ℕm - 1. p[f i;pred(f (i + 1))]))
   ∧ q[f (m - 1);e2]) ∈ ℙ

---

Latex:

---

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  \mleq{}loc  e2    {}\mRightarrow{}  q[e1;e2]  {}\mRightarrow{}  [e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b])


By

---

Latex:
(Auto  THEN  Unfold  `es-pstar-q`  0  THEN  (InstConcl  [\mkleeneopen{}1\mkleeneclose{}])\mcdot{})

---

Home Index