---

Step * 1 of Lemma accum_split_iseg


1. [T] : Type
2. [A] : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. L1 : T List
7. L2 : T List
8. L1 ≤ L2
9. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. accum_split(g;x;f;L1) = <v1, v3, v4> ∈ ((T List × A) List × T List × A)
13. v5 : (T List × A) List
14. v7 : T List
15. v8 : A
16. accum_split(g;x;f;L2) = <v5, v7, v8> ∈ ((T List × A) List × T List × A)
⊢ ((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
BY
{ (D 8
   THEN (Assert accum_split(g;x;f;L1 @ l) = <v5, v7, v8> ∈ ((T List × A) List × T List × A) BY
               Auto)
   THEN Unfold `accum_split` -1
   THEN (RWO "list_accum_append" (-1) THENA Auto)
   THEN Fold `accum_split` (-1)
   THEN (Subst' accum_split(g;x;f;L1) = <v1, v3, v4> ∈ ((T List × A) List × T List × A) -1 THENA Auto)) }

1
1. [T] : Type
2. [A] : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. L1 : T List
7. L2 : T List
8. l : T List
9. L2 = (L1 @ l) ∈ (T List)
10. v1 : (T List × A) List
11. v3 : T List
12. v4 : A
13. accum_split(g;x;f;L1) = <v1, v3, v4> ∈ ((T List × A) List × T List × A)
14. v5 : (T List × A) List
15. v7 : T List
16. v8 : A
17. accum_split(g;x;f;L2) = <v5, v7, v8> ∈ ((T List × A) List × T List × A)
18. accumulate (with value p and list item v):
     let LL,L2,z = p in 
     if null(L2) then <LL, [v], z>
     if f <L2, z> then <LL @ [<L2, z>], [v], g <L2, z>>
     else <LL, L2 @ [v], z>
     fi 
    over list:
      l
    with starting value:
     <v1, v3, v4>)
= <v5, v7, v8>
∈ ((T List × A) List × T List × A)
⊢ ((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  x  :  A
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
6.  L1  :  T  List
7.  L2  :  T  List
8.  L1  \mleq{}  L2
9.  v1  :  (T  List  \mtimes{}  A)  List
10.  v3  :  T  List
11.  v4  :  A
12.  accum\_split(g;x;f;L1)  =  <v1,  v3,  v4>
13.  v5  :  (T  List  \mtimes{}  A)  List
14.  v7  :  T  List
15.  v8  :  A
16.  accum\_split(g;x;f;L2)  =  <v5,  v7,  v8>
\mvdash{}  ((v1  =  v5)  \mwedge{}  v3  \mleq{}  v7  \mwedge{}  (v4  =  v8))
\mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((v1  @  [<Z,  v4>  /  ZZ])  =  v5)  \mwedge{}  v3  \mleq{}  Z))


By

---

Latex:
(D  8
  THEN  (Assert  accum\_split(g;x;f;L1  @  l)  =  <v5,  v7,  v8>  BY
                          Auto)
  THEN  Unfold  `accum\_split`  -1
  THEN  (RWO  "list\_accum\_append"  (-1)  THENA  Auto)
  THEN  Fold  `accum\_split`  (-1)
  THEN  (Subst'  accum\_split(g;x;f;L1)  =  <v1,  v3,  v4>  -1  THENA  Auto))

---

Home Index