NonMinimal 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 Minimal (respectively NonMinimal) predicate-variable tests whether the induction parameter is of a minimal (respectively non-minimal) form. 

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 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... 

---