Combining Induction Axioms by Machine

1 Introduction

One crucial point in proving theorems by induction is to find an induction axiom for a given conjecture 'I' as the right instance of the Generalized Principle of Noetherian Induction: [VmE M. [\ikE M. k<Mm ~ 'ljl(k)] ~ 'ljl(m)] ~ VmE M. 'ljl(m). The invention of a "successful" well­ founded relation <M for a statement constitutes the creativi­ ty of a human, and also of an automated expert in induction theorem proving. This problem has two aspects: (1) a proof strategic aspect, which means that the relation <M induced upon allows to prove the induction formula [VmE M. [\ikE M. k <M m ~ 'ljl(k)] ~ 'ljl(m)], and (2) a soundness aspect, which means that the relation <M induced upon must be indeed well founded.

system, a so-called relation description (r-description for short) is computed from the user's definition in a uniform way. Given, for instance, the functions

function quot(x,y:number):number ~ ify = 0 then 0 ifx < y then 0 ifx ~ y" y-:# 0 then succ(quot(x-y y)) cnl function half(x:number):number ~ ifx = 0 then 0 ifx= 1then0 ifx-:~; 0" x-:# 1then succ(half((x-1)-1))

as input, the r-descriptions Dquot = {(x~yAy-:#0, { {x/x-y, y/y} })} and Dttalf = {(x-:#OAx-:#1, { {x/(x-1)-1} })} are com­ puted from the recursive cases of the algorithms. 1 An r­ description Dis a finite and non-empty set {C 1 , ... ,Ck} of atomic r-descriptions ci =(<pi, ai). where the range for­ mula <pi is a quantifier-free formula and ~ is a finite and non-empty set of substitutions, called the domain substi­ tutions. The set rV(D) of relevant variables in D is the set of all variables mentioned in D, e.g. x andy in Dquott and the set of induction variables iV(D) of D contains all relevant variables which are substituted for by the domain substitutions. Each r-description D defines a relation <o on some cartesian product of the set of constructor ground terms, e.g. Dquot defines a relation <quot c (IJ'(:~:c)numberX IJ'(l::c)number) 2 given as (a b) <quot (c d) iff 3[ x/c, y/d] I= x~yAy-:#0, a=~n x/c, y/dl (x-y) and b=3[ x/c, y/dl (y). 3 is the interpretation for the known functions, which accepts some ground term from tT (l:) as input, e.g. plus(succ(O) succ(O)), and always returns a constructor ground term from IJ'(l:c) as output, e.g. succ(succ(O)). Also 3 ( q)=q may be assumed for all constructor ground terms q. The interpretation 3 can be applied also to terms with variables if variable assignments like [ x/c, y/d] are used. For the above r-descriptions, (2,3) <quot (5,3) <quot (8,3) <quot ... is a chain wrt. the relation defined by Dquot and 1 <half 3 <half 5 <half .. . is a chain wrt. the relation defined by Dttalf· The relations obtained are well-founded because only terminating functions are accepted by an induction theorem prover, and therefore these r-descriptions are called well-founded.

Since each well-founded r-description D defines a well­ founded relation <o and likewise a well-founded set, we may uniformly associate an induction axiom with D. Given an r-description D = {(<pl. a 1 ), ... ,(<pk' ak)} with relevant variables x* and a formu a \j1 with free variables x*, D is associated with k+l induction formulas, the base case 'l'o and the step formulas \jf 1 , ... ,\jfk. The range formulas <pi in the atomic r-descriptions of D define the cases of the induction steps and the domain substitutions 5e ~ are used to form the induction hypotheses. The base case is obtained as the complement of all the range formulas in D and ['1' 0 " ... " 'l'k --+ V x*. \jf] is an induction axiom.

1 To ease readability we often use the usual mathemati­ cal notation, e.g. x>y,x+y,x-y,x-1, 2 etc., instead of the terms formally required, e.g. gt(x y)=true, plus(x y), minus(x y), pred(x), succ(succ(O)) etc.

Consider, for instance, some formula \jf[x,y] with free variables x andy. The induction formulas to prove V x,y. \jf[x,y] are computed from Dquot as

'l'o = V x,y. x < y v y=O--+ \jf[x,y] and 'l't = V x,y. x~y A y-:#0 A \jf[x/x-y, y/y] --+ \jf[x,y]. But if~ is used instead of Dquot· the induction formulas for proving V x,y. \jf[x,y] are obtained as 'l'o = V x. x=O v x=1 --+ V y. \jf[x,y] and 'l't = V x. x-:#0 A x-:#1/\ Vy. \jf[x/(x-1)-1, y]

--+ V y.\jf[x,y].

The r-descriptions obtained from terminating functions necessitate further computations for subsequent induction proofs: Domain generalizations and range generalizations are computed and each range generalization ~n is separated which finally yields an r-description providing certain proof-technical advantages.2 For instance, the well­ founded r-description Dquot' = {(x~yAy-:#0, {{x/x-y}})} is a domain generalization of the above r-description Dquot having only x as an induction variable. Domain generali­ zations are obtained by removing some substitution pairs from the domain substitutions thus extending the domain of the defined relation, as Dquot' is obtained by removal of y/y. This extends the defined relation to (a b) <quot' (c d) iff 3[ x/c, y/dl l=x~yAy-:#0 and a=3l x/c, y/dl (x-y). Note that b may be any constructor ground term here because now no replacement is demanded for the relevant variable y. Consequently, (2,9) <quot' (5,3) <quot' (6,1) <quot' ... is a chain wrt. the relation defined by Dquot'· To prove V x,y. \jf[x,y], the following induction formulas are obtained if the domain generalization Dquot' is used:

'l'o = V x,y. x < y v y=O--+ \jf[x,y] and

'l't = Vx,y. x~y" y-:#0 A Vu. \jf[x/x-y, y/u]--+ \jf[x,y]. The variable y in this example is universally quantified (after being renamed to u) in the induction hypothesis \jf[x/x-y, y/u]. and this yields a stronger induction than with Dquot·

The well-founded r-description Dquot" = { (x-:#OAy-:#0, { {x/x-y} })} is a range generalization of the above r­ description Dquot'· It is obtained by replacing the range for­ mula in Dquot' by some weaker requirement, thus extending the range of the defined relation. For instance, (2,9) is a minimal element wrt. <quot' because 2~9 does not hold. But (2,9) is not minimal wrt. <quot" because 2;Jt0 " 9;Jt0, and therefore (0, ... ) <quot" (2,9). The advantage of a range generalization is that the fewer minimal elements a well­ founded relation has, the fewer elements have to be treated as base cases of an induction based on this relation. To prove V x,y. \jf[x,y], for instance, the following induction formulas are obtained if the range generalization Dquot" is used:

'l'o = V x,y. x=O v y=O--+ \jf[x,y] and 'l't = V x,y. x-:#0" y-:#0" Vu. \jf[x/x-y, y/u]--+ \jf[x,y].

2 The computation of a domain generalization corres­ ponds to the computation of a measure/ su6set as defmed by [Boyer and Moore, 1979], the computation of a range generalization corresponds to the computation of a revise/ macli.ine and the computation of a separation cor­ responds to the computation of a superimpose/ macli.ine.

Using its termination proof facility, cf. [Boyer and Moore, 1979; Walther, 1988], an induction theorem prover checks each domain and nnge generalization for well-foun­ dedness ·and those which fail the test are not considered any further. After this test only the generalized (we11-founded) r­ descriptions are used for computing induction axioms. This does not restrict provability, because <o c <o· ifD' is an r­ description obtained from D by a domain or a range ·genera­ lization.

If some statement 'I' has to be verified by the induction theorem prover, r-descriptions ar.e suggested by an induc­ tion heuristic in order- to compute induction axioms from them, cf. [Aubin, 1979; Boyer and Moore, 1979]. By reco,gnizing function "calls" in the statement, the r­ descriptions associated with the called functions are selected from the set of well-founded r-descriptions already compu­ ted. However, those r-descriptions which fail to meet cer­ tain variable requirements are disregarded. The remaining r­ descriptions are modified by replacing some relevant non­ induction variables with the corresponding terms in the call (if necessary).

Given, for instance, the statement V x. 'I' I = V x. quot(x 4) = half(half(x)), the r-descriptions Dquot'" = {(xit6A4i:O, {{x/x-4}})} and Dhalf = {(x:/:0, {{x/(x-1)-1}})} are sug­ gested by an induction heuristic. The r-description Dhalf' is a range generalization of ~alf and Dquot"' is built from the r-description Dquot" by replacing the non-induction variable y of D quot" with 4 to match the argument in the call.

3 Combining Induction Axioms

The r-descriptions obtained as suggestions of an induction heuristic are rated and compared, e.g. by using the sub­ sumption heuristic [Boyer and Moore, 1979] or the con­ tainment test [Walther, 1992], and those which fail the tests are rejected. But in general more than one r-description survives the comparison, e.g. Dquot'" and Dhalf' in the example above, and we have to decide what to do with them. Obviously, statement 'I' 1 can be easily proven by induction upon <guot"' (but not upon <half). However, this is only known after a proof is computed. So, the problem is to find a well-founded relation which guarantees prova­ bility whenever an induction proof using either the <quot'"­ or the <hau·-induction is successful. We simply use <quot~ u<half and with the subset principle provability is not destroyed. So the induction axiom for 'I' 1 is computed as:

V x. x=O ~ quot(x 4)=half(half(x)) ,

The induction 'hypothesis quot(((x-1 )-1) 4) - half(half((x-1 )-1)) stems from the <ihatrinduction and the induction hypothesis quot(x-4 4) = half(half(x-4)) stems from the <quot~-induction. Both induction formulas can be easily proven. Therefore statement 'l't is an inductive truth which intuitively means that all quantifiers in a formula range over constructor ground terms only. We define g~=: V x.<p iff g( x/q] l=<p for all constructor ground terms q which may be substituted for x and Thlnd := {'If I 'If is a closed formula such that g~=: 'If}. An induction theorem prover tests whether a formula 'I' is a member of the set Jbmd of all inductive true theorems. 4

3 Here and subsequently obv.ious simplifications are used, like 4""0 can be omitted here. We also abbreviate "Vx:number" by "V·x.".

A straightforward idea for formalizing this approach is to use the union D 1 uD2 of a pair of r-descriptions D 1 and D 2 as 1the r-description from which the induction axiom is computed, because <o,uo 2 = < 01 u< 02 · But generally non valid induction formulas are generated if the union of r­ descriptions is used. In particular Oquot"VDhalf = { (xo~:O, {{x/x-4}}), (x:/:0, {{x/(x-1)-1}})} yields two step formu­ las for statement 'If 1 , viz.

(1) V x. x:/:0" quot(x-4 4)=half(half(x-4))

one of which is not provable by first-order means: The induction hypothesis can be used to prove step formula (1), but this is not the case for step formula (2). The reason for this failure is that not all required induction hypotheses wrt. <quot"'C<half are provided by step formula (2). How­ ever, this problem can be avoided if a separated r-descrip­ tion is used. This is an r-description 0 such that the range formulas of 0 exclude each other, i.e. [Vx* -,<p 1 v-,<p2]E Thlnd for all members (<p 1 , L11) and (<p2, L12) of D, and a separated r-description guarantees that all possible induction hypotheses wrt. <o are provided by a step formula, cf. [Walther, 1992]. To avoid unseparated r-descriptions when forming the union of relations, we propose the separated union, i.e. a separated r-description such that the relation implicitly defined is the union of the relations implicitly defined by the constituting r-descriptions:

Definition 3.1 For a pair of r-descriptions 0 1 = {(<pl' &l), ... ,(<pk, &k)} and 02 = {(111' e.) ..... (llh' eh)}, the separated union 0 1 EElD 2 of 0 1 and 0 2 is the smallest r­ description such that for each atomic r-description (<pi, &i) E 0 1 and each atomic r-description (llj· ej) E 0 2

Theorem 3.1 [Walther, 1991] For each pair of separa­ ted r-descriptions 0 1 and D 2 : (1) 0 1 ®D 2 is a separated r­ description, and (2) <o,enz = <0 , u <nz .

4 An induction theorem prover only provides a suffi­ cient requirement for veThind because, due to Godel's First Incompleteness Theorem, neither Thrnd is decidable nor semi-decidable.

Since <o 1 c <o 1 ED~ and<~ c <o 1 ED~ by Theorem 3.1, we may always use the separated union D 1 $D 2 instead of D 1 or D 2 to compute an induction axiom. With the subset principle it is guaranteed that an induction proof with D 1 $D 2 always can be obtained whenever an induction proof with D 1 or with D 2 is successful. We compute Dquot"'$Dhalf = {(x:t<>, {{x/(x-1)-1}, {x/x-4}})}, and the above induction axiom for 'I' 1 was obtained from this r­ description.

4 Commuting Induction Axioms

However, since the union of well-founded relations general­ ly is not well-founded, the well-foundedness of D 1 $D 2 has to be verified before it is used to compute an induction axiom. For solving this problem the termination proof fa­ cility of an induction theorem prover may be used. Actually this will be our ultimate resort, but first we shall attempt to verify the well-foundedness of D 1 $D 2 directly from the well-foundedness of D 1 and D 2 .

To do so we borrow a technique from the area of term rewriting. There a problem quite similar to ours arises, viz. to prove that a term rewriting system R 1 uR 2 is noe­ therian, where R 1 and R 2 are noetherian term rewriting sys­ tems. For this problem the notion of quasi-commutation has been proposed:

Definition 4.1 [Bachmair and Dershowitz, 1986] For a pair of relations < 1 and < 2 on some set S, < 1 quasi­ commutes over < 2 iff (*) for all q ,t,rE S with q < 2 t < 1 r some t'E S exists such that q <* 1 u 2 t' < 2 r, cf. Figure I (i), where <* 1 u 2 denotes the reflexive and transi­ tive closure of < 1 u< 2 .

Theorem 4.1 [Bachmair and Dershowitz, 1986] If < 1 quasi-commutes over < 2 , then < 1 u< 2 is well-founded iff < 1 and < 2 are well-founded. '

Quasi-commutation can be used to verify the well­ foundedness of < 1 u< 2 as demonstrated by Theorem 4.1: If < 1 and < 2 are well-founded, only "< 1 quasi-commutes over < 2 " or else "< 2 quasi-commutes over < 1 " has to be verified for proving the well-foundedness of < 1 u< 2 . 5

5 We have two attempts to establish the well­ foundedness of <1 U<2 , because "quasi-commutes over" is not a symmetric property.

To check for quasi-commutation in our application, we have to formulate a syntactical requirement in terms of relation descriptions which is sufficient for requirement (*) in Definition 4.1. This is necessary because our relations are not explicitly given but are implicitly defined as the semantics of r-descriptions. So requirement (*) in Defini­ tion 4.1 essentially is a semantical property which neces­ sitates a syntactical counterpart for our purposes. But re­ quirement (*) cannot be characterized by a finite set of for­ mulas because the transitive closure<+ cannot be characte­ rized. So we have to be satisfied with those approximations of requirement (*) which are finitely representable and we define:

Definition 4.2 For a pair of relations < 1 and < 2 on some set S, < 1 quasi-commutes over < 2 with type A iff (**) for all q ,t ,rE S with q < 2 t < 1 r some t'E S exists such that q <A t' < 2 r, where A is some finite string over {1,2}, a <Aod b stands for "some cE S exists such that a <A c <d b ", and a <t: b means a = b (where E is the empty string).

Figure l(ii) illustrates Definition 4.2. Obviously, quasi­ commutation with type A ~ntails quasi-commutation, but not vice versa because A is afixed string. For instance, < 1 quasi-commutes over < 2 with type E iff for all q,t,rE S with q < 2 t < 1 r also q < 2 r, cf. Figure l(iii), and < 1 quasi-commutes over < 2 with type 1 iff for all q,t,rE S with q < 2 t < 1 r some t'E S exists such that q < 1 t' < 2 r, cf. Figure l(iv).

We have eliminated transitivity by using quasi-commu­ tation with a type and are able to represent this weaker requirement in terms of relation descriptions and formulas derived from them. For the sake of brevity we shall confine ourselves here to the cases of quasi-commutation with type E and type 1. Moreover, we shall confine ourselves to rela­ tion descriptions consisting of one atomic r~description with one domain substitution only, and refer to [Walther, 1991] for the general form. We start with the type 1 case:

Definition 4.3 For a pair of r-descriptions D 1 = {(q>, {o})} and D 2 = {('Jl, {9})}, D 1 quasi-commutes over D 2 with type 1 (1-commutes for short) iff for some variables x*:

Theorem 4.2 [Walther, 1991] If an r-description D1 1commutes over an r-description D2, then < 01 quasi­ commutes over <~ with type 1.

Requirement (1) in Definition 4.3 is the ]-variable requirement and the formulas in requirements (2) and (3) are the ]-commutation formulas. If these formulas hold, then < 01 quasi-commutes over < 02 by Theorem 4.2, hence < 01 U< 02 is well-founded by Theorem 4.1 (provided < 01 and <o 2 are well-founded), and since <o 1 EDo 2 = < 01 u< 02 by Theorem 3.1, D 1 $D 2 is a well-founded r-description.

Hence we demand that an induction theorem prover verifies the 1-commutation formulas before D 1 Gm 2 is used to com­ pute an induction axiom. For the above example, the 1commutation formulas to verify that Dhalf 1-commutes over D quot'" are computed as:

1. V x. x:tO A ((x-1}-1~ ~ x:tO A (x-4):t0 and

Obviously formula (2) does not hold, so 1-commutation of D uot"' over Dhalf is tested:6

• (2~ V x. x:tO A (x-4):t0 ~ x:tO A ((x-1}-1):t0 and
• (3') V x. x:tO A (x-4):t0 ~ ((x-1}-1)-4 = ((x-4)-1}-1.

Also obviously these 1-commutation formulas are true and consequently the well-foundedness of Dquot'" $Dhalf is verified. This proves the soundness of the induction axiom initially used for statement 'I' 1 , cf. Section 3.

Next we consider quasi-commutation of type e:

Definition 4.4 For a pair of r-descriptions D 1 = {(cp, {&})}and D 2 = {(Tt. {9})}, D 1 quasi-commutes over D 2 with type £ (£-commutes for short) iff for x* = rV(D 1 )urV(D 2 ):

1. all variables in 11 c Dom(&),
2. [V x*. cpA O(Tt) ~ Tt]E Thlnd, and
3. [V x*. cpA O(Tt) ~ AxeDom(9) 9(&(x))=9(x)]E Thlnd·

Theorem 4.3 [Walther, 1991] If an r-description D1 £­ commutes over an r-description D2. then < 01 quasi­ commutes over <0z with type £.

Requirement (1) in Definition 4.4 is the £-variable requirement. The formulas in requirements (2) and (3) are the £-commutation formulas and we demand that an induc­ tion theorem prover verifies these formulas before D 1 EDD 2 is used to compute an induction axiom.

As an example demonstrating the usefulness of £-com­ mutation, consider the functions minus1 and minus2 given as

function minus1(x,y:number):number ¢= ifx~y then 0 ifx>y then succ(minus1(x succ(y))) function minus2(x,y:number):number ¢= ifx=O then 0 if x:tO A y=O then x ifx:tO A y:tO then minus2(x-1 y-1)

and the statement Vx,y. '1'2 = Vx,y. minus1 (x y) .. minus2(x y). An induction heuristic could suggest Dminus2· = {(x*O, { { x/x-1}})} and Dminus2" = { (y:tO, { { y /y-1}})} both obtained by domain and range generalization from Dminus2 = {(x*OAy~. { {x/x-1, y/y-1}} )}, and also suggest Dminusl = {(x>y, {{x/x, y/succ(y)}})}.

6 The falsification of those formulas usually is trivial, at least if some facility looking for counterexamples for system-computed conjectures is applied, cf. [Protzen, 1992], yielding here x=3 as a counterexample.

The tests for 1- and for £-commutation fail for almost all combinations of the three r-descriptions, simply because the variable requirements are not satisfied. But the £­ variable requirement for verifying that Dminusl £-commutes over Dminus2· is satisfied and the £-commutation formulas are computed as

1. V x,y. x>y A x:tO ~ x:tO and
2. V x,y. x>y A x:tO ~ (x-1)=(x-1).

The verification of both formulas is trivial. Therefore, Dminusl$Dminus2' = {(x*OAx~y. {{x/x-1}}), (x>y, { {x/x-1}, {x/x, y/succ(y)}})} is a well-founded r-descrip­ tion from which the following induction axiom is com­ puted for '1'2:

V x,y. x=O ~ minus1(x y)=minus2(x y) , V x,y. x:tO A x~y A V z. minus1(x-1 z)=minus2(x-1 z) ~ minus1(x y)=minus2(x y) , V x,y. x>y A V z. minus1(x-1 z)=minus2(x-1 z) A minus1(x succ(y))=minus2(x succ(y)) ~ minus1(x y)=minus2(x y)

V x,y. minusl(x y)=minus2(x y) .

The induction hypothesis minus1 (x succ(y)) - minus2(x succ(y)) stems from the <minus1-induction and the induc­ tion hypothesis V z. minus1 (x-1 z) = minus2(x-1 z) (appearing in both step formulas) stems from the <minus2'­ induction. Since the variable z in the latter induction hypo­ thesis is universally quantified, the induction is so strong that the statement can be proven with one trivial lemma only, viz. [V x,y. x*O A x~y ~ Y*O] is required for the first step formula. Both induction hypotheses are used in the proof of the second step formula. The hypothesis stem­ ming from Dminus2· must be used twice, viz. with z sub­ stituted by y and with z substituted by y-1. The success of the Dminusl $Dminus2.-induction is remarkable because the functions minus1 and minus2 differ significantly in their recursion structure. This usually necessitates that an induction theorem prover is supported by additional lem­ mata which relate one function to the other if only one of the suggested r-descriptions is used to form an induction axiom. This is not needed here, and we consider this as an evidence for the strength of the proposed method.

As a further example, consider the function plus given as

function plus(x,y:number):number ¢= ifx=O then y ifx:tO then succ(plus(x-1 y))

and the statement Vx,y. '1' 3 = Vx,y. plus(x y) = plus(y x). An induction heuristic could suggest Dplus' = { (x*O, {{x/x-1}})} andalsoD 1 .. = {(y:tO, {{y/y-1}})}, both obtained by a domain g~~~ralization from Dplus = { (x~. { {x/x-1, y/y} })} (after a variable renaming for Dplus" to match the argument in the call). All tests for 1- and for £­ commutation fail because the variable requirements are not satisfied. Analysing the case, we see that Dplus'$D Ius" = { (x:tO A y=O, { { x/x-1}} ), (x=O A y:tO, { {y/y-1}} ), {x:tO A y:tO, { { x/x-1}. {y/y-1}})} cannot be well-founded because

···<plus" (0 1) '),Ius' (1 0) < Ius" (0 1) <oius' (1 O) is an infinite <plus'u plus .. -cbain in '1' (l:: c htumberX 'T(:Ec)number· But since <plus' and <plus" are well-founded, an obvious remedy is to use some subset <plus· of <plus' (or of <plus" respectively), hoping that <plus·uplus" is well-founded at least

But fortunately we know some subset of <plus': Since D 1 · was obtained from D~us by a domain generalization, pus . d . <plus c < Ius' holds (and erefore Dplus was Ignore m favour of b 1 · when r-descriptions were suggested for '!' 3 ). pus We now test Dplus and Dplus" for quasi-commutation. ~ere the !-variable requirement is not satisfied but the e-vanable requirement is when £-commutation of Dplus over Dplus" is tested. The £-commutation formulas are computed as:

1. V x,y. x:#O 1\ y:#O ~ y:#O and

(3) V x,y. x:#O 1\ y:#O ~ (y-1) = (y-1).

The verification of both formulas is trivial. Therefore, DplusEBDplus" = {(x~O 1\ y=O, {{x/x-1, y/y}} ), (x=O 1\ y:#O, {{y/y-1}}), (x:#O 1\ y:#O, {{x/x-1, y/y}, {y/y-1}})} is a well-founded r-description from which the induction axiom for '1' 3 is computed as:

V x,y. x=O 1\ y =0 ~ plus(x y)=plus(y x) , V x,y. x:#O 1\ y=O 1\ plus(x-1 y)=plus(y x-1) ~ plus(x y)=plus(y x) , V x,y. x=O 1\ y~O 1\ V z. plus(z y-l)=plus(y-1 z) ~ plus(x y)=plus(y x) , V x,y. x:#O 1\ y~O 1\ plus(x-1 y)=plus(y x-1) 1\ V z. plus(z y-l)=plus(y-1 z) ~ plus(x y)=plus(y x) ,

V x,y. plus(x y)=plus(y x) ·

The induction hypotheses plus(x-1 y) "' plus(y x-1) stem from the< 1 -induction and the induction hypotheses V z. pm . plus(z y-1) .. plus(y-1 z) stem from the <plus" -inducuo~. Since the variable z in the latter induction hypotheses IS universally quantified, the induction is so strong that the statement can be proven without an additional lemma. All induction hypotheses are required for the proofs of the step formulas, where the latter hypothesis must be used twice in the proof of the third step formula, viz. with z sub­ stituted by x, and with z substituted by x-1. Without using the relation description D 1 EBD 1 .. to form an induction pUS piUS axiom, additional lemmata such as [Vx. plus(x O)=x] (to prove the base case) and [Vx,y. plus(x succ(y)) · succ(plus(x y))] (to prove the step case) are needed to verify statement '1' 3 · cf. [Boyer and Moore, 1979]. This is not required here and we consider this as an evidence for the strength of the proposed method.

Based on the above analysis we demand for an imple­ mentation that an induction theorem prover considers the r­ descriptions from which the domain generalizations were computed, if the quasi-commutation tests fail for the gene­ ralized forms, as we did for the example above.

5 Concluding Remarks

There are cases where commutation with a type may not help because quasi-commutation with a type is not a neces­ sary requirement for quasi-commutation, which in tum is not a necessary requirement for the well-foundedness of the union of well-founded relations. If all commutation tests fail, then the termination proof facility of an induction theorem prover has to be used, cf. [Boyer and Moore, 1979; Walther, 1988], hoping that it can prove the well­ roundedness of the separated union. However, this should always be the ultimate resort. Such direct well-foundedness proofs usually are much more difficult than the proofs necessitated by the commutation tests, as it easily can be observed from the examples presented above. This is because the latter deduction problems embody the knowled­ ge that the given relations are well-founded and, therefore, quite often can be proven by propositional reasoning and case analysis only.