---

Step * of Lemma last-decidable

∀es:EO. ∀e:E.
  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]
    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
    ⇒ (∀e'≤e.P[e'] ⇐⇒ P[e] ∨ ∃e'≤e.(¬(P[e'] ⇐⇒ P[e])) ∧ ∀e''∈(e',e].P[e''] ⇐⇒ P[e]))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN Assert ⌈∃f:{a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b]\000C)⌉
        ⋅
   ) }

1
.....assertion..... 
1. es : EO@i'
2. e : E@i
3. [P] : {a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ
4. ∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a])@i
⊢ ∃f:{a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b])

2
1. es : EO@i'
2. e : E@i
3. [P] : {a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ
4. ∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a])@i
5. ∃f:{a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b])
⊢ ∀e'≤e.P[e'] ⇐⇒ P[e] ∨ ∃e'≤e.(¬(P[e'] ⇐⇒ P[e])) ∧ ∀e''∈(e',e].P[e''] ⇐⇒ P[e]

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.
    \mforall{}[P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a]))
        {}\mRightarrow{}  (\mforall{}e'\mleq{}e.P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e]  \mvee{}  \mexists{}e'\mleq{}e.(\mneg{}(P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e]))  \mwedge{}  \mforall{}e''\mmember{}(e',e].P[e'']  \mLeftarrow{}{}\mRightarrow{}  P[e]))


By

(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mexists{}f:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbB{}
                              \mforall{}a,b:\{a:E|  loc(a)  =  loc(e)\}  .    (P[a]  \mLeftarrow{}{}\mRightarrow{}  P[b]  \mLeftarrow{}{}\mRightarrow{}  f[a]  =  f[b])\mkleeneclose{}\mcdot{}
  )

---

Home Index