---

Step * of Lemma list_split_wf

∀[T:Type]. ∀[f:(T List) ⟶ 𝔹]. ∀[L:T List].
  (list_split(f;L) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;L;LL;L2;f)} )
BY
{ (InductionOnLength THEN (Decide ↑null(L) THENA Auto)) }

1
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ∀L1:T List
     (||L1|| < ||L||
     ⇒ (list_split(f;L1) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;L1;LL;L2;f)} ))
6. ↑null(L)
⊢ list_split(f;L) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;L;LL;L2;f)} 

2
1. T : Type
2. f : (T List) ⟶ 𝔹
3. n : ℕ
4. L : T List
5. ∀L1:T List
     (||L1|| < ||L||
     ⇒ (list_split(f;L1) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;L1;LL;L2;f)} ))
6. ¬↑null(L)
⊢ list_split(f;L) ∈ {p:T List List × (T List)| let LL,L2 = p in is_list_splitting(T;L;LL;L2;f)} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:(T  List)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    (list\_split(f;L)  \mmember{}  \{p:T  List  List  \mtimes{}  (T  List)|  let  LL,L2  =  p  in  is\_list\_splitting(T;L;LL;L2;f)\}  )


By

---

Latex:
(InductionOnLength  THEN  (Decide  \muparrow{}null(L)  THENA  Auto))

---

Home Index