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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

let t be INT-Expression of A,f; :: thesis: ( ( t . s is odd implies f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

A1: ( (t . s) mod 2 = 0 or (t . s) mod 2 = 1 ) by PRE_FF:6;

A2: t . s = (((t . s) div 2) * 2) + ((t . s) mod 2) by INT_1:59;

(f . (s,(t is_odd))) . b = (t . s) mod 2 by Th48;

hence ( t . s is odd iff f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) by A1, A2, Th2; :: thesis: ( t . s is even iff f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) )

A3: ( ((t . s) + 1) mod 2 = 0 or ((t . s) + 1) mod 2 = 1 ) by PRE_FF:6;

A4: (t . s) + 1 = ((((t . s) + 1) div 2) * 2) + (((t . s) + 1) mod 2) by INT_1:59;

(f . (s,(t is_even))) . b = ((t . s) + 1) mod 2 by Th48;

hence ( t . s is even iff f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) by A3, A4, Th2; :: 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 t being INT-Expression of A,g holds

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

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

( ( t . s is odd implies f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

let t be INT-Expression of A,f; :: thesis: ( ( t . s is odd implies f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) implies t . s is odd ) & ( t . s is even implies f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) implies t . s is even ) )

A1: ( (t . s) mod 2 = 0 or (t . s) mod 2 = 1 ) by PRE_FF:6;

A2: t . s = (((t . s) div 2) * 2) + ((t . s) mod 2) by INT_1:59;

(f . (s,(t is_odd))) . b = (t . s) mod 2 by Th48;

hence ( t . s is odd iff f . (s,(t is_odd)) in (Funcs (X,INT)) \ (b,0) ) by A1, A2, Th2; :: thesis: ( t . s is even iff f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) )

A3: ( ((t . s) + 1) mod 2 = 0 or ((t . s) + 1) mod 2 = 1 ) by PRE_FF:6;

A4: (t . s) + 1 = ((((t . s) + 1) div 2) * 2) + (((t . s) + 1) mod 2) by INT_1:59;

(f . (s,(t is_even))) . b = ((t . s) + 1) mod 2 by Th48;

hence ( t . s is even iff f . (s,(t is_even)) in (Funcs (X,INT)) \ (b,0) ) by A3, A4, Th2; :: thesis: verum