Step
*
2
of Lemma
split_tail_max
1. [A] : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀a:A. ((a ∈ v) 
⇒ ((a ∈ snd(split_tail(v | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ v 
⇒ (↑f[b]))) and (↑f[a])))
⊢ ∀a:A
    ((a ∈ [u / v])
    
⇒ ((a ∈ 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> es\000Cac))) supposing 
          ((∀b:A. (a before b ∈ [u / v] 
⇒ (↑f[b]))) and 
          (↑f[a])))
BY
{ (Auto THEN GenListD (-3) THEN D (-3)) }
1
1. [A] : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀a:A. ((a ∈ v) 
⇒ ((a ∈ snd(split_tail(v | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ v 
⇒ (↑f[b]))) and (↑f[a])))
6. a : A
7. a = u ∈ A
8. ↑f[a]
9. ∀b:A. (a before b ∈ [u / v] 
⇒ (↑f[b]))
⊢ (a ∈ 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))
2
1. [A] : Type
2. f : A ⟶ 𝔹
3. u : A
4. v : A List
5. ∀a:A. ((a ∈ v) 
⇒ ((a ∈ snd(split_tail(v | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ v 
⇒ (↑f[b]))) and (↑f[a])))
6. a : A
7. (a ∈ v)
8. ↑f[a]
9. ∀b:A. (a before b ∈ [u / v] 
⇒ (↑f[b]))
⊢ (a ∈ 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))
Latex:
Latex:
1.  [A]  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mforall{}a:A
          ((a  \mmember{}  v)
          {}\mRightarrow{}  ((a  \mmember{}  snd(split\_tail(v  |  \mforall{}x.f[x]))))  supposing 
                      ((\mforall{}b:A.  (a  before  b  \mmember{}  v  {}\mRightarrow{}  (\muparrow{}f[b])))  and 
                      (\muparrow{}f[a])))
\mvdash{}  \mforall{}a:A
        ((a  \mmember{}  [u  /  v])
        {}\mRightarrow{}  ((a  \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)))  supposing 
                    ((\mforall{}b:A.  (a  before  b  \mmember{}  [u  /  v]  {}\mRightarrow{}  (\muparrow{}f[b])))  and 
                    (\muparrow{}f[a])))
By
Latex:
(Auto  THEN  GenListD  (-3)  THEN  D  (-3))
Home
Index