let A be 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 being Variable of g
for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let X be 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
for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let s be 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
for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let b be Element of X; for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x being Variable of g
for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); for x being Variable of g
for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let x be Variable of g; for i being Integer holds
( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
let i be Integer; ( ( s . x <= i implies g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) implies s . x <= i ) & ( s . x >= i implies g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) implies s . x >= i ) )
( g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x leq i))) . b <> 0 )
by Th2;
hence
( s . x <= i iff g . (s,(x leq i)) in (Funcs (X,INT)) \ (b,0) )
by Th34; ( s . x >= i iff g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) )
( g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x geq i))) . b <> 0 )
by Th2;
hence
( s . x >= i iff g . (s,(x geq i)) in (Funcs (X,INT)) \ (b,0) )
by Th34; verum