for N being with_zero set
for l being Element of NAT holds SUCC (l,(STC N)) = {l,(NextLoc (l,(STC N)))}