Definition. Strategy and tactic configuration [ftip-00EV]

At depth \(d\), let \(\mathcal K_d\) be a finite set of tactic behaviors and let a strategy select a conditional tactic in \(\mathcal K_d\). A realized configuration is \((k_2,\ldots ,k_n)\). The notation records expressible choices, not the number of choices an implementation actually discovers.