---

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


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))
BY
{ (RepUR ``p-compose can-apply do-apply`` 0
   THEN ((GenConclAtAddr [1; 1; 1; 1; 1]) THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  (A  +  Top)
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}[y:A].  \mforall{}[m:\mBbbN{}].  \muparrow{}isl(f\^{}m  y)  supposing  m  \mleq{}  (n  -  1)  supposing  \muparrow{}isl(f\^{}n  -  1  y)
6.  y  :  A
7.  m  :  \mBbbN{}
8.  m  \mleq{}  n
9.  \mneg{}(m  =  0)
\mvdash{}  (\muparrow{}isl(f\^{}n  -  1  o  f\^{}1  y))  {}\mRightarrow{}  (\muparrow{}isl(f\^{}m  -  1  o  f\^{}1  y))


By

---

Latex:
(RepUR  ``p-compose  can-apply  do-apply``  0
  THEN  ((GenConclAtAddr  [1;  1;  1;  1;  1])  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index