---

Step * 2 of Lemma split_tail_trivial


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]))
BY
{ (ParallelOp (-1)) }

1
.....antecedent..... 
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))
⊢ ∀b:A. ((b ∈ v) ⇒ (↑f[b]))

2
1. A : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀b:A. ((b ∈ [u / v]) ⇒ (↑f[b]))
6. split_tail(v | ∀x.f[x]) = <[], v> ∈ (A List × (A List))
⊢ 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))

---

Latex:

---

Latex:

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


By

---

Latex:
(ParallelOp  (-1))

---

Home Index