theorem Th39:
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
x,
y being
Variable of
g holds
( (
s . x > s . y implies
(g . (s,(x gt y))) . b = 1 ) & (
s . x <= s . y implies
(g . (s,(x gt y))) . b = 0 ) & (
s . x < s . y implies
(g . (s,(x lt y))) . b = 1 ) & (
s . x >= s . y implies
(g . (s,(x lt y))) . b = 0 ) & ( for
z being
Element of
X st
z <> b holds
(
(g . (s,(x gt y))) . z = s . z &
(g . (s,(x lt y))) . z = s . z ) ) )