---

Step * of Lemma list_split_iseg2

∀[T:Type]
  ∀f:(T List) ⟶ 𝔹. ∀L1,L2:T List.
    (L1 ≤ L2
    ⇒ (∀LL1,LL2:T List List. ∀X,Y:T List.
          (((LL1 = LL2 ∈ (T List List)) ∧ X ≤ Y)
             ∨ (∃Z:T List. ∃ZZ:T List List. (((LL1 @ [Z / ZZ]) = LL2 ∈ (T List List)) ∧ X ≤ Z))) supposing 
             ((list_split(f;L2) = <LL2, Y> ∈ (T List List × (T List))) and 
             (list_split(f;L1) = <LL1, X> ∈ (T List List × (T List))))))
BY
{ xxx(InstLemma `list_split_iseg` []
      THEN RepeatFor 5 (ParallelLast')
      THEN Auto
      THEN (HypSubst' (-1) 6 THENA Auto)
      THEN Reduce (-1)
      THEN (HypSubst' (-3) (-1) THENA Auto)
      THEN Reduce (-1)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:(T  List)  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L1,L2:T  List.
        (L1  \mleq{}  L2
        {}\mRightarrow{}  (\mforall{}LL1,LL2:T  List  List.  \mforall{}X,Y:T  List.
                    (((LL1  =  LL2)  \mwedge{}  X  \mleq{}  Y)
                          \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((LL1  @  [Z  /  ZZ])  =  LL2)  \mwedge{}  X  \mleq{}  Z)))  supposing 
                          ((list\_split(f;L2)  =  <LL2,  Y>)  and 
                          (list\_split(f;L1)  =  <LL1,  X>))))


By

---

Latex:
xxx(InstLemma  `list\_split\_iseg`  []
        THEN  RepeatFor  5  (ParallelLast')
        THEN  Auto
        THEN  (HypSubst'  (-1)  6  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  (HypSubst'  (-3)  (-1)  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  Auto)xxx

---

Home Index