---

Step * of Lemma sorted-by-exists

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

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. u : T
7. v : T List
8. ∃L':T List. (sorted-by(λx,y. (↑(r x y));L') ∧ no_repeats(T;L') ∧ v ⊆ L' ∧ L' ⊆ v)
⊢ ∃L':T List. (sorted-by(λx,y. (↑(r x y));L') ∧ no_repeats(T;L') ∧ [u / v] ⊆ L' ∧ L' ⊆ [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{}L:T  List.  \mexists{}L':T  List.  (sorted-by(\mlambda{}x,y.  (\muparrow{}(r  x  y));L')  \mwedge{}  no\_repeats(T;L')  \mwedge{}  L  \msubseteq{}  L'  \mwedge{}  L'  \msubseteq{}  L)\000C) 
        supposing  \mforall{}a,b:T.    (\muparrow{}(eq  a  b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
InductionOnList\mcdot{}

---

Home Index