CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.when the union of two wellfounded relations is wellfounded
- Joerg Endrullis, 2008-07-28
- Frederic Blanqui, 2007-02-05
When the two relations commute.
Lemma SN_union_commut t :
(forall x, SN S x -> SN R x) -> SN S t -> R @ S << S @ R -> SN (R U S) t.
Lemma WF_union_commut : WF R -> WF S -> R @ S << S @ R -> WF (R U S).
When a relation absorbs the other.
Commutation and SN