---

Step * 1 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 o f^m;x)
BY
{ (Unfold `can-apply` 0
   THEN RepUR ``p-compose`` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Fold `can-apply` 0)
   THEN Auto)⋅ }

---

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  o  f\^{}m;x)


By

---

Latex:
(Unfold  `can-apply`  0
  THEN  RepUR  ``p-compose``  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Fold  `can-apply`  0)
  THEN  Auto)\mcdot{}

---

Home Index