---

Step * of Lemma insert-by-sorted-by

∀[T:Type]
  ∀eq,r:T ⟶ T ⟶ 𝔹.
    Linorder(T;a,b.↑(r a b))
    ⇒ (∀x:T. ∀L:T List.  (sorted-by(λx,y. (↑(r x y));L) ⇒ sorted-by(λx,y. (↑(r x y));insert-by(eq;r;x;L)))) 
    supposing ∀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
⊢ sorted-by(λx,y. (↑(r x y));[]) ⇒ sorted-by(λx,y. (↑(r x y));insert-by(eq;r;x;[]))

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. sorted-by(λx,y. (↑(r x y));v) ⇒ sorted-by(λx,y. (↑(r x y));insert-by(eq;r;x;v))
⊢ sorted-by(λx,y. (↑(r x y));[u / v]) ⇒ sorted-by(λx,y. (↑(r x y));insert-by(eq;r;x;[u / v]))

---

Latex:

---

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


By

---

Latex:
InductionOnList\mcdot{}

---

Home Index