---

Step * 2 1 1 of Lemma split_tail_max

.....equality..... 
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]))
⊢ split_tail(v | ∀x.f[x]) = <[], v> ∈ (A List × (A List))
BY
{ (BackThruLemma `split_tail_trivial` THEN Auto) }

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]))
10. b : A
11. (b ∈ v)
⊢ ↑f[b]

---

Latex:

---

Latex:
.....equality..... 
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])))
6.  a  :  A
7.  a  =  u
8.  \muparrow{}f[a]
9.  \mforall{}b:A.  (a  before  b  \mmember{}  [u  /  v]  {}\mRightarrow{}  (\muparrow{}f[b]))
\mvdash{}  split\_tail(v  |  \mforall{}x.f[x])  =  <[],  v>


By

---

Latex:
(BackThruLemma  `split\_tail\_trivial`  THEN  Auto)

---

Home Index