Integrity Constraints on Instances

The schemas above can be instantiated in many ways. However, some constraints need to be verified by these instantiation processes in order to result in valid divide-and-conquer logic algorithms. The constraints on instances of version 4 are as follows. 

The instance of X, that is the induction parameter, must be of an inductive type. Indeed, otherwise, its decomposition into tails TX that are each smaller thanX according to some well-founded relation would be impossible. 

The minimal and non-minimal forms must be mutually exclusive over the domain of the induction parameter. This means that the chosen instance of the formula  

The decomposition of X must yield tails 7X, that are each smaller than X according to some well-founded relation . This means that the formula  

---