---

Step * of Lemma list-partition_wf

∀T:Type. ∀L:T List. ∀f:ℕ||L|| ⟶ 𝔹.  (list-partition(f;L) ∈ T List × (T List))
BY
{ (InductionOnList
   THEN Unfold `list-partition` 0
   THEN Reduce 0
   THEN Try (Fold `list-partition` 0)
   THEN Try (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L:T  List.  \mforall{}f:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbB{}.    (list-partition(f;L)  \mmember{}  T  List  \mtimes{}  (T  List))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `list-partition`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `list-partition`  0)
  THEN  Try  (ParallelLast)
  THEN  Auto)

---

Home Index