---

Step * 1 of Lemma list_split_iseg


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))
BY
{ xxx(D 5
      THEN (Assert list_split(f;L1 @ l) = <v3, v4> ∈ (T List List × (T List)) BY
                  Auto)
      THEN Unfold `list_split` -1
      THEN (RWO "list_accum_append" (-1) THENA Auto)
      THEN Fold `list_split` (-1)
      THEN (Subst' list_split(f;L1) = <v1, v2> ∈ (T List List × (T List)) -1 THENA Auto))xxx }

1
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. L1 : T List
4. L2 : T List
5. l : T List
6. L2 = (L1 @ l) ∈ (T List)
7. v1 : T List List
8. v2 : T List
9. list_split(f;L1) = <v1, v2> ∈ (T List List × (T List))
10. v3 : T List List
11. v4 : T List
12. list_split(f;L2) = <v3, v4> ∈ (T List List × (T List))
13. accumulate (with value p and list item v):
     let LL,L2 = p 
     in if null(L2) then <LL, [v]>
        if f L2 then <LL @ [L2], [v]>
        else <LL, L2 @ [v]>
        fi 
    over list:
      l
    with starting value:
     <v1, v2>)
= <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:

1.  [T]  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  L1  :  T  List
4.  L2  :  T  List
5.  L1  \mleq{}  L2
6.  v1  :  T  List  List
7.  v2  :  T  List
8.  list\_split(f;L1)  =  <v1,  v2>
9.  v3  :  T  List  List
10.  v4  :  T  List
11.  list\_split(f;L2)  =  <v3,  v4>
\mvdash{}  ((v1  =  v3)  \mwedge{}  v2  \mleq{}  v4)  \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((v1  @  [Z  /  ZZ])  =  v3)  \mwedge{}  v2  \mleq{}  Z))


By

---

Latex:
xxx(D  5
        THEN  (Assert  list\_split(f;L1  @  l)  =  <v3,  v4>  BY
                                Auto)
        THEN  Unfold  `list\_split`  -1
        THEN  (RWO  "list\_accum\_append"  (-1)  THENA  Auto)
        THEN  Fold  `list\_split`  (-1)
        THEN  (Subst'  list\_split(f;L1)  =  <v1,  v2>  -1  THENA  Auto))xxx

---

Home Index