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
( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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
( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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
( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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
( ( s . x is odd implies g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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
( ( s . x is odd implies f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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: ( ( s . x is odd implies f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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) . s = s . x by Th22;
hence ( ( s . x is odd implies f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) ) & ( f . (s,(x is_odd)) in (Funcs (X,INT)) \ (b,0) implies s . x is odd ) & ( 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 Th50; :: thesis: verum