---

Step * 1 of Lemma accum_split_prefix


1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
⊢ (¬↑null(fst(accum_split(g;x;f;[]))))
⇒ (↑(f (snd(accum_split(g;x;f;concat(map(λp.(fst(p));fst(accum_split(g;x;f;[])))))))))
BY
{ (Unfold `accum_split` 0 THEN Reduce 0 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{}
\mvdash{}  (\mneg{}\muparrow{}null(fst(accum\_split(g;x;f;[]))))
{}\mRightarrow{}  (\muparrow{}(f  (snd(accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));fst(accum\_split(g;x;f;[])))))))))


By

---

Latex:
(Unfold  `accum\_split`  0  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index