---

Step * 3 of Lemma split_tail_lemma


1. A : Type
2. f : A ⟶ 𝔹
3. L : A List
4. a : A
5. (a ∈ L)
6. ↑f[a]
7. ∀b:A. (a before b ∈ L ⇒ (↑f[b]))
8. L = ((fst(split_tail(L | ∀x.f[x]))) @ (snd(split_tail(L | ∀x.f[x])))) ∈ (A List)
9. (a ∈ snd(split_tail(L | ∀x.f[x])))
10. ∀b:A. ((b ∈ snd(split_tail(L | ∀x.f[x]))) ⇒ (↑f[b]))
11. ¬↑null(fst(split_tail(L | ∀x.f[x])))
⊢ ¬↑f[last(fst(split_tail(L | ∀x.f[x])))]
BY
{ (((MoveToConcl (-1) THEN AllHyps Thin) THEN ListInd 3)
   THEN RecUnfold `split_tail` 0
   THEN Reduce 0
   THEN SimpConcl
   THEN 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]
⊢ ((¬↑null(p1)) ⇒ (¬↑f[last(p1)]))
⇒ (¬↑null(fst(case p1 of [] => <[], [u / p2]> | x::y => <[u / p1], p2> esac)))
⇒ (¬↑f[last(fst(case p1 of [] => <[], [u / p2]> | x::y => <[u / p1], p2> esac))])

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
⊢ ((¬↑null(p1)) ⇒ (¬↑f[last(p1)]))
⇒ (¬↑null(fst(case p1 of [] => <[u], p2> | x::y => <[u / p1], p2> esac)))
⇒ (¬↑f[last(fst(case p1 of [] => <[u], p2> | x::y => <[u / p1], p2> esac))])

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbB{}
3.  L  :  A  List
4.  a  :  A
5.  (a  \mmember{}  L)
6.  \muparrow{}f[a]
7.  \mforall{}b:A.  (a  before  b  \mmember{}  L  {}\mRightarrow{}  (\muparrow{}f[b]))
8.  L  =  ((fst(split\_tail(L  |  \mforall{}x.f[x])))  @  (snd(split\_tail(L  |  \mforall{}x.f[x]))))
9.  (a  \mmember{}  snd(split\_tail(L  |  \mforall{}x.f[x])))
10.  \mforall{}b:A.  ((b  \mmember{}  snd(split\_tail(L  |  \mforall{}x.f[x])))  {}\mRightarrow{}  (\muparrow{}f[b]))
11.  \mneg{}\muparrow{}null(fst(split\_tail(L  |  \mforall{}x.f[x])))
\mvdash{}  \mneg{}\muparrow{}f[last(fst(split\_tail(L  |  \mforall{}x.f[x])))]


By

---

Latex:
(((MoveToConcl  (-1)  THEN  AllHyps  Thin)  THEN  ListInd  3)
  THEN  RecUnfold  `split\_tail`  0
  THEN  Reduce  0
  THEN  SimpConcl
  THEN  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