---

Step * 2 of Lemma split_tail_rel


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)
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 AutoSplit) }

1
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. p1 : A List
6. p2 : A List
7. ↑f[u]
⊢ ((p1 @ p2) = v ∈ (A List))
⇒ (((fst(case p1 of [] => <[], [u / p2]> | x::y => <[u / p1], p2> esac)) @ (snd(case p1 of [] => <[], [u / p2]> | x::y \000C=> <[u / p1], p2> esac))) = [u / v] ∈ (A List))

2
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. ¬↑f[u]
5. v : A List
6. p1 : A List
7. p2 : A List
⊢ ((p1 @ p2) = v ∈ (A List))
⇒ (((fst(case p1 of [] => <[u], p2> | x::y => <[u / p1], p2> esac)) @ (snd(case p1 of [] => <[u], p2> | x::y => <[u / p\000C1], p2> esac))) = [u / v] ∈ (A List))

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  ((fst(split\_tail(v  |  \mforall{}x.f[x])))  @  (snd(split\_tail(v  |  \mforall{}x.f[x]))))  =  v
\mvdash{}  ((fst(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))
@  (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)))
=  [u  /  v]


By

---

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

---

Home Index