---

Step * of Lemma split_rel_last

∀[A:Type]
  ∀r:A ⟶ A ⟶ 𝔹. ∀L:A List.
    (∃L1,L2:A List
      (((L = (L1 @ L2) ∈ (A List)) ∧ (¬↑null(L2)) ∧ (∀b∈L2.↑r[b;last(L)]))
      ∧ ¬↑r[last(L1);last(L)] supposing ¬↑null(L1))) supposing 
       ((¬↑null(L)) and 
       (∀a:A. (↑r[a;a])))
BY
{ InductionOnList }

1
1. [A] : Type
2. r : A ⟶ A ⟶ 𝔹
⊢ (∃L1,L2:A List
    ((([] = (L1 @ L2) ∈ (A List)) ∧ (¬↑null(L2)) ∧ (∀b∈L2.↑r[b;last([])]))
    ∧ ¬↑r[last(L1);last([])] supposing ¬↑null(L1))) supposing 
     ((¬↑null([])) and 
     (∀a:A. (↑r[a;a])))

2
1. [A] : Type
2. r : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. (∃L1,L2:A List
     (((v = (L1 @ L2) ∈ (A List)) ∧ (¬↑null(L2)) ∧ (∀b∈L2.↑r[b;last(v)]))
     ∧ ¬↑r[last(L1);last(v)] supposing ¬↑null(L1))) supposing 
      ((¬↑null(v)) and 
      (∀a:A. (↑r[a;a])))
⊢ (∃L1,L2:A List
    ((([u / v] = (L1 @ L2) ∈ (A List)) ∧ (¬↑null(L2)) ∧ (∀b∈L2.↑r[b;last([u / v])]))
    ∧ ¬↑r[last(L1);last([u / v])] supposing ¬↑null(L1))) supposing 
     ((¬↑null([u / v])) and 
     (∀a:A. (↑r[a;a])))

---

Latex:

---

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


By

---

Latex:
InductionOnList

---

Home Index