---

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

∀[A:Type]. ∀[n,m:ℕ]. ∀[f:A ⟶ (A + Top)]. ∀[x:A].
  {(↑can-apply(f^m;x)) ∧ (↑can-apply(f^n;do-apply(f^m;x))) ∧ (do-apply(f^n + m;x) = do-apply(f^n;do-apply(f^m;x)) ∈ A)} 
  supposing ↑can-apply(f^n + m;x)
BY
{ (Auto'
   THEN (DupHyp (-1))
   THEN ((RWO "p-fun-exp-add" (-1)) THENA Auto)
   THEN Try ((Unfold `label` 0 THEN Auto))
   THEN ((FLemma `can-apply-compose` [-1]) THENA Auto)
   THEN Unfold `guard` 0
   THEN Auto
   THEN (RWO "p-fun-exp-add" 0 THENA Auto)
   THEN RWO "do-apply-compose" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto'
  THEN  (DupHyp  (-1))
  THEN  ((RWO  "p-fun-exp-add"  (-1))  THENA  Auto)
  THEN  Try  ((Unfold  `label`  0  THEN  Auto))
  THEN  ((FLemma  `can-apply-compose`  [-1])  THENA  Auto)
  THEN  Unfold  `guard`  0
  THEN  Auto
  THEN  (RWO  "p-fun-exp-add"  0  THENA  Auto)
  THEN  RWO  "do-apply-compose"  0
  THEN  Auto)

---

Home Index