---

Step * of Lemma fun-path-append1

∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. ∀[x,y,z:T].
  (z=f*(x) via L @ [x]) supposing ((¬(y = x ∈ T)) and (y = (f x) ∈ T) and z=f*(y) via L)
BY
{ xxx(InductionOnList THEN Reduce 0)xxx }

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

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

---

Latex:

---

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


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0)xxx

---

Home Index