---

Step * 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
⊢ ∃n:ℕ. (((↑can-apply(f^n;x)) c∧ (y = do-apply(f^n;x) ∈ A)) ∨ ((↑can-apply(f^n;y)) c∧ (x = do-apply(f^n;y) ∈ A)))
BY
{ (((InstConcl [⌜n1 - n⌝])⋅ THENA Auto') THEN (OrLeft THENA Auto) THEN D 0) }

1
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)

2
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

---

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{}  \mexists{}n:\mBbbN{}
      (((\muparrow{}can-apply(f\^{}n;x))  c\mwedge{}  (y  =  do-apply(f\^{}n;x)))  \mvee{}  ((\muparrow{}can-apply(f\^{}n;y))  c\mwedge{}  (x  =  do-apply(f\^{}n;y))))


By

---

Latex:
(((InstConcl  [\mkleeneopen{}n1  -  n\mkleeneclose{}])\mcdot{}  THENA  Auto')  THEN  (OrLeft  THENA  Auto)  THEN  D  0)

---

Home Index