Hi, they are the same. Use the following theorem from prim_rec:
WF_IFF_WELLFOUNDED ⊢ ∀R. WF R ⇔ wellfounded R Best, Lorenz On Tue, 11 Sep 2018 at 17:59 Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > Hi, > > in prim_recTheory, there’s a definition of ``wellfounded``: > > [wellfounded_def] Definition > > ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n) > > In relationTheory, there’s a definition of ``WF``: > > [WF_DEF] Definition > > ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b > > are they essentially the same thing? (and if so, how to prove?) > > —Chun > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
