---

Step * of Lemma accum_split_inverse

∀[A,T:Type]. ∀[x:A]. ∀[g:(T List × A) ⟶ A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[L:T List]. ∀[LL:(T List × A) List]. ∀[X:T List].
∀[z:A].
  L = (concat(map(λp.(fst(p));LL)) @ X) ∈ (T List) 
  supposing accum_split(g;x;f;L) = <LL, X, z> ∈ ((T List × A) List × T List × A)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;2]
   THEN Auto
   THEN D -3
   THEN RepeatFor 2 (D -4)
   THEN All Reduce
   THEN AutoSimpHyp Auto (-1)
   THEN D -5
   THEN Auto) }

---

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{}[LL:(T  List  \mtimes{}  A)  List].  \mforall{}[X:T  List].  \mforall{}[z:A].
    L  =  (concat(map(\mlambda{}p.(fst(p));LL))  @  X)  supposing  accum\_split(g;x;f;L)  =  <LL,  X,  z>


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;2]
  THEN  Auto
  THEN  D  -3
  THEN  RepeatFor  2  (D  -4)
  THEN  All  Reduce
  THEN  AutoSimpHyp  Auto  (-1)
  THEN  D  -5
  THEN  Auto)

---

Home Index