---

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

∀[A:Type]. ∀[n,m:ℕ]. ∀[f:A ⟶ (A + Top)]. ∀[x:A].
  uiff(↑can-apply(f^n + m;x);(↑can-apply(f^m;x)) ∧ (↑can-apply(f^n;do-apply(f^m;x))))
BY
{ (Auto THEN Try ((DoSubsume THEN Auto')) THEN Try ((FLemma `can-apply-fun-exp-add` [-1] THEN 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 + m;x)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Try  ((DoSubsume  THEN  Auto'))  THEN  Try  ((FLemma  `can-apply-fun-exp-add`  [-1]  THEN  Auto)\mcdot{}))

---

Home Index