Re: [Hol-info] Two definitions of wellfoundedness

Hi, ah... thanks, I didn’t see this theorem before. —Chun > Il giorno 11 set 2018, alle ore 10:08, Lorenz Leutgeb 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

Re: [Hol-info] Two definitions of wellfoundedness

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) wrote: > Hi, > > in prim_recTheory, there’s a definition of ``wellfounded``: > > [wellfounded_def] Definition > > ⊢

[Hol-info] CfP: Postproceedings ThEdu'18

Open Call for Papers ** Postproceedings for ThEdu'18 by EPTCS Theorem proving components for Educational software http://www.uc.pt/en/congressos/thedu/th

[Hol-info] Two definitions of wellfoundedness

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 a