---

Step * 2 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. x=f*(y) via L
9. ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]
10. x1 : T
11. y1 : T
12. f1 : ℕ2 ⟶ ℕ||L||
13. increasing(f1;2)
14. ∀j:ℕ2. ([x1; y1][j] = L[f1 j] ∈ T)
⊢ ¬(L[f1 0] = L[f1 1] ∈ T)
BY
{ (InstHyp [⌜f1 1⌝;⌜f1 0⌝] 9⋅ THEN Auto') }

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. x=f*(y) via L
9. ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]
10. x1 : T
11. y1 : T
12. f1 : ℕ2 ⟶ ℕ||L||
13. increasing(f1;2)
14. ∀j:ℕ2. ([x1; y1][j] = L[f1 j] ∈ T)
15. h L[f1 0] < h L[f1 1]
⊢ ¬(L[f1 0] = L[f1 1] ∈ T)

---

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.  x=f*(y)  via  L
9.  \mforall{}j:\mBbbN{}||L||.  \mforall{}i:\mBbbN{}j.    h  L[i]  <  h  L[j]
10.  x1  :  T
11.  y1  :  T
12.  f1  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||L||
13.  increasing(f1;2)
14.  \mforall{}j:\mBbbN{}2.  ([x1;  y1][j]  =  L[f1  j])
\mvdash{}  \mneg{}(L[f1  0]  =  L[f1  1])


By

---

Latex:
(InstHyp  [\mkleeneopen{}f1  1\mkleeneclose{};\mkleeneopen{}f1  0\mkleeneclose{}]  9\mcdot{}  THEN  Auto')

---

Home Index