---

Step * of Lemma split_tail_trivial

∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].
  split_tail(L | ∀x.f[x]) = <[], L> ∈ (A List × (A List)) supposing ∀b:A. ((b ∈ L) ⇒ (↑f[b]))
BY
{ (((RepeatFor 3 (D 0 THENA Auto) THEN ListInd (-1)) THEN RecUnfold `split_tail` 0) THEN Reduce 0) }

1
1. A : Type
2. f : A ⟶ 𝔹
⊢ <[], []> = <[], []> ∈ (A List × (A List)) supposing ∀b:A. ((b ∈ []) ⇒ (↑f[b]))

2
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. split_tail(v | ∀x.f[x]) = <[], v> ∈ (A List × (A List)) supposing ∀b:A. ((b ∈ v) ⇒ (↑f[b]))
⊢ let hs,ftail = split_tail(v | ∀x.f[x]) 
  in case hs of [] => if f[u] then <[], [u / ftail]> else <[u], ftail> fi  | x::y => <[u / hs], ftail> esac
  = <[], [u / v]>
  ∈ (A List × (A List)) 
  supposing ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
    split\_tail(L  |  \mforall{}x.f[x])  =  <[],  L>  supposing  \mforall{}b:A.  ((b  \mmember{}  L)  {}\mRightarrow{}  (\muparrow{}f[b]))


By

---

Latex:
(((RepeatFor  3  (D  0  THENA  Auto)  THEN  ListInd  (-1))  THEN  RecUnfold  `split\_tail`  0)  THEN  Reduce  0)

---

Home Index