---

Step * 1 1 of Lemma list_split_iseg


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))
BY
{ xxx(MoveToConcl (-1) THEN All Thin)xxx }

1
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. l : T List
4. v1 : T List List
5. v2 : T List
6. v3 : T List List
7. v4 : T List
⊢ (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.  l  :  T  List
6.  L2  =  (L1  @  l)
7.  v1  :  T  List  List
8.  v2  :  T  List
9.  list\_split(f;L1)  =  <v1,  v2>
10.  v3  :  T  List  List
11.  v4  :  T  List
12.  list\_split(f;L2)  =  <v3,  v4>
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>
\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(MoveToConcl  (-1)  THEN  All  Thin)xxx

---

Home Index