Hi, ah... thanks, I didn’t see this theorem before.
—Chun > Il giorno 11 set 2018, alle ore 10:08, Lorenz Leutgeb <lor...@leutgeb.xyz> ha > scritto: > > 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 > <mailto: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 <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info > <https://lists.sourceforge.net/lists/listinfo/hol-info>
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
