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, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

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, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

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, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let b be Element of X; :: thesis: 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 leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let x, y be Variable of g; :: thesis: ( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x leq y))) . b <> 0 ) by Th2;

hence ( s . x <= s . y iff g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) by Th35; :: thesis: ( s . x >= s . y iff g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) )

( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x geq y))) . b <> 0 ) by Th2;

hence ( s . x >= s . y iff g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) by Th35; :: thesis: verum

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

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, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

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, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let b be Element of X; :: thesis: 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 leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x, y being Variable of g holds

( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

let x, y be Variable of g; :: thesis: ( ( s . x <= s . y implies g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) implies s . x <= s . y ) & ( s . x >= s . y implies g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) implies s . x >= s . y ) )

( g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x leq y))) . b <> 0 ) by Th2;

hence ( s . x <= s . y iff g . (s,(x leq y)) in (Funcs (X,INT)) \ (b,0) ) by Th35; :: thesis: ( s . x >= s . y iff g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) )

( g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) iff (g . (s,(x geq y))) . b <> 0 ) by Th2;

hence ( s . x >= s . y iff g . (s,(x geq y)) in (Funcs (X,INT)) \ (b,0) ) by Th35; :: thesis: verum