let A be Euclidean preIfWhileAlgebra; :: thesis: 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 t being INT-Expression of A,g holds
( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )
let X be non empty countable set ; :: thesis: 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 t being INT-Expression of A,g holds
( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )
let s be Element of Funcs (X,INT); :: thesis: for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for t being INT-Expression of A,g holds
( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for t being INT-Expression of A,g holds
( (g . (s,(t is_odd))) . b = (t . s) mod 2 & (g . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (g . (s,(t is_odd))) . z = s . z & (g . (s,(t is_even))) . z = s . z ) ) )
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for t being INT-Expression of A,f holds
( (f . (s,(t is_odd))) . b = (t . s) mod 2 & (f . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (f . (s,(t is_odd))) . z = s . z & (f . (s,(t is_even))) . z = s . z ) ) )
let t be INT-Expression of A,f; :: thesis: ( (f . (s,(t is_odd))) . b = (t . s) mod 2 & (f . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (f . (s,(t is_odd))) . z = s . z & (f . (s,(t is_even))) . z = s . z ) ) )
reconsider y = b as Variable of f by Def2;
A1: t is_odd = y := (t mod (. (2,A,f))) ;
dom (t + 1) = Funcs (X,INT) by FUNCT_2:def 1;
then A2: (t + 1) . s = 1 + (t . s) by VALUED_1:def 2;
A3: (. (2,A,f)) . s = 2 ;
then A4: ((t + 1) mod (. (2,A,f))) . s = ((t + 1) . s) mod 2 by Def30;
(t mod (. (2,A,f))) . s = (t . s) mod 2 by A3, Def30;
hence ( (f . (s,(t is_odd))) . b = (t . s) mod 2 & (f . (s,(t is_even))) . b = ((t . s) + 1) mod 2 & ( for z being Element of X st z <> b holds
( (f . (s,(t is_odd))) . z = s . z & (f . (s,(t is_even))) . z = s . z ) ) ) by A1, A2, A4, Th26; :: thesis: verum