---

Step * 1 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. ZZ : (T List × A) List
7. Z : T List × A
8. X : T List × A
9. accum_split(g;x;f;[]) = <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
{ ((RepUR ``accum_split`` -1 THEN Auto) THEN AutoSimpHyp Auto (-1) THEN AutoSimpHyp Auto (-2) THEN Auto) }

---

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.  ZZ  :  (T  List  \mtimes{}  A)  List
7.  Z  :  T  List  \mtimes{}  A
8.  X  :  T  List  \mtimes{}  A
9.  accum\_split(g;x;f;[])  =  <ZZ  @  [Z],  X>
\mvdash{}  accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ  @  [Z])))  =  <ZZ,  Z>


By

---

Latex:
((RepUR  ``accum\_split``  -1  THEN  Auto)
  THEN  AutoSimpHyp  Auto  (-1)
  THEN  AutoSimpHyp  Auto  (-2)
  THEN  Auto)

---

Home Index