---

Step * of Lemma insert-by-no-repeats

∀[T:Type]. ∀[eq,r:T ⟶ T ⟶ 𝔹].
  (∀[x:T]. ∀[L:T List].
     (no_repeats(T;insert-by(eq;r;x;L))) supposing (no_repeats(T;L) and sorted-by(λx,y. (↑(r x y));L))) supposing 
     (Linorder(T;a,b.↑(r a b)) and 
     (∀a,b:T.  (↑(eq a b) ⇐⇒ a = b ∈ T)))
BY
{ InductionOnList⋅ }

1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. r : T ⟶ T ⟶ 𝔹
4. ∀a,b:T.  (↑(eq a b) ⇐⇒ a = b ∈ T)
5. Linorder(T;a,b.↑(r a b))
6. x : T
⊢ (no_repeats(T;insert-by(eq;r;x;[]))) supposing (no_repeats(T;[]) and sorted-by(λx,y. (↑(r x y));[]))

2
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. r : T ⟶ T ⟶ 𝔹
4. ∀a,b:T.  (↑(eq a b) ⇐⇒ a = b ∈ T)
5. Linorder(T;a,b.↑(r a b))
6. x : T
7. u : T
8. v : T List
9. (no_repeats(T;insert-by(eq;r;x;v))) supposing (no_repeats(T;v) and sorted-by(λx,y. (↑(r x y));v))
⊢ (no_repeats(T;insert-by(eq;r;x;[u / v]))) supposing (no_repeats(T;[u / v]) and sorted-by(λx,y. (↑(r x y));[u / v]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq,r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
    (\mforall{}[x:T].  \mforall{}[L:T  List].
          (no\_repeats(T;insert-by(eq;r;x;L)))  supposing 
                (no\_repeats(T;L)  and 
                sorted-by(\mlambda{}x,y.  (\muparrow{}(r  x  y));L)))  supposing 
          (Linorder(T;a,b.\muparrow{}(r  a  b))  and 
          (\mforall{}a,b:T.    (\muparrow{}(eq  a  b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)))


By

---

Latex:
InductionOnList\mcdot{}

---

Home Index