Changing inductive definitions

In searchtrees.v , the predicates min and maj are inductively defined with the help of the predicate occ. Give another definition, whithout using occ, and compare the ease of development in the two approaches. You should be able to redo the all development with the new definitions.

Solution

This file contains some lemmas which establish the relationship between both definitions. You should be able to build a development similar to using these lemmas.

Going home

Pierre Castéran