---

Step * 2 of Lemma split_tail_correct


1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. (∀b∈snd(split_tail(v | ∀x.f[x])).↑f[b])
⊢ (∀b∈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).↑f[\000Cb])
BY
{ ((((((MoveToConcl (-1)) THEN GenConcl split_tail(v | ∀x.f[x]) = p ∈ (A List × (A List))⋅) THENA Auto)
     THEN (Thin (-1))
     THEN (D (-1))
     THEN Reduce 0
     THEN SplitOnConclITE)
    THENA Auto
    )
   THEN (ListInd (-3))
   THEN Reduce 0
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto))) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  (\mforall{}b\mmember{}snd(split\_tail(v  |  \mforall{}x.f[x])).\muparrow{}f[b])
\mvdash{}  (\mforall{}b\mmember{}snd(let  hs,ftail  =  split\_tail(v  |  \mforall{}x.f[x]) 
                    in  case  hs  of 
                              []  =>  if  f[u]  then  <[],  [u  /  ftail]>  else  <[u],  ftail>  fi   
                              x::y  =>
                                <[u  /  hs],  ftail> 
                          esac).\muparrow{}f[b])


By

---

Latex:
((((((MoveToConcl  (-1))  THEN  GenConcl  split\_tail(v  |  \mforall{}x.f[x])  =  p\mcdot{})  THENA  Auto)
      THEN  (Thin  (-1))
      THEN  (D  (-1))
      THEN  Reduce  0
      THEN  SplitOnConclITE)
    THENA  Auto
    )
  THEN  (ListInd  (-3))
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index