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
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
