---

Step * 2 1 1 2 1 1 1 of Lemma accum_split_prefix2

.....truecase..... 
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. ∀ZZ:(T List × A) List. ∀Z,X:T List × A.
     ((accum_split(g;x;f;ys) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A))
     ⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)))
9. ZZ : (T List × A) List
10. Z : T List × A
11. X : T List × A
12. v1 : (T List × A) List
13. v3 : T List
14. v4 : A
15. let LL,L2 = <v1, v3, v4> 
    in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
16. 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)} 
17. ¬↑null(v1)
18. L' : (T List × A) List
19. v1 = (L' @ [last(v1)]) ∈ ((T List × A) List)
20. <v1, [y], v4> = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A)
21. accum_split(g;x;f;concat(map(λp.(fst(p));L' @ [last(v1)]))) = <L', last(v1)> ∈ ((T List × A) List × T List × A)
22. v3 = [] ∈ (T List)
⊢ accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)
BY
{ AutoSimpHyp Auto (-3) }

1
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. ∀ZZ:(T List × A) List. ∀Z,X:T List × A.
     ((accum_split(g;x;f;ys) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A))
     ⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)))
9. ZZ : (T List × A) List
10. Z : T List × A
11. X : T List × A
12. v1 : (T List × A) List
13. v3 : T List
14. v4 : A
15. let LL,L2 = <v1, v3, v4> 
    in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
16. 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)} 
17. ¬↑null(v1)
18. L' : (T List × A) List
19. v1 = (L' @ [last(v1)]) ∈ ((T List × A) List)
20. v1 = (ZZ @ [Z]) ∈ ((T List × A) List)
21. <[y], v4> = X ∈ (T List × A)
22. accum_split(g;x;f;concat(map(λp.(fst(p));L' @ [last(v1)]))) = <L', last(v1)> ∈ ((T List × A) List × T List × A)
23. v3 = [] ∈ (T List)
⊢ accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)

---

Latex:

---

Latex:
.....truecase..... 
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.  \mforall{}ZZ:(T  List  \mtimes{}  A)  List.  \mforall{}Z,X:T  List  \mtimes{}  A.
          ((accum\_split(g;x;f;ys)  =  <ZZ  @  [Z],  X>)
          {}\mRightarrow{}  (accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ  @  [Z])))  =  <ZZ,  Z>))
9.  ZZ  :  (T  List  \mtimes{}  A)  List
10.  Z  :  T  List  \mtimes{}  A
11.  X  :  T  List  \mtimes{}  A
12.  v1  :  (T  List  \mtimes{}  A)  List
13.  v3  :  T  List
14.  v4  :  A
15.  let  LL,L2  =  <v1,  v3,  v4> 
        in  is\_accum\_splitting(T;A;ys;LL;L2;f;g;x)
16.  accum\_split(g;x;f;ys)  =  <v1,  v3,  v4>
17.  \mneg{}\muparrow{}null(v1)
18.  L'  :  (T  List  \mtimes{}  A)  List
19.  v1  =  (L'  @  [last(v1)])
20.  <v1,  [y],  v4>  =  <ZZ  @  [Z],  X>
21.  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));L'  @  [last(v1)])))  =  <L',  last(v1)>
22.  v3  =  []
\mvdash{}  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ  @  [Z])))  =  <ZZ,  Z>


By

---

Latex:
AutoSimpHyp  Auto  (-3)

---

Home Index