``` ```

# Some Properties of Well-foundation

``` Require Import List. ```
 Accessible => no direct cycles
``` Lemma well_foundation1:   forall (A: Set) (R: A -> A -> Prop) (x: A),     (Acc R x) ->     forall (y: A),       (R x y) ->       (R y x) -> False. ```
 Well-founded => no direct cycles
``` Lemma well_foundation2:   forall (A: Set) (R: A -> A -> Prop),     (well_founded R) ->     forall (x y: A),       (R x y) ->       (R y x) -> False. ```
 Function extension of a binary relation
``` Definition fun_extension (A B: Set) (f: A -> B) (R: B -> B -> Prop) (x y: A): Prop :=   (R (f x) (f y)) . ```
 accessible interpretation
``` Lemma well_foundation3:   forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),     forall (x: B),       (Acc R x) ->       forall (x': A),         (x = (f x')) ->         (Acc (fun_extension A B f R) x') . ```
 Well-founded interpretation
``` Lemma well_foundation4:   forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),     (well_founded R) ->     (well_founded (fun_extension A B f R)) . ```
Index