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 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 ) )

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 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 ) )

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 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 ) )

let b be Element of X; :: thesis: 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 ) )

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x being Variable of f holds

( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) )

let x be Variable of f; :: thesis: ( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) )

(. x) . s = s . x by Th22;

hence ( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) ) by Th48; :: thesis: verum

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 ) )

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 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 ) )

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 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 ) )

let b be Element of X; :: thesis: 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 ) )

let f be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x being Variable of f holds

( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) )

let x be Variable of f; :: thesis: ( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) )

(. x) . s = s . x by Th22;

hence ( (f . (s,(x is_odd))) . b = (s . x) mod 2 & (f . (s,(x is_even))) . b = ((s . x) + 1) mod 2 & ( for z being Element of X st z <> b holds

(f . (s,(x is_odd))) . z = s . z ) ) by Th48; :: thesis: verum