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