Library CoLoR.Util.Relation.RedLength

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-08-08
maximal reduction length of a term for a finitely branching well-founded relation

Set Implicit Arguments.

Section S.

Variables (A : Type) (R : relation A) (FB : finitely_branching R) (WF : WF R).

Definition len_aux x (len : forall y, R x y -> nat) :=
  let f i (hi : i < length (sons FB x)) :=
    len (ith hi) (in_sons_R FB (ith_In hi))
  in S (lmax (pvalues f)).

Lemma len_aux_ext : forall x (f g : forall y, R x y -> nat),
  (forall y (p : R x y), f y p = g y p) -> len_aux f = len_aux g.

Definition len : A -> nat := Fix (WF_wf_transp WF) _ len_aux.

Lemma len_eq : forall x, len x = S (lmax (map len (sons FB x))).

Lemma R_len : forall x y, R x y -> len x > len y.

End S.