---

Step * 1 of Lemma fun-path-no_repeats

.....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]
BY
{ xxx(MoveToConcl (-1)
      THEN (MakeUniform THENA Auto)
      THEN RepeatFor 3 (MoveToConcl (-1))
      THEN BLemma `fun-path-induction`
      THEN Auto)xxx }

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
⊢ h [x; [y / L]][i] < h [x; [y / L]][j]

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  \mforall{}j:\mBbbN{}||L||.  \mforall{}i:\mBbbN{}j.    h  L[i]  <  h  L[j]


By

---

Latex:
xxx(MoveToConcl  (-1)
        THEN  (MakeUniform  THENA  Auto)
        THEN  RepeatFor  3  (MoveToConcl  (-1))
        THEN  BLemma  `fun-path-induction`
        THEN  Auto)xxx

---

Home Index