---

Step * of Lemma final-iterate_wf

∀[A:Type]. ∀[f:A ⟶ (A + Top)].  ∀[x:A]. (final-iterate(f;x) ∈ A) supposing SWellFounded(p-graph(A;f) y x)
BY
{ xxx(RepUR ``p-graph`` 0 THEN UniformUnivCD Auto THEN MoveToConcl (-1))xxx }

1
1. A : Type
2. f : A ⟶ (A + Top)
3. SWellFounded((↑can-apply(f;y)) c∧ (x = do-apply(f;y) ∈ A))
⊢ ∀x:A. (final-iterate(f;x) ∈ A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].
    \mforall{}[x:A].  (final-iterate(f;x)  \mmember{}  A)  supposing  SWellFounded(p-graph(A;f)  y  x)


By

---

Latex:
xxx(RepUR  ``p-graph``  0  THEN  UniformUnivCD  Auto  THEN  MoveToConcl  (-1))xxx

---

Home Index