---

Step * 1 of Lemma can-apply-fun-exp-add-iff


1. A : Type
2. n : ℕ
3. m : ℕ
4. f : A ⟶ (A + Top)
5. x : A
6. ↑can-apply(f^m;x)
7. ↑can-apply(f^n;do-apply(f^m;x))
⊢ ↑can-apply(f^n + m;x)
BY
{ (RWO "p-fun-exp-add" 0 THENA Auto') }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  f  :  A  {}\mrightarrow{}  (A  +  Top)
5.  x  :  A
6.  \muparrow{}can-apply(f\^{}m;x)
7.  \muparrow{}can-apply(f\^{}n;do-apply(f\^{}m;x))
\mvdash{}  \muparrow{}can-apply(f\^{}n  +  m;x)


By

---

Latex:
(RWO  "p-fun-exp-add"  0  THENA  Auto')

---

Home Index