---

Step * of Lemma sublist-sorted-by

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀sa,sb:T List.  (sa ⊆ sb ⇒ sorted-by(R;sb) ⇒ sorted-by(R;sa))
BY
{ (Auto THEN D -2 THEN ParallelLast THEN Auto THEN (RWO "7" 0 THENA Auto) THEN BackThruSomeHyp THEN Auto THEN Auto') }

1
.....wf..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. sa : T List@i
4. sb : T List@i
5. f : ℕ||sa|| ⟶ ℕ||sb||@i
6. increasing(f;||sa||)@i
7. ∀j:ℕ||sa||. (sa[j] = sb[f j] ∈ T)@i
8. ∀i:ℕ||sb||. ∀j:ℕi.  (R sb[j] sb[i])@i
9. i : ℕ||sa||@i
10. j : ℕi@i
⊢ f j ∈ ℕf i

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}sa,sb:T  List.    (sa  \msubseteq{}  sb  {}\mRightarrow{}  sorted-by(R;sb)  {}\mRightarrow{}  sorted-by(R;sa))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  ParallelLast
  THEN  Auto
  THEN  (RWO  "7"  0  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  Auto')

---

Home Index