Decompose predicate-variable

An instantiation of the Decompose predicate-variable deterministically decomposes, in the non-minimal case, the induction parameter, say X, into a vector HX of heads and a vector TX of tails, the tails TXj being smaller than X according to some well-founded relation. These tails are meant for the recursive computation of the tails TYj of the other parameter, say Y. Step 3 yields LA ir) by instantiating the Decompose predicate-variable by means of the Database Method, which here relies on a database of type-specific decomposition formulas. 

Note the redundancy between the instantiations of the NonMinimal and Decompose predicate-variables. This logic algorithm is thus equivalent to its predecessor. 

The objective at Step 3 is to instantiate the predicate-variable Decompose of the divide-and-conquer schema. This amounts to transforming LAi r) into LA ir) such that it is covered by the following schema ... 

---