for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for T being Subset of (Funcs (X,INT))
for f being Euclidean ExecutionFunction of A, Funcs (X,INT),T
for t being INT-Expression of A,f
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
for-do ((i := t),(i leq n),(i += 1),I) is_terminating_wrt g