---

Step * 2 of Lemma accum_split_prefix2


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. accum_split(g;x;f;ys @ [y]) = <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)
BY
{ xxx(Unfold `accum_split` -1
      THEN (RWO "list_accum_append" (-1) THENA Auto)
      THEN Fold `accum_split` (-1)
      THEN Reduce (-1))xxx }

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. let LL,L2,z = accum_split(g;x;f;ys) in 
if null(L2) then <LL, [y], z>
if f <L2, z> then <LL @ [<L2, z>], [y], g <L2, z>>
else <LL, L2 @ [y], z>
fi 
= <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)

---

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.  \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.  accum\_split(g;x;f;ys  @  [y])  =  <ZZ  @  [Z],  X>
\mvdash{}  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ  @  [Z])))  =  <ZZ,  Z>


By

---

Latex:
xxx(Unfold  `accum\_split`  -1
        THEN  (RWO  "list\_accum\_append"  (-1)  THENA  Auto)
        THEN  Fold  `accum\_split`  (-1)
        THEN  Reduce  (-1))xxx

---

Home Index