---

Step * 2 1 of Lemma accum_split_wf


1. A : Type
2. T : Type
3. f : (T List × A) ⟶ 𝔹
4. g : (T List × A) ⟶ A
5. x : A
6. n : ℕ
7. L : T List
8. ∀L1:T List
     (||L1|| < ||L||
     ⇒ (accum_split(g;x;f;L1) ∈ {p:(T List × A) List × T List × A| 
                                  let LL,L2 = p 
                                  in is_accum_splitting(T;A;L1;LL;L2;f;g;x)} ))
9. ¬↑null(L)
10. accum_split(g;x;f;firstn(||L|| - 1;L)) ∈ {p:(T List × A) List × T List × A| 
                                              let LL,L2 = p 
                                              in is_accum_splitting(T;A;firstn(||L|| - 1;L);LL;L2;f;g;x)} 
⊢ accum_split(g;x;f;firstn(||L|| - 1;L) @ [last(L)]) ∈ {p:(T List × A) List × T List × A| 
                                                        let LL,L2 = p 
                                                        in is_accum_splitting(T;A;firstn(||L|| - 1;L)
                                                           @ [last(L)];LL;L2;f;g;x)} 
BY
{ (Thin (-3)
   THEN All (Unfold `accum_split`)
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN GenConclAtAddr [2;2]
   THEN Thin (-1)
   THEN Thin (-2)) }

1
1. A : Type
2. T : Type
3. f : (T List × A) ⟶ 𝔹
4. g : (T List × A) ⟶ A
5. x : A
6. n : ℕ
7. L : T List
8. ¬↑null(L)
9. v : {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;firstn(||L|| - 1;L);LL;L2;f;g;x)} 
⊢ 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:
    [last(L)]
  with starting value:
   v) ∈ {p:(T List × A) List × T List × A| 
         let LL,L2 = p 
         in is_accum_splitting(T;A;firstn(||L|| - 1;L) @ [last(L)];LL;L2;f;g;x)} 

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  x  :  A
6.  n  :  \mBbbN{}
7.  L  :  T  List
8.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\mRightarrow{}  (accum\_split(g;x;f;L1)  \mmember{}  \{p:(T  List  \mtimes{}  A)  List  \mtimes{}  T  List  \mtimes{}  A| 
                                                                    let  LL,L2  =  p 
                                                                    in  is\_accum\_splitting(T;A;L1;LL;L2;f;g;x)\}  ))
9.  \mneg{}\muparrow{}null(L)
10.  accum\_split(g;x;f;firstn(||L||  -  1;L))  \mmember{}  \{p:(T  List  \mtimes{}  A)  List  \mtimes{}  T  List  \mtimes{}  A| 
                                                                                            let  LL,L2  =  p 
                                                                                            in  is\_accum\_splitting(T;A;firstn(||L|| 
                                                                                                  -  1;L);LL;L2;f;g;x)\} 
\mvdash{}  accum\_split(g;x;f;firstn(||L||  -  1;L)  @  [last(L)])  \mmember{}  \{p:(T  List  \mtimes{}  A)  List  \mtimes{}  T  List  \mtimes{}  A| 
                                                                                                                let  LL,L2  =  p 
                                                                                                                in  is\_accum\_splitting(T;A;firstn(||L|| 
                                                                                                                      -  1;L)
                                                                                                                      @  [last(L)];LL;L2;f;g;x)\} 


By

---

Latex:
(Thin  (-3)
  THEN  All  (Unfold  `accum\_split`)
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  GenConclAtAddr  [2;2]
  THEN  Thin  (-1)
  THEN  Thin  (-2))

---

Home Index