Disjunctive Termination for Affluent Families


We introduce affluence, a condition on composition that entails a finite family of rewrite relations is terminating iff its union is (disjunctive termination), and relate it to jumping. Our proofs transform infinite reductions in the family union into such in family members, by induction on family size.