---

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


1. A : Type
2. f : A ⟶ (A + Top)
3. SWellFounded(p-graph(A;f) y x)
4. p-inject(A;A;f)
5. x : A
6. y : A
7. 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
17. ↑can-apply(f^n1 - n;x)
⊢ y = do-apply(f^n1 - n;x) ∈ A
BY
{ ((Assert ↑can-apply(f^n + (n1 - n);x) BY
          (Subst' n + (n1 - n) ~ n1 0 THEN Auto))
   THEN (FLemma `can-apply-fun-exp-add` [-1])
   THEN Auto
   THEN (Using [`n',⌜n⌝] (FLemma `p-fun-exp-injection` [4]))⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  (A  +  Top)
3.  SWellFounded(p-graph(A;f)  y  x)
4.  p-inject(A;A;f)
5.  x  :  A
6.  y  :  A
7.  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
17.  \muparrow{}can-apply(f\^{}n1  -  n;x)
\mvdash{}  y  =  do-apply(f\^{}n1  -  n;x)


By

---

Latex:
((Assert  \muparrow{}can-apply(f\^{}n  +  (n1  -  n);x)  BY
                (Subst'  n  +  (n1  -  n)  \msim{}  n1  0  THEN  Auto))
  THEN  (FLemma  `can-apply-fun-exp-add`  [-1])
  THEN  Auto
  THEN  (Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (FLemma  `p-fun-exp-injection`  [4]))\mcdot{}
  THEN  Auto)

---

Home Index