---

Step * of Lemma sorted-cons

∀[T:Type]. ∀[x:T]. ∀[L:T List].  uiff(sorted([x / L]);sorted(L) ∧ (∀z∈L.x ≤ z)) supposing T ⊆r ℤ
BY
{ (Unfold `sorted` 0 THEN Reduce 0 THEN Auto THEN Try ((D -1 THEN Complete (Auto))) THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. T ⊆r ℤ
3. x : T
4. L : T List
5. ∀i:ℕ||L|| + 1. ∀j:ℕi.  ([x / L][j] ≤ [x / L][i])
6. i : ℕ||L||
7. j : ℕi
⊢ L[j] ≤ L[i]

2
1. T : Type
2. T ⊆r ℤ
3. x : T
4. L : T List
5. ∀i:ℕ||L|| + 1. ∀j:ℕi.  ([x / L][j] ≤ [x / L][i])
⊢ (∀z∈L.x ≤ z)

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[L:T  List].    uiff(sorted([x  /  L]);sorted(L)  \mwedge{}  (\mforall{}z\mmember{}L.x  \mleq{}  z))  supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
(Unfold  `sorted`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  -1  THEN  Complete  (Auto)))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index