---

Step * 1 of Lemma es-local-pred-property2


1. [Info] : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
⊢ (↑isl(last(P) e) ⇐⇒ ∃a:E. ((a <loc e) ∧ (↑(P a))))
∧ (outl(last(P) e) <loc e)
  ∧ (↑(P outl(last(P) e)))
  ∧ (∀e'':E. ((e'' <loc e) ⇒ (outl(last(P) e) <loc e'') ⇒ (¬↑(P e'')))) 
  supposing ↑isl(last(P) e)
BY
{ ((GenConclAtAddr [1;1;1;1] THENA Auto) THEN Thin (-1) THEN D -1 THEN Reduce 0 THEN Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
6. x : ∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))}@i
7. True@i
⊢ ∃a:E. ((a <loc e) ∧ (↑(P a)))

2
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
6. x : ∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))}@i
7. True ⇐ ∃a:E. ((a <loc e) ∧ (↑(P a)))
8. True
9. ∃a:E. ((a <loc e) ∧ (↑(P a)))
⊢ (x <loc e)

3
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
6. x : ∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))}@i
7. True ⇐ ∃a:E. ((a <loc e) ∧ (↑(P a)))
8. True
9. (x <loc e)
10. ↑(P x)
11. e'' : E@i
12. (e'' <loc e)@i
13. (x <loc e'')@i
14. ∃a:E. ((a <loc e) ∧ (↑(P a)))
⊢ ¬↑(P e'')

4
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
6. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))})@i
7. ∃a:E. ((a <loc e) ∧ (↑(P a)))@i
⊢ False

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  P  :  \{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}@i
5.  last(P)  e  \mmember{}  (\mexists{}e':\{E|  ((e'  <loc  e)
                                                \mwedge{}  (\muparrow{}(P  e'))
                                                \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\})
      \mvee{}  (\mneg{}(\mexists{}e':\{E|  ((e'  <loc  e)  \mwedge{}  (\muparrow{}(P  e')))\}))
\mvdash{}  (\muparrow{}isl(last(P)  e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  ((a  <loc  e)  \mwedge{}  (\muparrow{}(P  a))))
\mwedge{}  (outl(last(P)  e)  <loc  e)
    \mwedge{}  (\muparrow{}(P  outl(last(P)  e)))
    \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (outl(last(P)  e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))) 
    supposing  \muparrow{}isl(last(P)  e)


By

---

Latex:
((GenConclAtAddr  [1;1;1;1]  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1  THEN  Reduce  0  THEN  Auto)

---

Home Index