---

Step * of Lemma p-fun-exp-add-sq

∀[A:Type]. ∀[f:A ⟶ (A + Top)]. ∀[x:A]. ∀[m,n:ℕ].  f^n + m x ~ f^n do-apply(f^m;x) supposing ↑can-apply(f^m;x)
BY
{ xxx(InductionOnNat THEN (UnivCD THENA Auto))xxx }

1
1. A : Type
2. f : A ⟶ (A + Top)
3. x : A
4. m : ℤ
5. n : ℕ
6. ↑can-apply(f^0;x)
⊢ f^n + 0 x ~ f^n do-apply(f^0;x)

2
1. A : Type
2. f : A ⟶ (A + Top)
3. x : A
4. m : ℤ
5. 0 < m
6. ∀[n:ℕ]. f^n + (m - 1) x ~ f^n do-apply(f^m - 1;x) supposing ↑can-apply(f^m - 1;x)
7. n : ℕ
8. ↑can-apply(f^m;x)
⊢ f^n + m x ~ f^n do-apply(f^m;x)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].  \mforall{}[x:A].  \mforall{}[m,n:\mBbbN{}].
    f\^{}n  +  m  x  \msim{}  f\^{}n  do-apply(f\^{}m;x)  supposing  \muparrow{}can-apply(f\^{}m;x)


By

---

Latex:
xxx(InductionOnNat  THEN  (UnivCD  THENA  Auto))xxx

---

Home Index