for n being Nat st n >= 1 holds
ZeroTuring computes n const 0