Step 2 Synthesis of Minimal and NonMinimal

We can now prove a theorem establishing that Step 1 is in line with the strategy  

Example 12-2 For the firstPlateaufi problem. Step 1 yields LA j (firstPlateau) as in Logic Algorithm 12-1, and exp(LA (firstPlateau)) as in Logic Algorithm 12-2. 

Example 12-3 For the compress problem. Step 1 yields a logic algorithm and its expansion as in Example 11-1. 

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  

---

What induction parameter to select Task A of Step 2 (Synthesis of Minimal and NonMinimal) does this non-deterministically by considering all parameters that are of an inductive type, and possibly by using some selection heuristics, or by listening to the specifier s preference hints. 

---