---

Step * of Lemma sorted-by-cons

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x:T. ∀L:T List.  (sorted-by(R;[x / L]) ⇐⇒ sorted-by(R;L) ∧ (∀z∈L.R x z))
BY
{ (Unfold `sorted-by` 0 THEN Reduce 0 THEN Auto THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. L : T List
5. ∀i:ℕ||L|| + 1. ∀j:ℕi.  (R [x / L][j] [x / L][i])
6. i : ℕ||L||
7. j : ℕi
⊢ R L[j] L[i]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. L : T List
5. ∀i:ℕ||L|| + 1. ∀j:ℕi.  (R [x / L][j] [x / L][i])
⊢ (∀z∈L.R x z)

3
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. L : T List
5. ∀i:ℕ||L||. ∀j:ℕi.  (R L[j] L[i])
6. (∀z∈L.R x z)
7. i : ℕ||L|| + 1
8. j : ℕi
⊢ R [x / L][j] [x / L][i]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}x:T.  \mforall{}L:T  List.    (sorted-by(R;[x  /  L])  \mLeftarrow{}{}\mRightarrow{}  sorted-by(R;L)  \mwedge{}  (\mforall{}z\mmember{}L.R  x  z))


By

---

Latex:
(Unfold  `sorted-by`  0  THEN  Reduce  0  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index