---

Step * of Lemma fun-path-no_repeats

∀[T:Type]. ∀[f:T ⟶ T].  ∀[L:T List]. ∀[x,y:T].  no_repeats(T;L) supposing x=f*(y) via L supposing retraction(T;f)
BY
{ xxx(xxxAutoxxx THEN D 3 THEN Assert ⌜∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]⌝⋅)xxx }

1
.....assertion..... 
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
⊢ ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h 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. x=f*(y) via L
9. ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]
⊢ no_repeats(T;L)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].
    \mforall{}[L:T  List].  \mforall{}[x,y:T].    no\_repeats(T;L)  supposing  x=f*(y)  via  L  supposing  retraction(T;f)


By

---

Latex:
xxx(xxxAutoxxx  THEN  D  3  THEN  Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}||L||.  \mforall{}i:\mBbbN{}j.    h  L[i]  <  h  L[j]\mkleeneclose{}\mcdot{})xxx

---

Home Index