---

Step * 1 1 of Lemma same-final-iterate-one-one


1. [A] : Type
2. f : A ⟶ (A + Top)
3. SWellFounded(p-graph(A;f) y x)
4. [%1] : p-inject(A;A;f)
5. x : A
6. y : A
7. [%2] : final-iterate(f;x) = final-iterate(f;y) ∈ A
8. n1 : ℕ
9. ↑can-apply(f^n1;x)
10. final-iterate(f;x) = do-apply(f^n1;x) ∈ A
11. ¬↑can-apply(f;final-iterate(f;x))
12. n : ℕ
13. ↑can-apply(f^n;y)
14. final-iterate(f;y) = do-apply(f^n;y) ∈ A
15. ¬↑can-apply(f;final-iterate(f;y))
16. n ≤ n1
⊢ ↑can-apply(f^n1 - n;x)
BY
{ (Using [`n',⌜n1⌝] (BLemma `can-apply-fun-exp`)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  f  :  A  {}\mrightarrow{}  (A  +  Top)
3.  SWellFounded(p-graph(A;f)  y  x)
4.  [\%1]  :  p-inject(A;A;f)
5.  x  :  A
6.  y  :  A
7.  [\%2]  :  final-iterate(f;x)  =  final-iterate(f;y)
8.  n1  :  \mBbbN{}
9.  \muparrow{}can-apply(f\^{}n1;x)
10.  final-iterate(f;x)  =  do-apply(f\^{}n1;x)
11.  \mneg{}\muparrow{}can-apply(f;final-iterate(f;x))
12.  n  :  \mBbbN{}
13.  \muparrow{}can-apply(f\^{}n;y)
14.  final-iterate(f;y)  =  do-apply(f\^{}n;y)
15.  \mneg{}\muparrow{}can-apply(f;final-iterate(f;y))
16.  n  \mleq{}  n1
\mvdash{}  \muparrow{}can-apply(f\^{}n1  -  n;x)


By

---

Latex:
(Using  [`n',\mkleeneopen{}n1\mkleeneclose{}]  (BLemma  `can-apply-fun-exp`)\mcdot{}  THEN  Auto)

---

Home Index