(¬∃k.z=k∗succ(succ(0)) ∧ ∃h.((¬(h=0)) ∧y=z+h)