---

Step * 1 2 1 of Lemma eo-strict-forward-before


1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. e ∈ E
8. loc(e) = loc(b) ∈ Id
9. ¬↑first(e)
10. ¬(pred(e) = b ∈ E)
11. before(pred(e)) = (b, pred(e)) ∈ (E List)
⊢ (before(pred(e)) @ [pred(e)]) = (b, e) ∈ (E List)
BY
{ ((Assert ⌈pred(e) ∈ E⌉⋅
    THENA ((BLemma `member-eo-strict-forward-E` THEN Auto)
           THEN InstLemma `es-pred_property` [⌈es⌉;⌈e⌉]⋅
           THEN Auto
           THEN (InstHyp [⌈b⌉] (-1)⋅ THENA Auto)
           THEN D (-1)
           THEN Auto)
    )
   THEN (Assert ⌈¬↑first(e)⌉⋅
         THENA ((D 0 THENA Auto)
                THEN (RWO "eo-strict-forward-first" (-1) THENA Auto)
                THEN SplitOnHypITE (-1)
                THEN Auto
                THEN D (-5)
                THEN (RWO "assert-es-eq-E" 0 THENA Auto)
                THEN RepUR ``es-eq-E eqof`` 0
                THEN Auto)
         )
   THEN (InstLemma `eo-strict-forward-E-subtype` [⌈Info⌉;⌈es⌉;⌈b⌉]⋅ THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. e ∈ E
8. loc(e) = loc(b) ∈ Id
9. ¬↑first(e)
10. ¬(pred(e) = b ∈ E)
11. before(pred(e)) = (b, pred(e)) ∈ (E List)
12. pred(e) ∈ E
13. ¬↑first(e)
14. E ⊆r E
⊢ (before(pred(e)) @ [pred(e)]) = (b, e) ∈ (E List)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E@i
4.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\mforall{}b:E.  ((b  <loc  e1)  {}\mRightarrow{}  (before(e1)  =  (b,  e1)))))
5.  b  :  E@i
6.  (b  <loc  e)@i
7.  e  \mmember{}  E
8.  loc(e)  =  loc(b)
9.  \mneg{}\muparrow{}first(e)
10.  \mneg{}(pred(e)  =  b)
11.  before(pred(e))  =  (b,  pred(e))
\mvdash{}  (before(pred(e))  @  [pred(e)])  =  (b,  e)


By

((Assert  \mkleeneopen{}pred(e)  \mmember{}  E\mkleeneclose{}\mcdot{}
    THENA  ((BLemma  `member-eo-strict-forward-E`  THEN  Auto)
                  THEN  InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
                  THEN  Auto
                  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                  THEN  D  (-1)
                  THEN  Auto)
    )
  THEN  (Assert  \mkleeneopen{}\mneg{}\muparrow{}first(e)\mkleeneclose{}\mcdot{}
              THENA  ((D  0  THENA  Auto)
                            THEN  (RWO  "eo-strict-forward-first"  (-1)  THENA  Auto)
                            THEN  SplitOnHypITE  (-1)
                            THEN  Auto
                            THEN  D  (-5)
                            THEN  (RWO  "assert-es-eq-E"  0  THENA  Auto)
                            THEN  RepUR  ``es-eq-E  eqof``  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `eo-strict-forward-E-subtype`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index