---

Step * 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
⊢ (inl x) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else inl x1 fi  ∈ (E?)
BY
{ ((Assert ⌈(e <loc x) ∨ (¬(loc(x) = loc(e) ∈ Id))⌉⋅
    THENA (InstLemma `eo-strict-forward-E-member` [⌈Info⌉;⌈eo⌉;⌈e⌉;⌈x⌉]⋅ THEN Auto)
    )
   THEN (InstHyp [⌈x⌉] (-2)⋅ THENA Auto)⋅
   THEN (InstHyp [⌈x1⌉] (-6)⋅
         THENA (Try ((BLemma `member-eo-strict-forward-E`
                      THEN Auto
                      THEN D (-3)
                      THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
                      THEN D (-2)
                      THEN Auto
                      THEN (Assert ⌈(x <loc x1)⌉⋅ THENA Auto)
                      THEN FLemma `es-locl_transitivity` [-4;-1]
                      THEN Auto))
                THEN Auto
                )
         )
   THEN D (-2)
   THEN D (-1)
   THEN Auto
   THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
   THEN OldAutoBoolCase ⌈loc(e) = loc(e1)⌉⋅
   THEN (Assert ⌈¬↑first(e1)⌉⋅
         THENA (InstLemma `eo-strict-forward-E-member` [⌈Info⌉;⌈eo⌉;⌈e⌉;⌈e1⌉]⋅
                THEN Auto
                THEN (D (-1) THENA Auto)
                THEN (FLemma `es-locl-first` [-1] THENA Auto)
                THEN HypSubst' (-1) 0
                THEN Auto)
         )
   THEN (OldAutoSplit THENA (Auto THEN DoSubsume THEN Auto))) }

1
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?)

---

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
\mvdash{}  (inl  x)  =  if  loc(e)  =  loc(e1)  \mwedge{}\msubb{}  (es-eq(eo)  pred(e1)  e)  then  inr  \mcdot{}    else  inl  x1  fi 


By

((Assert  \mkleeneopen{}(e  <loc  x)  \mvee{}  (\mneg{}(loc(x)  =  loc(e)))\mkleeneclose{}\mcdot{}
    THENA  (InstLemma  `eo-strict-forward-E-member`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
    )
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-6)\mcdot{}
              THENA  (Try  ((BLemma  `member-eo-strict-forward-E`
                                        THEN  Auto
                                        THEN  D  (-3)
                                        THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
                                        THEN  D  (-2)
                                        THEN  Auto
                                        THEN  (Assert  \mkleeneopen{}(x  <loc  x1)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                        THEN  FLemma  `es-locl\_transitivity`  [-4;-1]
                                        THEN  Auto))
                            THEN  Auto
                            )
              )
  THEN  D  (-2)
  THEN  D  (-1)
  THEN  Auto
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  OldAutoBoolCase  \mkleeneopen{}loc(e)  =  loc(e1)\mkleeneclose{}\mcdot{}
  THEN  (Assert  \mkleeneopen{}\mneg{}\muparrow{}first(e1)\mkleeneclose{}\mcdot{}
              THENA  (InstLemma  `eo-strict-forward-E-member`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  (D  (-1)  THENA  Auto)
                            THEN  (FLemma  `es-locl-first`  [-1]  THENA  Auto)
                            THEN  HypSubst'  (-1)  0
                            THEN  Auto)
              )
  THEN  (OldAutoSplit  THENA  (Auto  THEN  DoSubsume  THEN  Auto)))

---

Home Index