 where \(\phi\) is a functional variable of r-type \((\tau)/n\) and x is a variable of r-type \(\tau\), and the bound variables of A are all of order less than the order of \(\phi\) and the free variables of A are all of order not greater than the order of \(\phi\).