Minimal predicate-variable

A schema-variable c represents the number of different sub-cases of the non-minimal case. This new schema supersedes the previous schema if c is bound to 1, and the Discriminatei predicate-variable is bound to a predicate that always holds. 

Instances of Solve may be defined by fairly complex formulas, including divisions into sub-cases and the corresponding discriminating mechanisms, just as in non-minimal cases. But since this is relatively exceptional, we prefer to keep the schema simple, and always treat such a formula as the instance of a single predicate-variable. 

An instantiation of the Minimal (respectively NonMinimal) predicate-variable tests whether the induction parameter is of a minimal (respectively non-minimal) form. These forms must be mutually exclusive over the domain of the induction parameter. Step 2 yields LAiir) by first selecting an induction parameter, and then instantiating the Minimal and NonMinimal predicate-variables by means of a so-called Database Method, which here relies on a database of type-specific form-identifying formulas. 

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. 

An instantiation of the Solve (respectively SolveNonMinj ) predicate-variable computes, in the minimal case (respectively the non-recursive non-minimal case), the value of the other parameter Y from the induction parameter X. Step 5 yields LA r) by using similar methods to those of Steps 6 and 7. 

An instantiation of the Minimal (respectively NonMinimal) predicate-variable tests whether the induction parameter is of a minimal (respectively non-minimal) form. 

The objective at Step 2 is to instantiate the predicate-variables Minimal and NonMinimal of the divide-and-conquer schema. This amounts to transforming LA ir) into LA2 r) such that it is covered by the following schema ... 

Second, it is the very focus on structural aspects of the induction parameter (its size, that is) that makes this database approach possible. If semantic aspects of the induction parameter (its value, that is) also have to be taken into account, then a deductive approach reasoning backwards from instances of all other predicate-variables becomes necessary [Smith 85]. We here clearly separate these aspects the size of the induction parameter is analyzed at Step 2 for instantiating Minimal and NonMinimal, and its value is analyzed at Step 7 for instantiating the Discriminate... 

The state updating functions combine information about the constraints on the state variables with the objective function minimization. The feasibility predicate forces the state variables to obey certain constraints, such as the nonoverlap of batches, forcing the start-times of successive operations to be greater than the end-times of the previous operation. The constraints do not force the start-times to be equal to the previous... 

---