Step
*
of Lemma
split_tail_max
∀[A:Type]
  ∀f:A ⟶ 𝔹. ∀L:A List. ∀a:A.
    ((a ∈ L) 
⇒ ((a ∈ snd(split_tail(L | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ L 
⇒ (↑f[b]))) and (↑f[a])))
BY
{ (((RepeatFor 3 (D 0 THENA Auto) THEN ListInd (-1)) THEN RecUnfold `split_tail` 0) THEN Reduce 0) }
1
1. [A] : Type
2. f : A ⟶ 𝔹
⊢ ∀a:A. ((a ∈ []) 
⇒ ((a ∈ [])) supposing ((∀b:A. (a before b ∈ [] 
⇒ (↑f[b]))) and (↑f[a])))
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])))
⊢ ∀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])))
Latex:
Latex:
\mforall{}[A:Type]
    \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.  \mforall{}a:A.
        ((a  \mmember{}  L)
        {}\mRightarrow{}  ((a  \mmember{}  snd(split\_tail(L  |  \mforall{}x.f[x]))))  supposing 
                    ((\mforall{}b:A.  (a  before  b  \mmember{}  L  {}\mRightarrow{}  (\muparrow{}f[b])))  and 
                    (\muparrow{}f[a])))
By
Latex:
(((RepeatFor  3  (D  0  THENA  Auto)  THEN  ListInd  (-1))  THEN  RecUnfold  `split\_tail`  0)  THEN  Reduce  0)
Home
Index