---

Step * of Lemma can-apply-fun-exp

∀[A:Type]. ∀[f:A ⟶ (A + Top)]. ∀[n:ℕ]. ∀[y:A].  ∀[m:ℕ]. ↑can-apply(f^m;y) supposing m ≤ n supposing ↑can-apply(f^n;y)
BY
{ (Unfold `can-apply` 0
   THEN ((InductionOnNat THEN Auto)
         THEN CaseNat 0 `m'
         THEN Try ((RepUR ``p-fun-exp p-compose p-id`` 0 THEN Trivial))
         THEN Subst' m ~ (m - 1) + 1 0
         THEN Try (Complete (Auto'))
         THEN RWO "p-fun-exp-add" 0
         THEN Auto
         THEN MoveToConcl (-4)
         THEN Subst' n ~ (n - 1) + 1 0
         THEN Try (Complete (Auto'))
         THEN (RWO "p-fun-exp-add" 0 THENA Auto))
   ) }

1
1. A : Type
2. f : A ⟶ (A + Top)
3. n : ℤ
4. 0 < n
5. ∀[y:A]. ∀[m:ℕ]. ↑isl(f^m y) supposing m ≤ (n - 1) supposing ↑isl(f^n - 1 y)
6. y : A
7. m : ℕ
8. m ≤ n
9. ¬(m = 0 ∈ ℤ)
⊢ (↑isl(f^n - 1 o f^1 y)) ⇒ (↑isl(f^m - 1 o f^1 y))

---

Latex:

---

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


By

---

Latex:
(Unfold  `can-apply`  0
  THEN  ((InductionOnNat  THEN  Auto)
              THEN  CaseNat  0  `m'
              THEN  Try  ((RepUR  ``p-fun-exp  p-compose  p-id``  0  THEN  Trivial))
              THEN  Subst'  m  \msim{}  (m  -  1)  +  1  0
              THEN  Try  (Complete  (Auto'))
              THEN  RWO  "p-fun-exp-add"  0
              THEN  Auto
              THEN  MoveToConcl  (-4)
              THEN  Subst'  n  \msim{}  (n  -  1)  +  1  0
              THEN  Try  (Complete  (Auto'))
              THEN  (RWO  "p-fun-exp-add"  0  THENA  Auto))
  )

---

Home Index