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


1. [A] Type
2. A ⟶ (A Top)
3. SWellFounded(p-graph(A;f) x)
4. [%1] p-inject(A;A;f)
5. A
6. 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. : ℕ
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⌝])⋅ THENA Auto') THEN (OrRight THENA Auto) THEN 0) }

1
1. [A] Type
2. A ⟶ (A Top)
3. SWellFounded(p-graph(A;f) x)
4. [%1] p-inject(A;A;f)
5. A
6. 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. : ℕ
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^n n1;y)

2
1. Type
2. A ⟶ (A Top)
3. SWellFounded(p-graph(A;f) x)
4. p-inject(A;A;f)
5. A
6. 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. : ℕ
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^n n1;y)
⊢ do-apply(f^n n1;y) ∈ 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.  \mneg{}(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{}n  -  n1\mkleeneclose{}])\mcdot{}  THENA  Auto')  THEN  (OrRight  THENA  Auto)  THEN  D  0)




Home Index