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