theorem
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))
in (Funcs (X,INT)) \ (
b,
0) ) & (
g . (
s,
(x gt y))
in (Funcs (X,INT)) \ (
b,
0) implies
s . x > s . y ) & (
s . x < s . y implies
g . (
s,
(x lt y))
in (Funcs (X,INT)) \ (
b,
0) ) & (
g . (
s,
(x lt y))
in (Funcs (X,INT)) \ (
b,
0) implies
s . x < s . y ) )