We have implemented 16 small formulas for where and are small. For example, this formula

is implemented by a routine which returns a certificate whose components are