---

Step * 1 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
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]))
BY
{ ((InstHyp [⌜l (f i)⌝] (-1)⋅ THENA Auto) THEN (SplitOnHypITE -1  THEN Auto) THEN SplitOnHypITE -2  THEN Auto') }

1
.....truecase..... 
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 )
12. ((rank (f i)) + 1) ≤ ((rank (f j)) + 1)
13. (l (f i)) = (l (f i)) ∈ ℤ
14. (l (f j)) = (l (f i)) ∈ ℤ
⊢ ↓∃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
9.  j  :  \mBbbN{}
10.  i  :  \mBbbN{}j
11.  \mforall{}k:\mBbbN{}k
            (if  (l  (f  i)  =\msubz{}  k)  then  (rank  (f  i))  +  1  else  0  fi    \mleq{}  if  (l  (f  j)  =\msubz{}  k)
              then  (rank  (f  j))  +  1
              else  0
              fi  )
\mvdash{}  \mdownarrow{}\mexists{}i,j:\mBbbN{}.  (i  <  j  \mwedge{}  (\mneg{}R[f  j;f  i]))


By

---

Latex:
((InstHyp  [\mkleeneopen{}l  (f  i)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (SplitOnHypITE  -1    THEN  Auto)
  THEN  SplitOnHypITE  -2 
  THEN  Auto')

---

Home Index