---

Step * of Lemma list_split_iseg

∀[T:Type]
  ∀f:(T List) ⟶ 𝔹. ∀L1,L2:T List.
    (L1 ≤ L2
    ⇒ let LL1,X = list_split(f;L1) 
       in let LL2,Y = list_split(f;L2) 
          in ((LL1 = LL2 ∈ (T List List)) ∧ X ≤ Y)
             ∨ (∃Z:T List. ∃ZZ:T List List. (((LL1 @ [Z / ZZ]) = LL2 ∈ (T List List)) ∧ X ≤ Z)))
BY
{ xxx(Auto
      THEN RepeatFor 2 ((GenConclAtAddr [1] THEN D -2 THEN D -3 THEN All Reduce))
      THEN Thin (-2)
      THEN Thin (-5)
      THEN ∀h:hyp. ((EqTypeHD h THENM Thin (h+1)) THENA Auto) )xxx }

1
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. L1 : T List
4. L2 : T List
5. L1 ≤ L2
6. v1 : T List List
7. v2 : T List
8. list_split(f;L1) = <v1, v2> ∈ (T List List × (T List))
9. v3 : T List List
10. v4 : T List
11. list_split(f;L2) = <v3, v4> ∈ (T List List × (T List))
⊢ ((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z))

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  RepeatFor  2  ((GenConclAtAddr  [1]  THEN  D  -2  THEN  D  -3  THEN  All  Reduce))
        THEN  Thin  (-2)
        THEN  Thin  (-5)
        THEN  \mforall{}h:hyp.  ((EqTypeHD  h  THENM  Thin  (h+1))  THENA  Auto)  )xxx

---

Home Index