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
( ( not t . s is even implies g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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
( ( not t . s is even implies g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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
( ( not t . s is even implies g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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
( ( not t . s is even implies g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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
( ( not t . s is even implies f . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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: ( ( not t . s is even implies f . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(t is_odd ) in (Funcs X,INT ) \ b,0 implies not t . s is even ) & ( 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 ) )
01: ( (f . s,(t is_odd )) . b = (t . s) mod 2 & (f . s,(t is_even )) . b = ((t . s) + 1) mod 2 ) by Th118;
02: ( (t . s) mod 2 = 0 or (t . s) mod 2 = 1 ) by PRE_FF:6;
03: t . s = (((t . s) div 2) * 2) + ((t . s) mod 2) by INT_1:86;
thus ( not t . s is even iff f . s,(t is_odd ) in (Funcs X,INT ) \ b,0 ) by 01, 02, 03, LemTS; :: thesis: ( t . s is even iff f . s,(t is_even ) in (Funcs X,INT ) \ b,0 )
02: ( ((t . s) + 1) mod 2 = 0 or ((t . s) + 1) mod 2 = 1 ) by PRE_FF:6;
03: (t . s) + 1 = ((((t . s) + 1) div 2) * 2) + (((t . s) + 1) mod 2) by INT_1:86;
thus ( t . s is even iff f . s,(t is_even ) in (Funcs X,INT ) \ b,0 ) by 01, 02, 03, LemTS; :: thesis: verum