---

Step * of Lemma split_tail_rel

∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].  (((fst(split_tail(L | ∀x.f[x]))) @ (snd(split_tail(L | ∀x.f[x])))) = L ∈ (A List))
BY
{ (((Auto THEN ListInd (-1)) THEN RecUnfold `split_tail` 0) THEN Reduce 0) }

1
1. A : Type
2. f : A ⟶ 𝔹
⊢ [] = [] ∈ (A List)

2
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ((fst(split_tail(v | ∀x.f[x]))) @ (snd(split_tail(v | ∀x.f[x])))) = v ∈ (A List)
⊢ ((fst(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))
@ (snd(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)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
    (((fst(split\_tail(L  |  \mforall{}x.f[x])))  @  (snd(split\_tail(L  |  \mforall{}x.f[x]))))  =  L)


By

---

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

---

Home Index