---

Step * of Lemma split_tail_lemma

∀[A:Type]
  ∀f:A ⟶ 𝔹. ∀L:A List.
    (∀a∈L.∃L1,L2:A List. (((L = (L1 @ L2) ∈ (A List)) ∧ (a ∈ L2) ∧ (∀b∈L2.↑f[b])) ∧ ¬↑f[last(L1)] supposing ¬↑null(L1)) 
          supposing (∀b≥a∈L.↑f[b]))
BY
{ ((Auto THEN (BLemma `l_all_iff` THENA Auto))
   THEN Auto
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN Unfold `l_all_since` -1
   THEN Auto
   THEN InstConcl [fst(split_tail(L | ∀x.f[x]));snd(split_tail(L | ∀x.f[x]))]
   THEN Auto) }

1
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)
⊢ (a ∈ snd(split_tail(L | ∀x.f[x])))

2
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
11. (b ∈ snd(split_tail(L | ∀x.f[x])))
⊢ ↑f[b]

3
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])))]

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.
        (\mforall{}a\mmember{}L.\mexists{}L1,L2:A  List
                      (((L  =  (L1  @  L2))  \mwedge{}  (a  \mmember{}  L2)  \mwedge{}  (\mforall{}b\mmember{}L2.\muparrow{}f[b]))  \mwedge{}  \mneg{}\muparrow{}f[last(L1)]  supposing  \mneg{}\muparrow{}null(L1)) 
                    supposing  (\mforall{}b\mgeq{}a\mmember{}L.\muparrow{}f[b]))


By

---

Latex:
((Auto  THEN  (BLemma  `l\_all\_iff`  THENA  Auto))
  THEN  Auto
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  Unfold  `l\_all\_since`  -1
  THEN  Auto
  THEN  InstConcl  [fst(split\_tail(L  |  \mforall{}x.f[x]));snd(split\_tail(L  |  \mforall{}x.f[x]))]
  THEN  Auto)

---

Home Index