---

Step * 2 of Lemma last-decidable


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]
BY
{ (ExRepD THEN ((InstLemma `last-transition` [⌈es⌉; ⌈e⌉; ⌈f⌉])⋅ THENA Auto)) }

1
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}  ─→ 𝔹
6. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b])
7. ∀e'≤e.f[e'] = f[e] ∨ ∃e'≤e.(¬f[e'] = f[e]) ∧ ∀e''∈(e',e].f[e''] = f[e]
⊢ ∀e'≤e.P[e'] ⇐⇒ P[e] ∨ ∃e'≤e.(¬(P[e'] ⇐⇒ P[e])) ∧ ∀e''∈(e',e].P[e''] ⇐⇒ P[e]

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  [P]  :  \{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a])@i
5.  \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])
\mvdash{}  \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

(ExRepD  THEN  ((InstLemma  `last-transition`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index