for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x))) is_terminating_wrt g