---

Step * 1 1 of Lemma fun-path-no_repeats


1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. L : T List
6. x : T
7. y : T
8. z : T
9. x = (f y) ∈ T
10. ¬(x = y ∈ T)
11. ∀j:ℕ||[y / L]||. ∀i:ℕj.  h [y / L][i] < h [y / L][j]
12. j : ℕ||[x; [y / L]]||
13. i : ℕj
⊢ h [x; [y / L]][i] < h [x; [y / L]][j]
BY
{ CaseNat 0 `i' }

1
1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. L : T List
6. x : T
7. y : T
8. z : T
9. x = (f y) ∈ T
10. ¬(x = y ∈ T)
11. ∀j:ℕ||[y / L]||. ∀i:ℕj.  h [y / L][i] < h [y / L][j]
12. j : ℕ||[x; [y / L]]||
13. i : ℕj
14. i = 0 ∈ ℤ
⊢ h [x; [y / L]][0] < h [x; [y / L]][j]

2
1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. L : T List
6. x : T
7. y : T
8. z : T
9. x = (f y) ∈ T
10. ¬(x = y ∈ T)
11. ∀j:ℕ||[y / L]||. ∀i:ℕj.  h [y / L][i] < h [y / L][j]
12. j : ℕ||[x; [y / L]]||
13. i : ℕj
14. ¬(i = 0 ∈ ℤ)
⊢ h [x; [y / L]][i] < h [x; [y / L]][j]

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  h  :  T  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x)
5.  L  :  T  List
6.  x  :  T
7.  y  :  T
8.  z  :  T
9.  x  =  (f  y)
10.  \mneg{}(x  =  y)
11.  \mforall{}j:\mBbbN{}||[y  /  L]||.  \mforall{}i:\mBbbN{}j.    h  [y  /  L][i]  <  h  [y  /  L][j]
12.  j  :  \mBbbN{}||[x;  [y  /  L]]||
13.  i  :  \mBbbN{}j
\mvdash{}  h  [x;  [y  /  L]][i]  <  h  [x;  [y  /  L]][j]


By

---

Latex:
CaseNat  0  `i'

---

Home Index