Well-founded Unions Verified

Jeremy Dawson^{1}, Nachum Dershowitz^{2}, and Rajeev Goré^{1}

1 Research School of Computer Science, Australian National University 2 School of Computer Science, Tel Aviv University

Abstract. Given n > 1 well-founded binary relations R_{1}, R_{2}, ⋯, R_{n}, when is their union ⋃_{i=1}^{n} R_{i} also well-founded ? We first describe two sets of incomparable conditions and the pen-and-paper proofs for n = 3 due to Dershowitz. We then describe conditions and machine-checked proofs for n = 4 due to Dawson and Goré. We finally describe general conditions and machine-checked proofs for arbitrary n due to Dawson and Goré.

1 Introduction

A binary relation R over some underlying set is well-founded if there is no infinite ascending chain x_{0} R x_{1} R ⋯ R x_{n−1} R x_{n} R ⋯ Thus, by well-founded, we mean the absence of infinite forward-pointing paths. Lescanne [?] as well as Blass and Gurevich [?] give some of the history of well-foundedness based on Ramsey’s Theorem 1 (below).

Given n ≥ 3 well-founded binary relations R_{1}, R_{2}, ⋯, R_{n} over some common underlying set, when is their union ⋃_{i=1}^{n} R_{i} also well-founded ?

To garner insight, we first tackle just three relations, A, B, and C and refer to the relations as “colours”. We then extend our results to n = 4 and finally describe the general pattern for arbitrary n. All proofs have been machine-checked using Isabelle/HOL and are available at www.

cecs.anu.edu.au:~jeremy/

2 Well-founded Tri-partite Unions

Assuming that A, B and C are all well-founded binary relations over some set of elements, let us use the following shorthand notations:

{A|B}  stands for  A ∪ B
AB  stands for  {(x, z) | ∃y.(x, y) ∈ A & (y, z) ∈ B}
C^{∗}  stands for  the transitive closure of C

reflexive and transitive closure ? YES Theorem 1 (Ramsey). The union {A|B |C} is well-founded if

{A|B |C}{A|B |C} ⊆ {A|B |C}  (1)

Proof. The infinite version of Ramsey’s Theorem applies when the union is transitive, so that every two (distinct) nodes within an infinite chain in the union of the colours has a coloured (directed) edge. Then, there must lie an infinite monochrome subchain within any infinite chain, contradicting the well-foundedness of each colour alone. ⊓ ⊔

Only three of the nine cases are actually needed for the limited outcome that we are seeking, an infinite monochromic path, rather than a clique as in Ramsey’s Theorem, as we observe next.

Theorem 2 (Dershowitz). The union {A|B|C} is well-founded if

{BA|CA|CB} ⊆ {A|B|C} .  (2)

Proof. When the union is not well-founded, there is an infinite path X = {x_{i}}_{i} with each edge from x_{i} to X_{i+1} one of A, B, or C. Extract a maximal subsequence {x_{i_{j}}}_{j} of X such that x_{i_{j}} A x_{i_{j+1}} for each j. If it’s finite, then repeat at the first opportunity in the tail. If any is infinite, we have our contradiction. If they’re all finite, then consider the first occurrence of x {B|C} y A z. Since we could not take an A-step from x, or we would have, the conditions tell us that x {B|C} z. Swallowing up all such (non-initial) A-steps in this way, we are left with an infinite chain in B ∪ C, for which we also know that no A-steps are possible anywhere. Now extract maximal B-chains and then erase them, replacing x C y B z with x C z (A- and B-steps having been precluded), leaving an infinite chain coloured purely C. ⊓ ⊔

Corollary 1 (Dershowitz). If A, B, and C are transitive and

BA ∪ CA ∪ CB ⊆ {A|B|C} ,

then, whenever there is an infinite path in the union {A|B|C}, there is an infinite monochromatic clique.

Let’s call the existence of an infinite ascending chain in the union {A|B|C}-immortality. We can do considerably better than the previous theorem:

Theorem 3 (Tripartite). The union {A|B|C} is well-founded if

{B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C  (3)
CB ⊆ A{A|B|C}^{∗} ∪ BB^{∗} ∪ C .

Proof. We first construct an infinite chain X = {x_{i}}_{i}, in which an A-step is always preferred over B or C, as long as immortality is maintained. To do this, we start with an immortal element x_{0} ∈ V. At each stage in the construction, if the chain so far ends in x_{i}, we look to see if there is any y such that x_{i} A y and from which proceeds some infinite chain in the union, in which case y is chosen to be x_{i+1}. Otherwise, x_{i+1} is any immortal element z such that x_{i} B z or x_{i} C z.

If there are infinitely many B’s and/or C’s in X, use them—by means of the first condition—to remove all subsequent A-steps, leaving only B- and C-steps going out of points from which A leads of necessity to mortality. From what remains, if there is any C-step at a point where one could take one or more B-steps to anyplace later in the chain, take the latter route instead. What remains now are C-steps at points where BB^{∗} detours are also precluded. If there are infinitely many such C-steps, then applying the condition for CB will result in a pure C-chain, because neither A{A|B|C}^{∗} nor BB^{∗} are options. ⊓ ⊔

Dropping C from the conditions of the previous theorem, one gets the criterion of Doornbos and Burghard von Karger [?] for well-foundedness of the union of two well-founded relations A and B, called “jumping” by Dershowitz [?] and called dvk_cond in the sequel:

jumping: BA ⊆ A{A|B}^{∗} ∪ B .

Applying this criterion twice, one gets somewhat different (incomparable) conditions for well-foundedness.

Theorem 4 (Jumping I). The union {A|B|C} is well-founded if

BA ⊆ A{A|B}^{∗} ∪ B
C{A|B} ⊆ {A|B}{A|B|C}^{∗} ∪ C .

Proof. The first inequality is the jumping criterion. The second is the same with C for B and {A|B} in place of A. ⊓ ⊔

For two relations, jumping provides a substantially weaker criterion for well-foundedness than does the appeal to Ramsey. But for three, whereas jumping allows more than one step for BA (in essence, AA^{∗}B^{∗}), it doesn’t allow for C, which Ramsey does.

Switching rôles, start with jumping for {B|C} before combining with A, we get slightly different conditions yet:

Theorem 5 (Jumping II). The union {A|B|C} is well-founded if

CB ⊆ B{B|C}^{∗} ∪ C
{B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C .

Both this version of jumping and our tripartite condition allow

{B|C}A ⊆ A{A|B|C}^{∗} ∪ B ∪ C
CB ⊆ BB^{∗} ∪ C .

They differ in that jumping also allows the condition shown below on the left whereas tripartite has the one shown on the right instead:

jumping allows  tripartite allows
CB ⊆ B{B|C}^{∗}  CB ⊆ A{A|B|C}^{∗}

Sadly, we cannot have the best of both worlds. Let’s color edges A, B, and C with (solid) azure, (dotted) black, and (dashed) crimson ink, respectively. The graph below only has multicolored loops despite satisfying

\begin{aligned}\{B|C\}A & ⊆ & C \\ CB & ⊆ & A ∪ B\{B|C\}^{∗} . \end{aligned}

\begin{matrix}• \\ • \\ • \\ • \end{matrix}

Even

\begin{aligned}\{B|C\}A & ⊆ & C \\ CB & ⊆ & B\{A|B\}^{∗} \end{aligned}

doesn’t work. To wit, the double loop in the graph below harbours no monochrome subchain:

\begin{matrix}• \\ • \\ • \end{matrix}

By the same token, the putative hypothesis below left is countered by the graph below right:

\begin{aligned}BA ∪ CB & ⊆ & C \\ CA & ⊆ & BA^{∗} \end{aligned}  \begin{matrix}• \\ • \\ • \end{matrix}

3 Verifying these theorems in Isabelle

In Section 2, we started with Theorems 1 and 2, and proved Theorem 3, which is a considerable improvement of Theorems 1 and 2. Now, we start with Theorem 3, which we call wfp tri. In the sequel, we write each Why is there no

prime here but there is one later on? It’s not wf tri and wf tri’. And I have changed D to BC. wf tri has the definition of BC and of dvk cond expanded. I’ll put current versions of both following statement of theorem. definition and theorem in both plain text and in Isabelle notation to highlight the correspondeces.

Definition 1. In Isabelle, the well-foundedness and composition of relations is defined as follows where x <_{R} y means (x, y) ∈ R:

1. A relation R is well-founded if there is no infinite descending chain

… <_{R} x_{n} <_{R} x_{n−1} <_{R} … <_{R} x_{1} <_{R} x_{0}

   wf ?r == ALL P.
              (ALL x. (ALL y. (y, x) : ?r --> P y) --> P x)
            --> (ALL x. P x)

2. The composition R o S of relations R and S is defined by

R o S = {(x, z) | ∃y.(x, y) ∈ S & (y, z) ∈ R}

   ?r O ?s == {(x, z). EX y. (x, y) : ?s & (y, z) : ?r}

In Definition 1, the question mark symbol ? indicates implicit universal quantification and so ?r and ?s are free variables (parameters) that are instantiated.

Since both o and the definition wf of well-founded used in Isabelle are the opposite of those used in Section 2, the theorems in the sequel capture the same notions. If only one were different, we would have to reverse the order of relation composition to make the two notions coincide.

Definition 2 (dvk cond ≡ jumping). Following Doornbos and von Karger [?], we define a binary condition dvk cond D A as:

D ∘ A ⊆ (A ∘ (A ∪ D)^{∗}) ∪ D

 dvk_cond ?d ?a == ?d O ?a <= (?a O (?a Un ?d)^*) Un ?d
 FOLLOWING is dvk_cond_def
 val it = "dvk_cond ?s ?r == ?s O ?r <= dvk_rel ?s ?r" : Thm.thm

why the prime in

dvk cond def'?

Without the prime, it is in terms of dvk rel, above

In Definition 2, O is Isabelle’s relational composition operator from Definition 1; Un is Isabelle’s set-union operator; and <= is ⊆.

We separate Dershowitz’s proof of the Tripartite Theorem 3 into a number of lemmas. Note how, generally, statements in the proof of the form “there exists an infinite chain” have to be translated into a (contrapositive) lemma with hypotheses and conclusion that certain relations are well-founded, or that something is in the well-founded part of a relation.

Definition 3 (wfp R). The well-founded part of a relation R, written wfp R, is the set whose elements are not the head of any infinite descending R-chain.

val wfpI =
   "ALL y. (y, ?x) : ?r --> y : wfp ?r ==> ?x : wfp ?r"

The only elements which can be shown to be in wfp r by repeated applications of this rule are in wfp r. So a relation R over an underlying

JED, is this cor- set V is well-founded if and only if every member of the underlying set rect? YES V is in the well-founded part of R. The complement operation is written

as - in Isabelle, thus - wfp R is the set of those elements which are the head of an infinite descending R-chain.

Definition 4 (immortal). Following Dershowitz, an R-immortal element is the head of an infinite descending R-chain and “ immortal” means

JED, please can (A ∪ R)-immortal, or (A ∪ B ∪ C)-immortal, as the case may be. you tidy this up. We really need to give the complicated Int part a name. I suggest just one definition for immortal, parametrized by the relation

immortal_def:    "immortal R ?y == (?y : (- wfp ?R))"
Should we also define the A-image of R-immortal elements ??, ie
not sure if it's simplier, see altermative definition of cminus below
image_immortal_def:
"image_immortal A R x == x : A `` {y : immortal R y}"

Definition 5. The (forward) image r“s of a set s under a relation r consists of those z such that some y ∈ s has (y, z) ∈ r.

Image_def: "?r `` ?s == {z. EX y:?s. (y, z) : ?r}"

In Definition 5, the expression y:?s encodes x ∈ s and (y, z) : ?r encodes (y, z) ∈ r thus in the next Definition 6, ~: is ∉.

Definition 6 (R^{−}).

R^{−} = R \ {(w, z) | ∃y.(y, z) ∈ A & y is (A ∪ R)-immortal }
= R \ {(w, z) | ∃y.(y, z) ∈ A & arimm y}
= R \ {(w, z) | ∃y.(y, z) ∈ A & y ∈ (−wfp(A ∪ R))}
= R ∩ {(w, z) | z ∉ (A“(−wfp(A ∪ R)))}

 rminus ?R ?A ==
       (?R Int {(w, z). z ~: ?A `` (- wfp (?A Un ?R))})

Thus R^{−} excludes from R all steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is (A ∪ R)-immortal.

Lemma 1 (wfp tri lem ch contra). If A∪R^{−} is well-founded then A∪ R is well-founded.

wfp_tri_lem_ch:
   "?x : wfp (?A Un (rminus ?R ?A)) ==> ?x : wfp (?A Un ?R)"

Proof. We can construct an infinite descending (A ∪ R)-chain using A where possible and using R only where necessary. ⊓ ⊔

Corollary 2 (wfp tri lem ch). If there is an infinite descending (A ∪ R)-chain then there is an infinite descending (A ∪ R)-chain where each step (w, z) ∈ R in that chain has the property that there is no (y, z) ∈ A such that y is the head of an infinite descending (A ∪ R)-chain.

Lemma 2 (wfp tri lem dvk contra). If R and A satisfy the Doornbos & von Karger [?] condition dvk cond, and A and R^{−} are well-founded, then A ∪ R is well-founded.

wfp_tri_lem_dvk: "[| dvk_cond ?R ?A;
       wf ?A; wf (rminus ?R ?A) |] ==> ?x : wfp (?A Un ?R)"

We first give a more intuitive proof, then a proof which more closely approximates the Isabelle proof. Intuitive Proof. Consider an infinite descending (A ∪ R)-chain. As A is well-founded, from any point in this chain there must be another R-step. Wherever possible replace an R-step z >_{R} v followed by an A-step v >_{A} u by an A-step (possibly followed by a number of A- or R-steps) in the given chain. (This relates to the part R ∘ A ⊆ (A ∘ (A ∪ R)^{∗}) ∪ … of dvk cond). Alternatively, if possible, replace the remainder of the chain from this point by any other infinite chain z >_{A} y >_{A∪R} . . .. Again, this will not always be possible since A is well-founded.

So, where this is not possible, we can replace an R-step followed by an A-step by a single R-step, which is possible using the part R∘A ⊆ …∪R

of dvk cond.

Doing this repeatedly could absorb any number of A-steps, but, again, as A is well-founded there cannot be infinitely many such A-steps, so eventually we reach another R-step. Repeating this gives the required infinite R-chain, with the given property.

The next proof approximates more closely to the Isabelle proof.

Proof. Assume that A is well-founded. Define R^{−} to be R, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is immortal. Assume that R^{−} is well-founded.

Suppose that there is an infinite descending (A ∪ R)-chain. Choose a head z of such a chain, choosing z to be A-minimal, and also to be R^{−}-minimal among A-minimal immortal elements. As z is A-minimal, the first step of an infinite chain must be (y, z) ∈ R (say), and also in fact (y, z) ∈ R^{−}. As A is well-founded, let y be A-minimal among possible choices for y. Then, by the R^{−}-minimality of z, although y is immortal, it is not A-minimal among immortal members. So we have (x, y) ∈ A, where x is immortal. Since R ∘ A ⊆ (A ∘ (A ∪ R)^{∗}) ∪ R, we could replace z >_{R} y >_{A} x in the infinite chain by

(x, z) ∈ A ∘ (A ∪ R)^{∗}: say (x, y′) ∈ (A ∪ R)^{∗} and (y′, z) ∈ A where x, y′ and z are immortal. But this would contradict the A-minimality of z and our consequent inference that (y, z) ∉ A, or

(x, z) ∈ R: which would contradict our choice of y which was to be Aminimal, since x could have been chosen instead of y.

Thus, either way we get a contradiction, so A ∪ R is well-founded. ⊓ ⊔

Corollary 3 (wfp tri lem dvk). If R and A satisfy the Doornbos & von Karger [?] condition dvk cond, and A is well-founded, and there is an infinite descending (A ∪ R)-chain, then there is an infinite descending Rchain whose members are not of the form z where (y, z) ∈ A and y is immortal, ie is the head of an infinite descending (A ∪ R)-chain.

Definition 7. Define C^{−} to be C, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is (X ∪ B ∪ C)- immortal. JED, we need to

give the complicated Int construct a name.

C^{−} = C \ {(w, z) | ∃y.(y, z) ∈ A & y is (X ∪ B ∪ C)-immortal}
= C ∩ {(w, z) | z ∉ A“(−wfp(X ∪ B ∪ C))}

  cminus ?C ?B ?A ?X ==
       (?C Int {(w, z). z ~: ?A `` (- wfp (?X Un ?B Un ?C))})
  cminus ?C ?B ?A ?X ==
       (?C Int {(w, z). ~ image_immortal A (X Un B Un C) z})

For the purposes of Theorem 6, X will be A, but we will use the lemma with more general X when there are four or more relations.

Lemma 3 (wf tri lem BCm). If B and C^{−} are well-founded, and condition (d) of Theorem 6 is satisfied, then B ∪ C^{−} is well-founded. JED please fix

this. DONE

wf_tri_lem_BCm: "[| wf ?B; wf (cminus ?C ?B ?A ?X);
 ?C O ?B <= (?A O (?X Un ?B Un ?C)^*) Un (?B O ?B^*) Un ?C |]
 ==> wf (?B Un (cminus ?C ?A ?B ?X))"

Proof. Assume that B and C^{−} are well-founded.

For a contradiction, suppose that B ∪C^{−} is not well-founded. So there exists an (B ∪ C^{−})-immortal z. Choose z to be B-minimal such, and also to be C^{−}-minimal among possible B-minimal choices.

As z is B-minimal, the first step of an infinite B ∪ C^{−}-chain must be (y, z) ∈ C^{−} (say). As B is well-founded, let y be B-minimal among possible choices for y. Then, by the C^{−}-minimality of z, although y is (B∪ C^{−})-immortal, it is not B-minimal among (B ∪ C^{−})-immortal members. So we have (x, y) ∈ B, where x is (B ∪ C^{−})-immortal. Since C ∘ B ⊆ (A ∘ (X ∪ B ∪ C)^{∗}) ∪ (B ∘ B^{∗}) ∪ C, we could replace z >_{C} y >_{B} x in the infinite chain by

(x, z) ∈ A ∘ (X ∪ B ∪ C)^{∗}: say (x, y′) ∈ (X ∪ B ∪ C)^{∗} and (y′, z) ∈ A — but x is (B∪C^{−})-immortal, and so is the head of an infinite descending X ∪ B ∪ C-chain, contradicting that (y, z) ∈ C^{−}; or (x, z) ∈ B ∘ B^{∗}: which would contradict our choice of z to be B-minimal;

or (x, z) ∈ C: and so (x, z) ∈ C^{−} which would contradict our choice of y to

be B-minimal, since x could have been chosen instead of y.

Thus, in each case we get a contradiction, so B ∪ C^{−} is well-founded.

⊓ ⊔

Theorem 6 (wf tri', Tripartite, Dershowitz, Theorem 3). Given three binary relations A, B and C, their tripartite union A ∪ B ∪ C is well-founded if all of the following hold:

(a) each of A, B, C are well-founded;

(b) D = (B ∪ C);

(c) dvk cond D A ;

(d) C ∘ B ⊆ (A ∘ (A ∪ D)^{∗}) ∪ (B ∘ B^{∗}) ∪ C.

wf_tri':  "[|
    wf ?A ; wf ?B ; wf ?C ;
    ?D = ?B Un ?C ;
    dvk_cond ?D ?A ;
    ?C O ?B <= (?A O (?A Un ?D)^*) Un (?B O ?B^*) Un ?C
    |] ==> wf (?A Un ?D)"
CURRENT VERSION FOLLOWS
wf_tri';
  "[| ?BC = ?B Un ?C; dvk_cond ?BC ?A;
   ?C O ?B <= (?A O (?A Un ?BC)^*) Un (?B O ?B^*) Un ?C;
   wf ?A; wf ?B; wf ?C |] ==> wf (?A Un ?BC)"
VERSION WITH BC and dvk_cond expanded FOLLOWS
wf_tri;
   "[| ?B Un ?C O ?A <= (?A O (?A Un (?B Un ?C))^*) Un (?B Un ?C);
    ?C O ?B <= (?A O (?A Un (?B Un ?C))^*) Un (?B O ?B^*) Un ?C;
    wf ?A; wf ?B; wf ?C |] ==> wf (?A Un (?B Un ?C))"

Proof. (of Theorem 6) By Corollary 3 it is enough to prove that (B ∪C)^{−} is well-founded. By Lemma 3 we have that B ∪ C^{−} is well-founded, and clearly (B ∪ C)^{−} ⊆ B ∪ C^{−}. ⊓ ⊔

4 Quatro-partite Well-foundedness

Now we show how to extend this result to four (or more) relations.

Theorem 7 (wf four Dawson and Goré). Uall = A ∪ B ∪ C ∪ D is well-founded if

(a) each of A, B, C and D are well-founded, and

(b) (B ∪ C ∪ D) ∘ A ⊆ (A ∘ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (B ∪ C ∪ D)

(c) D ∘ C ⊆ (A ∘ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (C ∘ C^{∗}) ∪ D

(d) (C ∪ D) ∘ B ⊆ (A ∘ (A ∪ B ∪ C ∪ D)^{∗}) ∪ (B ∘ B^{∗}) ∪ C ∪ D

val wf_four =
 "[| ?uall = ?A Un ?B Un ?C Un ?D;
     wf ?A; wf ?B; wf ?C; wf ?D ;
     dvk_cond (?B Un ?C Un ?D) ?A;
     ?D O ?C <= (?A O ?uall^*) Un (?C O ?C^*) Un ?D;
     (?C Un ?D) O ?B <= (?A O ?uall^*) Un (?B O ?B^*) Un (?C Un ?D)
  |] ==> wf ?uall"

Proof. We adapt the previous definition of R^{−} for a relation R: that is, R^{−} is R, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is (A ∪ B ∪ C ∪ D)-immortal:

R^{−} = R\{(w, z) ∈ R | ∃y.(y, z) ∈ A and y is (A∪B∪C ∪D)−immortal}.

As D is well-founded, a fortiori D^{−} is well-founded. Setting A, X, B, C to A, A ∪ B, C, D, respectively, in Lemma 3 and using condition (c), we obtain that C ∪ D^{−} is well-founded, and so a fortiori (C ∪ D)^{−} is wellfounded. Setting A, X, B, C to A, A, B, C ∪ D, respectively in Lemma 3 and condition (d) we obtain that B ∪ (C ∪ D)^{−} is well-founded and so a fortiori (B∪C ∪D)^{−} is well-founded. Finally, by Corollary 3 A∪B∪C ∪D is well-founded. ⊓ ⊔

5 The General Result

We now extend Theorem 7 to an arbitrary number of relations. The proof is straightforward but we need to set up some definitions.

First the condition we call tri cond, which is the condition satisfied by the list [B, C, D] in the case of four relations. It is defined recursively and gives (for example) conditions (c) and (d) of Theorem 7.

Definition 8. For an arbitrary binary operator f , define the right-fold operator for list [B, C, D] with initial value Z to be

foldr f [B, C, D] Z = B f (C f (D f Z))

foldr.simps : [
   "foldr ?f [] ?z = ?z",
   "foldr ?f (?x # ?xs) ?z = ?f ?x (foldr ?f ?xs ?z)"]

Definition 9. For all Auall, the condition tri cond Auall L is true if

Base Case: L is the empty list

Inductive Case: L=B.Bs and uBs  =  ⋃_{b∈Bs} b and

   uBs ∘ B ⊆ Auall ∪ (B ∘ B^{∗}) ∪ uBs and tri cond Auall Bs holds.
tri_cond_Nil  : "tri_cond ?Auall [] = True"
tri_cond_Cons : "tri_cond ?Auall (?B # ?Bs) =
   ((let uBs = foldr (op Un) ?Bs {}
      in uBs O ?B <= ?Auall Un (?B O ?B^*) Un uBs)
   & tri_cond ?Auall ?Bs)"

We then need a separate lemma which is proved by structural induction on the list, say [B, C, D], of relations. For the general case we work with a list B_{1}, B_{2}, …, B_{n}.

Definition 10. Define U^{−} to be U, but excluding steps of the form (w, z) where there exists some y such that (y, z) ∈ A and y is (X ∪U)-immortal:

U^{−} = U \ {(w, z) ∈ U | ∃y.(y, z) ∈ A and y is (X ∪ U)-immortal }

Lemma 4. If Bs = [B_{1}, B_{2}, …, B_{n}], and B_{1}, B_{2}, …, B_{n} are all wellfounded, and U = (B_{1} ∪ B_{2} ∪ … ∪ B_{n}) and tri cond A ∘ (X ∪ U) [B_{1}, B_{2}, …, B_{n}] holds then U^{−} is well-founded.

tri_n_lem :
 "[| ALL B:(set ?Bs) . wf B ;
     ?uBs = foldr (op Un) ?Bs {};
     ?Auall = ?A O (?X Un ?uBs)^*;
     tri_cond ?Auall ?Bs |] ==> wf (uminus ?uBs ?A ?X)"

Proof. The proof is by structural induction on the list Bs = [B_{1}, B_{2}, …, B_{n}]. That is, the base case is when Bs is the empty list [] and the inductive step is when Bs = [B_{i}, B_{i+1}, ⋯, B_{n}] and X is an arbitrary X_{i} and then the inductive hypothesis used is that the lemma holds for Bs = [B_{i+1}, ⋯, B_{n}] and X = X_{i} ∪ B_{i}. The inductive step is proved using Lemma 3.

The value used for X varies throughout, so if its final value is X_{f}, then the lemma is proved successively for

[]  X = X_{f} ∪ B_{1} ∪ B_{2} ∪ … ∪ B_{n}
[B_{n}]  X = X_{f} ∪ B_{1} ∪ B_{2} ∪ … ∪ B_{n−1}
⋮  ⋮
[B_{2}, …, B_{n}]  X = X_{f} ∪ B_{1}
[B_{1}, B_{2}, …, B_{n}]  X = X_{f}

Note that the value of X ∪ U (as used in the definition of U^{−} above) therefore remains unchanged, and that at each step we also use, in addition to Lemma 3, the fact that if B ∪ V^{−} is well-founded, then (B ∪ V)^{−} is well-founded. ⊓ ⊔

Then we have the following theorem.

Theorem 8 (Dawson and Goré). Assuming that Bs = [B_{1}, B_{2}, …, B_{n}], for n ≥ 1, the union A ∪ B_{1} ∪ B_{2} ∪ … ∪ B_{n} is well-founded if

(a) A and B_{1}, B_{2}, …, B_{n} are all well-founded; and

(b) U = (B_{1} ∪ B_{2} ∪ … ∪ B_{n}); and

(c) tri cond A ∘ (A ∪ U) [B_{1}, B_{2}, …, B_{n}] holds; and

(d) U ∘ A ⊆ (A ∘ (A ∪ U)^{∗}) ∪ U

tri_n "[|
  wf ?A;  ALL B : (set ?Bs). wf B
  ?uBs = (foldr (op Un) ?Bs {});
  ?Auall = ?A O (?A Un ?uBs)^*; tri_cond ?Auall ?Bs;
  dvk_cond ?uBs ?A |] ==> wf (?A Un ?uBs)"

Proof. By Lemma 4 we get that U^{−} is well-founded, where we use X = A in the definition of U^{−}. Then Corollary 3 gives the result. ⊓ ⊔