---

Step * 2 1 1 of Lemma accum_split_prefix


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>])
⊢ ↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));v1 @ [<v3, v4>]))))))
BY
{ xxx((Subst' accum_split(g;x;f;concat(map(λp.(fst(p));v1 @ [<v3, v4>])))
       = <v1, v3, v4>
       ∈ ((T List × A) List × T List × A) 0
       THENA Auto
       )
      THEN Reduce 0
      THEN Auto)xxx }

1
.....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)

---

Latex:

---

Latex:

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{}  \muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));v1  @  [<v3,  v4>]))))))


By

---

Latex:
xxx((Subst'  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));v1  @  [<v3,  v4>])))  =  <v1,  v3,  v4>  0  THENA  Auto)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index