theorem Th34: :: AOFA_I00:34

for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for s being Element of Funcs (X,INT)
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x being Variable of g
for i being Integer holds
( ( s . x <= i implies (g . (s,(x leq i))) . b = 1 ) & ( s . x > i implies (g . (s,(x leq i))) . b = 0 ) & ( s . x >= i implies (g . (s,(x geq i))) . b = 1 ) & ( s . x < i implies (g . (s,(x geq i))) . b = 0 ) & ( for z being Element of X st z <> b holds
( (g . (s,(x leq i))) . z = s . z & (g . (s,(x geq i))) . z = s . z ) ) )