---

Step * of Lemma fun-path-fixedpoint

∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ L) and z=f*(x) via L)
BY
{ xxxInductionOnListxxx }

1
1. T : Type
2. f : T ⟶ T
⊢ ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ []) and z=f*(x) via [])

2
1. T : Type
2. f : T ⟶ T
3. u : T
4. v : T List
5. ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ v) and z=f*(x) via v)
⊢ ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ [u / v]) and z=f*(x) via [u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[L:T  List].  \mforall{}[x,y,z:T].
    (y  =  z)  supposing  (((f  y)  =  y)  and  (y  \mmember{}  L)  and  z=f*(x)  via  L)


By

---

Latex:
xxxInductionOnListxxx

---

Home Index