---

Step * 1 of Lemma final-iterate_wf


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)
BY
{ (D -1
   THEN NatIndOn ⌜f@0 x⌝⋅
   THEN Auto
   THEN RecUnfold `final-iterate` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Complete (Auto))
   THEN (Assert f@0 do-apply(f;x) < f@0 x BY
               (BackThruSomeHyp THEN Auto))
   THEN Auto'
   THEN BackThruSomeHyp
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  (A  +  Top)
3.  SWellFounded((\muparrow{}can-apply(f;y))  c\mwedge{}  (x  =  do-apply(f;y)))
\mvdash{}  \mforall{}x:A.  (final-iterate(f;x)  \mmember{}  A)


By

---

Latex:
(D  -1
  THEN  NatIndOn  \mkleeneopen{}f@0  x\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RecUnfold  `final-iterate`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  (Assert  f@0  do-apply(f;x)  <  f@0  x  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  Auto'
  THEN  BackThruSomeHyp
  THEN  Auto')\mcdot{}

---

Home Index