---

Step * of Lemma es-hist-is-append

∀[Info:Type]
  ∀es:EO+(Info). ∀e1,e2:E. ∀L1,L2:Info List.
    (∃e∈(e1,e2].(es-hist(es;e1;pred(e)) = L1 ∈ (Info List)) ∧ (es-hist(es;e;e2) = L2 ∈ (Info List))) supposing 
       ((es-hist(es;e1;e2) = (L1 @ L2) ∈ (Info List)) and 
       (¬(L2 = [] ∈ (Info List))) and 
       (¬(L1 = [] ∈ (Info List))))
BY
{ (Auto
   THEN Unfold `es-hist` (-1)⋅
   THEN (Assert ||[e1, e2]|| = (||L1|| + ||L2||) ∈ ℤ BY
               ((Assert ||map(λe.info(e);[e1, e2])|| = (||L1|| + ||L2||) ∈ ℤ BY
                       ((HypSubst (-1) 0) THEN Auto THEN RWO "length-append" 0 THEN Auto))
                THEN (RWO "length-map" (-1))
                THEN Auto))
   THEN AllHyps h.((FLemma `pos_length` [h]) THENA Complete (Auto)) 
   THEN (Assert ∃e∈(e1,e2].||[e1, pred(e)]|| = ||L1|| ∈ ℤ BY
               (BLemma `es-subinterval` THEN Auto' THEN (RWO "es-interval-non-zero" 0 THEN Auto')⋅))) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. L1 : Info List@i
6. L2 : Info List@i
7. ¬(L1 = [] ∈ (Info List))
8. ¬(L2 = [] ∈ (Info List))
9. map(λe.info(e);[e1, e2]) = (L1 @ L2) ∈ (Info List)
10. ||[e1, e2]|| = (||L1|| + ||L2||) ∈ ℤ
11. ||L2|| ≥ 1 
12. ||L1|| ≥ 1 
13. ∃e∈(e1,e2].||[e1, pred(e)]|| = ||L1|| ∈ ℤ
⊢ ∃e∈(e1,e2].(es-hist(es;e1;pred(e)) = L1 ∈ (Info List)) ∧ (es-hist(es;e;e2) = L2 ∈ (Info List))

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}L1,L2:Info  List.
        (\mexists{}e\mmember{}(e1,e2].(es-hist(es;e1;pred(e))  =  L1)  \mwedge{}  (es-hist(es;e;e2)  =  L2))  supposing 
              ((es-hist(es;e1;e2)  =  (L1  @  L2))  and 
              (\mneg{}(L2  =  []))  and 
              (\mneg{}(L1  =  [])))


By

(Auto
  THEN  Unfold  `es-hist`  (-1)\mcdot{}
  THEN  (Assert  ||[e1,  e2]||  =  (||L1||  +  ||L2||)  BY
                          ((Assert  ||map(\mlambda{}e.info(e);[e1,  e2])||  =  (||L1||  +  ||L2||)  BY
                                          ((HypSubst  (-1)  0)  THEN  Auto  THEN  RWO  "length-append"  0  THEN  Auto))
                            THEN  (RWO  "length-map"  (-1))
                            THEN  Auto))
  THEN  AllHyps  h.((FLemma  `pos\_length`  [h])  THENA  Complete  (Auto)) 
  THEN  (Assert  \mexists{}e\mmember{}(e1,e2].||[e1,  pred(e)]||  =  ||L1||  BY
                          (BLemma  `es-subinterval`  THEN  Auto'  THEN  (RWO  "es-interval-non-zero"  0  THEN  Auto')\mcdot{})))

---

Home Index