---

Step * 1 of Lemma locally-ranked-is-well-founded


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R[y;x])
4. k : ℕ
5. rank : T ⟶ ℕ
6. l : T ⟶ ℕk
7. ∀x,y:T.  (((l x) = (l y) ∈ ℤ) ⇒ R[x;y] ⇒ rank x < rank y)
8. f : ℕ ⟶ T
⊢ ↓∃i,j:ℕ. (i < j ∧ (¬R[f j;f i]))
BY
{ ((InstLemma `Dickson\'s lemma` [⌜k⌝;⌜λi,n. if (l (f n) =z i) then (rank (f n)) + 1 else 0 fi ⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RepUR ``so_apply`` -1) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R[y;x])
4. k : ℕ
5. rank : T ⟶ ℕ
6. l : T ⟶ ℕk
7. ∀x,y:T.  (((l x) = (l y) ∈ ℤ) ⇒ R[x;y] ⇒ rank x < rank y)
8. f : ℕ ⟶ T
9. j : ℕ
10. i : ℕj
11. ∀k:ℕk. (if (l (f i) =z k) then (rank (f i)) + 1 else 0 fi  ≤ if (l (f j) =z k) then (rank (f j)) + 1 else 0 fi )
⊢ ↓∃i,j:ℕ. (i < j ∧ (¬R[f j;f i]))

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  Trans(T;x,y.R[y;x])
4.  k  :  \mBbbN{}
5.  rank  :  T  {}\mrightarrow{}  \mBbbN{}
6.  l  :  T  {}\mrightarrow{}  \mBbbN{}k
7.  \mforall{}x,y:T.    (((l  x)  =  (l  y))  {}\mRightarrow{}  R[x;y]  {}\mRightarrow{}  rank  x  <  rank  y)
8.  f  :  \mBbbN{}  {}\mrightarrow{}  T
\mvdash{}  \mdownarrow{}\mexists{}i,j:\mBbbN{}.  (i  <  j  \mwedge{}  (\mneg{}R[f  j;f  i]))


By

---

Latex:
((InstLemma  `Dickson\mbackslash{}'s  lemma`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}i,n.  if  (l  (f  n)  =\msubz{}  i)  then  (rank  (f  n))  +  1  else  0  fi  \mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  ExRepD
  THEN  RepUR  ``so\_apply``  -1)

---

Home Index