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` THEN (InstConcl [⌈1⌉])⋅}

1
.....wf..... 
1. es EO@i'
2. e1 E@i
3. e2 {e:E| loc(e) loc(e1) ∈ Id} @i
4. {e:E| loc(e) loc(e1) ∈ Id}  ─→ {e:E| loc(e) loc(e1) ∈ Id}  ─→ ℙ
5. {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) ∧ (1 1) ≤loc e2 )
   ∧ ((∀i:ℕ1. (f i <loc (i 1))) ∧ (∀i:ℕ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. {e:E| loc(e) loc(e1) ∈ Id}  ─→ {e:E| loc(e) loc(e1) ∈ Id}  ─→ ℙ
5. {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. : ℕ+
⊢ ∃f:ℕm ─→ {e:E| loc(e) loc(e1) ∈ Id} 
   ((((f 0) e1 ∈ E) ∧ (m 1) ≤loc e2 )
   ∧ ((∀i:ℕ1. (f i <loc (i 1))) ∧ (∀i:ℕ1. p[f i;pred(f (i 1))]))
   ∧ q[f (m 1);e2]) ∈ ℙ


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

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




Home Index