---

Step * 1 of Lemma sublist-sorted-by

.....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
BY
{ ((FLemma `increasing_implies` [6]  THEN Auto) THEN BHyp -1  THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  sa  :  T  List@i
4.  sb  :  T  List@i
5.  f  :  \mBbbN{}||sa||  {}\mrightarrow{}  \mBbbN{}||sb||@i
6.  increasing(f;||sa||)@i
7.  \mforall{}j:\mBbbN{}||sa||.  (sa[j]  =  sb[f  j])@i
8.  \mforall{}i:\mBbbN{}||sb||.  \mforall{}j:\mBbbN{}i.    (R  sb[j]  sb[i])@i
9.  i  :  \mBbbN{}||sa||@i
10.  j  :  \mBbbN{}i@i
\mvdash{}  f  j  \mmember{}  \mBbbN{}f  i


By

---

Latex:
((FLemma  `increasing\_implies`  [6]    THEN  Auto)  THEN  BHyp  -1    THEN  Auto)

---

Home Index