---

Step * of Lemma accum_split_prefix2

∀[A,T:Type]. ∀[x:A]. ∀[g:(T List × A) ⟶ A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[L:T List]. ∀[ZZ:(T List × A) List].
∀[Z,X:T List × A].
  accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A) 
  supposing accum_split(g;x;f;L) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A)
BY
{ xxx(Auto THEN RepeatFor 5 (MoveToConcl (-1)) THEN BLemma `last_induction` THEN Auto)xxx }

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

2
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)

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[x:A].  \mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
\mforall{}[ZZ:(T  List  \mtimes{}  A)  List].  \mforall{}[Z,X:T  List  \mtimes{}  A].
    accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ  @  [Z])))  =  <ZZ,  Z> 
    supposing  accum\_split(g;x;f;L)  =  <ZZ  @  [Z],  X>


By

---

Latex:
xxx(Auto  THEN  RepeatFor  5  (MoveToConcl  (-1))  THEN  BLemma  `last\_induction`  THEN  Auto)xxx

---

Home Index