Safe While Statement
This statement using only addition constraints in s, f, g is safe! It negates the ability of a while loop to become infinite because it is safe because it will not find the same information twice without finding other new information.
While(x,y,state,...) :- . While(x,y,state,...) :- (condition), state=s{state1,x1,y1,...}, x=f(state1,x1,y1,...), y=g(state,x1,y1,...), while(state1,x1,y1,...).