---

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

No Annotations
∀[A:Type]
  ∀f:A ⟶ (A + Top)
    (SWellFounded(p-graph(A;f) y x)
    ⇒ ∀x,y:A.
         ∃n:ℕ. ((p-graph(A;f^n) x y) ∨ (p-graph(A;f^n) y x)) supposing final-iterate(f;x) = final-iterate(f;y) ∈ A 
       supposing p-inject(A;A;f))
BY
{ (Intros
   THEN RepUR ``p-graph`` 0
   THEN Auto
   THEN ((InstLemma `final-iterate-property` [⌜A⌝; ⌜f⌝; ⌜x⌝])⋅ THENA Auto)
   THEN ((InstLemma `final-iterate-property` [⌜A⌝; ⌜f⌝; ⌜y⌝])⋅ THENA Auto)
   THEN ExRepD
   THEN (Decide n ≤ n1 THENA Auto)) }

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
⊢ ∃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)))

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type]
    \mforall{}f:A  {}\mrightarrow{}  (A  +  Top)
        (SWellFounded(p-graph(A;f)  y  x)
        {}\mRightarrow{}  \mforall{}x,y:A.
                  \mexists{}n:\mBbbN{}.  ((p-graph(A;f\^{}n)  x  y)  \mvee{}  (p-graph(A;f\^{}n)  y  x)) 
                  supposing  final-iterate(f;x)  =  final-iterate(f;y) 
              supposing  p-inject(A;A;f))


By

---

Latex:
(Intros
  THEN  RepUR  ``p-graph``  0
  THEN  Auto
  THEN  ((InstLemma  `final-iterate-property`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `final-iterate-property`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Decide  n  \mleq{}  n1  THENA  Auto))

---

Home Index