Dimensional inference rule format

A style of formal definition that defines a set inductively as the smallest set closed under the rules - an element is in the set iff it can be derived by a finite Derivation tree of rule applications.