---

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

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}  ─→ 𝔹
6. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b])
7. ∃e':E. (e' ≤loc e  c∧ ((¬f[e'] = f[e]) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ f[e''] = f[e]))))
⊢ ∃e':E. (e' ≤loc e  c∧ ((¬(P[e'] ⇐⇒ P[e])) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc 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.  f  :  \{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}a,b:\{a:E|  loc(a)  =  loc(e)\}  .    (P[a]  \mLeftarrow{}{}\mRightarrow{}  P[b]  \mLeftarrow{}{}\mRightarrow{}  f[a]  =  f[b])
7.  (\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  f[e']  =  f[e]))
\mvee{}  (\mexists{}e':E
        (e'  \mleq{}loc  e    c\mwedge{}  ((\mneg{}f[e']  =  f[e])  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  f[e'']  =  f[e])))))
\mvdash{}  (\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e])))
\mvee{}  (\mexists{}e':E
        (e'  \mleq{}loc  e 
        c\mwedge{}  ((\mneg{}(P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e]))  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (P[e'']  \mLeftarrow{}{}\mRightarrow{}  P[e]))))))


By

(ParallelLast  THEN  Try  (Complete  (Auto)))

---

Home Index