---

Step * of Lemma final-iterate-property

∀[A:Type]
  ∀f:A ⟶ (A + Top)
    (SWellFounded(p-graph(A;f) y x)
    ⇒ (∀x:A
          ∃n:ℕ
           ((↑can-apply(f^n;x)) c∧ ((final-iterate(f;x) = do-apply(f^n;x) ∈ A) ∧ (¬↑can-apply(f;final-iterate(f;x)))))))
BY
{ xxx(Auto
      THEN DupHyp (-2)
      THEN RepUR ``p-graph`` -1
      THEN MoveToConcl (-2)
      THEN D -1
      THEN NatIndOn ⌜f@0 x⌝⋅
      THEN Auto
      THEN RecUnfold `final-iterate` 0
      THEN (SplitOnConclITE THENA Auto)
      THEN Try (Complete (((InstConcl [⌜0⌝])⋅
                           THEN Auto
                           THEN Try (((InstLemma `p-fun-exp_wf` [⌜A⌝; ⌜f⌝; ⌜n⌝])⋅ THEN Auto))
                           THEN Try (Complete ((RepUR ``p-fun-exp p-id can-apply do-apply`` 0 THEN Auto))))))
      THEN (Assert f@0 do-apply(f;x) < f@0 x BY
                  (BackThruSomeHyp THEN Auto))
      THEN Auto'
      THEN ((InstHyp [⌜do-apply(f;x)⌝] (-5))⋅ THENA Auto)
      THEN ExRepD
      THEN (InstConcl [⌜n + 1⌝])⋅
      THEN Auto
      THEN Try (((InstLemma `p-fun-exp_wf` [⌜A⌝; ⌜f⌝; ⌜n1⌝])⋅ THEN Auto))
      THEN OnMaybeHyp 14 (\h. (NthHypSq h
                               THEN Unfolds ``do-apply can-apply`` 0
                               THEN RepeatFor 2 (EqCD)
                               THEN Fold `do-apply` 0
                               THEN Try ((BLemma `p-fun-exp-add1-sq` THEN Auto)))))xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}f:A  {}\mrightarrow{}  (A  +  Top)
        (SWellFounded(p-graph(A;f)  y  x)
        {}\mRightarrow{}  (\mforall{}x:A
                    \mexists{}n:\mBbbN{}
                      ((\muparrow{}can-apply(f\^{}n;x))
                      c\mwedge{}  ((final-iterate(f;x)  =  do-apply(f\^{}n;x))  \mwedge{}  (\mneg{}\muparrow{}can-apply(f;final-iterate(f;x)))))))


By

---

Latex:
xxx(Auto
        THEN  DupHyp  (-2)
        THEN  RepUR  ``p-graph``  -1
        THEN  MoveToConcl  (-2)
        THEN  D  -1
        THEN  NatIndOn  \mkleeneopen{}f@0  x\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  RecUnfold  `final-iterate`  0
        THEN  (SplitOnConclITE  THENA  Auto)
        THEN  Try  (Complete  (((InstConcl  [\mkleeneopen{}0\mkleeneclose{}])\mcdot{}
                                                  THEN  Auto
                                                  THEN  Try  (((InstLemma  `p-fun-exp\_wf`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{}])\mcdot{}  THEN  Auto))
                                                  THEN  Try  (Complete  ((RepUR  ``p-fun-exp  p-id  can-apply  do-apply``  0
                                                                                            THEN  Auto
                                                                                            ))))))
        THEN  (Assert  f@0  do-apply(f;x)  <  f@0  x  BY
                                (BackThruSomeHyp  THEN  Auto))
        THEN  Auto'
        THEN  ((InstHyp  [\mkleeneopen{}do-apply(f;x)\mkleeneclose{}]  (-5))\mcdot{}  THENA  Auto)
        THEN  ExRepD
        THEN  (InstConcl  [\mkleeneopen{}n  +  1\mkleeneclose{}])\mcdot{}
        THEN  Auto
        THEN  Try  (((InstLemma  `p-fun-exp\_wf`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}n1\mkleeneclose{}])\mcdot{}  THEN  Auto))
        THEN  OnMaybeHyp  14  (\mbackslash{}h.  (NthHypSq  h
                                                          THEN  Unfolds  ``do-apply  can-apply``  0
                                                          THEN  RepeatFor  2  (EqCD)
                                                          THEN  Fold  `do-apply`  0
                                                          THEN  Try  ((BLemma  `p-fun-exp-add1-sq`  THEN  Auto)))))xxx

---

Home Index