Once Lemma 3.6 has been proved, it is easy to reduce the bounded domino problem to consistency. Lemma 3.7 Let be a domino system.
T w enforces the initial condition.
We use an atomic concept C d for each tile . Also, for a fixed domino system , is obviously polynomially computable. It should be noted that it is open if the problem can be decided in , if binary coding of numbers is used, since the reduction of only yields decidability in 2- . This shows that the coding of numbers indeed has an influence on the complexity of the reasoning problem. For unary coding, we needed both inverse roles and cardinality restrictions for the reduction.