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
( ( not s . x is even implies g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies g . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x 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 x being Variable of g holds
( ( not s . x is even implies g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies g . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x 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 x being Variable of g holds
( ( not s . x is even implies g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies g . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x 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 x being Variable of g holds
( ( not s . x is even implies g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies g . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x is even ) )
let f be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x being Variable of f holds
( ( not s . x is even implies f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies f . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x is even ) )
let x be Variable of f; :: thesis: ( ( not s . x is even implies f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies f . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x is even ) )
( x is_odd = (. x) is_odd & (. x) . s = s . x ) by ThE1;
hence ( ( not s . x is even implies f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_odd ) in (Funcs X,INT ) \ b,0 implies not s . x is even ) & ( s . x is even implies f . s,(x is_even ) in (Funcs X,INT ) \ b,0 ) & ( f . s,(x is_even ) in (Funcs X,INT ) \ b,0 implies s . x is even ) ) by Th318; :: thesis: verum