theorem Th50:
for
A being
Euclidean preIfWhileAlgebra 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 ) )