---

Step * 2 1 1 1 of Lemma accum_split_prefix

.....equality..... 
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. v1 : (T List × A) List
9. v3 : T List
10. v4 : A
11. let LL,L2 = <v1, v3, v4> 
    in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
12. accum_split(g;x;f;ys)
= <v1, v3, v4>
∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;ys;LL;L2;f;g;x)} 
13. ¬(v3 = [] ∈ (T List))
14. ↑(f <v3, v4>)
15. (¬↑null(v1)) ⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));v1)))))))
16. ¬↑null(v1 @ [<v3, v4>])
⊢ accum_split(g;x;f;concat(map(λp.(fst(p));v1 @ [<v3, v4>]))) = <v1, v3, v4> ∈ ((T List × A) List × T List × A)
BY
{ xxx((FLemma `accum_split_inverse` [-5] THENA Auto)
      THEN (RWO "map_append_sq" 0 THENM (Reduce 0 THEN RWW "concat_append concat-single" 0))
      THEN Auto)xxx }

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  Type
2.  T  :  Type
3.  x  :  A
4.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
5.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
6.  ys  :  T  List
7.  y  :  T
8.  v1  :  (T  List  \mtimes{}  A)  List
9.  v3  :  T  List
10.  v4  :  A
11.  let  LL,L2  =  <v1,  v3,  v4> 
        in  is\_accum\_splitting(T;A;ys;LL;L2;f;g;x)
12.  accum\_split(g;x;f;ys)  =  <v1,  v3,  v4>
13.  \mneg{}(v3  =  [])
14.  \muparrow{}(f  <v3,  v4>)
15.  (\mneg{}\muparrow{}null(v1))  {}\mRightarrow{}  (\muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));v1)))))))
16.  \mneg{}\muparrow{}null(v1  @  [<v3,  v4>])
\mvdash{}  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));v1  @  [<v3,  v4>])))  =  <v1,  v3,  v4>


By

---

Latex:
xxx((FLemma  `accum\_split\_inverse`  [-5]  THENA  Auto)
        THEN  (RWO  "map\_append\_sq"  0  THENM  (Reduce  0  THEN  RWW  "concat\_append  concat-single"  0))
        THEN  Auto)xxx

---

Home Index