---

Step * 2 1 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. ¬↑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)} 
BY
{ (D -1
   THEN RepeatFor 2 ((D -2 THEN All Reduce))
   THEN RepUR ``is_accum_splitting`` -1
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0) }

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. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. firstn(||L|| - 1;L) = (concat(map(λp.(fst(p));v1)) @ v3) ∈ (T List)
13. (∀L'∈v1.(↑(f L'))
        ∧ (¬↑null(fst(L')))
        ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
14. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬↑null(v3))
15. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ v3 ⇒ (¬(S = v3 ∈ (T List))) ⇒ (¬↑(f <S, v4>)))
16. (snd(hd(v1 @ [<v3, v4>]))) = x ∈ A
17. ∀i:ℕ||v1||. ((snd(v1 @ [<v3, v4>][i + 1])) = (g v1[i]) ∈ A)
18. v3 = [] ∈ (T List)
⊢ is_accum_splitting(T;A;firstn(||L|| - 1;L) @ [last(L)];v1;<[last(L)], v4>;f;g;x)

2
.....falsecase..... 
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. v1 : (T List × A) List
10. v3 : T List
11. v4 : A
12. firstn(||L|| - 1;L) = (concat(map(λp.(fst(p));v1)) @ v3) ∈ (T List)
13. (∀L'∈v1.(↑(f L'))
        ∧ (¬↑null(fst(L')))
        ∧ (∀S:T List. ((¬↑null(S)) ⇒ S ≤ fst(L') ⇒ (¬(S = (fst(L')) ∈ (T List))) ⇒ (¬↑(f <S, snd(L')>)))))
14. (¬↑null(firstn(||L|| - 1;L))) ⇒ (¬↑null(v3))
15. ∀S:T List. ((¬↑null(S)) ⇒ S ≤ v3 ⇒ (¬(S = v3 ∈ (T List))) ⇒ (¬↑(f <S, v4>)))
16. (snd(hd(v1 @ [<v3, v4>]))) = x ∈ A
17. ∀i:ℕ||v1||. ((snd(v1 @ [<v3, v4>][i + 1])) = (g v1[i]) ∈ A)
18. ¬(v3 = [] ∈ (T List))
⊢ let LL,L2 = if f <v3, v4> then <v1 @ [<v3, v4>], [last(L)], g <v3, v4>> else <v1, v3 @ [last(L)], v4> fi  
  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.  \mneg{}\muparrow{}null(L)
9.  v  :  \{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{}  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)  \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:
(D  -1
  THEN  RepeatFor  2  ((D  -2  THEN  All  Reduce))
  THEN  RepUR  ``is\_accum\_splitting``  -1
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0)

---

Home Index