Well-Founded Unions

Given two or more well-founded binary relations, when can one be certain that their union is likewise well-founded? We provide conditions for an arbitrary number of relations, generalizing known conditions for two relations, along with counterexamples to several potential weakenings. Such conditions may be useful for proving termination of rewrite systems. (All proofs have been machine checked.)

Joint with Jeremy Dawson and Rajeev Goré

hosted by