---

Step * of Lemma is_accum_splitting_wf

∀[T,A:Type]. ∀[L:T List]. ∀[LL:(T List × A) List]. ∀[L2:T List × A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[x:A].
∀[g:(T List × A) ⟶ A].
  (is_accum_splitting(T;A;L;LL;L2;f;g;x) ∈ ℙ)
BY
{ xxx(ProveWfLemma THEN RWO "length-append" 0 THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[L:T  List].  \mforall{}[LL:(T  List  \mtimes{}  A)  List].  \mforall{}[L2:T  List  \mtimes{}  A].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:A].
\mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].
    (is\_accum\_splitting(T;A;L;LL;L2;f;g;x)  \mmember{}  \mBbbP{})


By

---

Latex:
xxx(ProveWfLemma  THEN  RWO  "length-append"  0  THEN  Auto')xxx

---

Home Index