theorem Th49: :: AOFA_I00:49

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 holds
( (g . (s,(x is_odd))) . b = (s . x) mod 2 & (g . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds
(g . (s,(x is_odd))) . z = s . z ) )