The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.