---

Step * 1 1 of Lemma eo-strict-forward-pred?


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. x : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
7. es-pred?(eo>e;e1) = (inl x) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
8. x1 : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
9. es-pred?(eo;e1) = (inl x1) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
10. loc(x) = loc(e1) ∈ Id@i
11. (x < e1)@i
12. ∀e':E. (e' < e1) ⇒ ((e' = x ∈ E) ∨ (e' < x)) supposing loc(e') = loc(e1) ∈ Id@i
13. loc(x1) = loc(e1) ∈ Id@i
14. (x1 < e1)@i
15. ∀e':E. (e' < e1) ⇒ ((e' = x1 ∈ E) ∨ (e' < x1)) supposing loc(e') = loc(e1) ∈ Id@i
16. (e <loc x) ∨ (¬(loc(x) = loc(e) ∈ Id))
17. x = x1 ∈ E
18. x1 = x ∈ E
19. loc(e) = loc(e1) ∈ Id
20. ¬↑first(e1)
21. ↑(es-eq(eo) pred(e1) e)
⊢ (inl x) = (inr ⋅ ) ∈ (E?)
BY
{ ((Assert ⌈False⌉⋅ THEN Auto)
   THEN (Assert ⌈↑pred(e1) = e⌉⋅ THENA (RepUR ``es-eq-E eqof`` 0 THEN Auto))
   THEN (RWO "assert-es-eq-E<" (-1) THENA Auto)
   THEN D (-7)
   THEN (InstLemma `es-pred_property` [⌈eo⌉;⌈e1⌉]⋅ THENA Auto)
   THEN RepD
   THEN (InstHyp [⌈x⌉] (-1)⋅ THENA Auto)
   THEN D (-1)
   THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  e1  :  E@i
5.  E  \msubseteq{}r  E
6.  x  :  \{e':E|  (e'  <loc  e1)  \mwedge{}  (e'  =  pred(e1))\}  @i
7.  es-pred?(eo>e;e1)  =  (inl  x)@i
8.  x1  :  \{e':E|  (e'  <loc  e1)  \mwedge{}  (e'  =  pred(e1))\}  @i
9.  es-pred?(eo;e1)  =  (inl  x1)@i
10.  loc(x)  =  loc(e1)@i
11.  (x  <  e1)@i
12.  \mforall{}e':E.  (e'  <  e1)  {}\mRightarrow{}  ((e'  =  x)  \mvee{}  (e'  <  x))  supposing  loc(e')  =  loc(e1)@i
13.  loc(x1)  =  loc(e1)@i
14.  (x1  <  e1)@i
15.  \mforall{}e':E.  (e'  <  e1)  {}\mRightarrow{}  ((e'  =  x1)  \mvee{}  (e'  <  x1))  supposing  loc(e')  =  loc(e1)@i
16.  (e  <loc  x)  \mvee{}  (\mneg{}(loc(x)  =  loc(e)))
17.  x  =  x1
18.  x1  =  x
19.  loc(e)  =  loc(e1)
20.  \mneg{}\muparrow{}first(e1)
21.  \muparrow{}(es-eq(eo)  pred(e1)  e)
\mvdash{}  (inl  x)  =  (inr  \mcdot{}  )


By

((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}\muparrow{}pred(e1)  =  e\mkleeneclose{}\mcdot{}  THENA  (RepUR  ``es-eq-E  eqof``  0  THEN  Auto))
  THEN  (RWO  "assert-es-eq-E<"  (-1)  THENA  Auto)
  THEN  D  (-7)
  THEN  (InstLemma  `es-pred\_property`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepD
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)\mcdot{}

---

Home Index