# Library CoLoR.MannaNess.AMannaNess

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2006-12-01
termination by using compatible reduction orderings

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig).
Notation rule := (rule Sig). Notation rules := (list rule).

Manna-Ness theorem (1970)

Lemma manna_ness (R : rules) succ :
reduction_ordering succ -> compat succ R -> WF (red R).

an extension for proving the well-foundedness of relations of the form: several steps of R1 followed by a step of R2

Lemma manna_ness_mod (R E : rules) (rp : Reduction_pair Sig) :
compat (rp_succ_eq rp) E -> compat (rp_succ rp) R -> WF (red_mod E R).

an extension for proving the well-foundedness of relations of the form: several steps of R1 followed by a -head- step of R2
rule elimination

Section rule_elimination.

Variables R Rgt Rge : rules.

Section mod.

Variables E Egt Ege : rules.

Lemma rule_elimination_mod : forall rp : Reduction_pair Sig,
compat (rp_succ rp) Rgt ->
compat (rp_succ_eq rp) Rge ->
compat (rp_succ rp) Egt ->
compat (rp_succ_eq rp) Ege ->
WF (red_mod Ege Rge) ->
WF (red_mod (Egt ++ Ege) (Rgt ++ Rge)).

Lemma rule_elimination_hd_mod : forall wp : Weak_reduction_pair Sig,
compat (wp_succ_eq wp) E ->
compat (wp_succ_eq wp) Rge ->
compat (wp_succ wp ) Rgt ->
WF (hd_red_mod E Rge) ->
WF (hd_red_mod E (Rgt ++ Rge)).

End mod.

Lemma rule_elimination : forall rp : Reduction_pair Sig,
compat (rp_succ_eq rp) Rge ->
compat (rp_succ rp ) Rgt ->
WF (red Rge) ->
WF (red (Rgt ++ Rge)).

Lemma rule_elimination_hd_red : forall wp : Weak_reduction_pair Sig,
compat (wp_succ_eq wp) Rge ->
compat (wp_succ wp ) Rgt ->
WF (hd_red Rge) ->
WF (hd_red (Rgt ++ Rge)).

End rule_elimination.

End S.