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, 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 ) ) )
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, 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 ) ) )
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, 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 ) ) )
let b be 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 ) ) )
let f be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); for x, y being Variable of f holds
( ( s . x > s . y implies (f . (s,(x gt y))) . b = 1 ) & ( s . x <= s . y implies (f . (s,(x gt y))) . b = 0 ) & ( s . x < s . y implies (f . (s,(x lt y))) . b = 1 ) & ( s . x >= s . y implies (f . (s,(x lt y))) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . (s,(x gt y))) . z = s . z & (f . (s,(x lt y))) . z = s . z ) ) )
reconsider b9 = b as Variable of f by Def2;
let x, y be Variable of f; ( ( s . x > s . y implies (f . (s,(x gt y))) . b = 1 ) & ( s . x <= s . y implies (f . (s,(x gt y))) . b = 0 ) & ( s . x < s . y implies (f . (s,(x lt y))) . b = 1 ) & ( s . x >= s . y implies (f . (s,(x lt y))) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . (s,(x gt y))) . z = s . z & (f . (s,(x lt y))) . z = s . z ) ) )
set v = ^ b9;
A1:
(^ b9) . s = b
;
A2:
( (. x) . s > (. y) . s implies IFGT (((. x) . s),((. y) . s),1,0) = 1 )
by XXREAL_0:def 11;
A3:
(gt ((. x),(. y))) . s = IFGT (((. x) . s),((. y) . s),1,0)
by Def32;
A4:
( (. x) . s < (. y) . s implies IFGT (((. y) . s),((. x) . s),1,0) = 1 )
by XXREAL_0:def 11;
(. x) . s = s . ((^ x) . s)
by Def19;
then A5:
s . x = (. x) . s
;
A6:
( (. x) . s <= (. y) . s implies IFGT (((. x) . s),((. y) . s),1,0) = 0 )
by XXREAL_0:def 11;
A7:
(gt ((. y),(. x))) . s = IFGT (((. y) . s),((. x) . s),1,0)
by Def32;
A8:
( (. x) . s >= (. y) . s implies IFGT (((. y) . s),((. x) . s),1,0) = 0 )
by XXREAL_0:def 11;
(. y) . s = s . ((^ y) . s)
by Def19;
hence
( ( s . x > s . y implies (f . (s,(x gt y))) . b = 1 ) & ( s . x <= s . y implies (f . (s,(x gt y))) . b = 0 ) & ( s . x < s . y implies (f . (s,(x lt y))) . b = 1 ) & ( s . x >= s . y implies (f . (s,(x lt y))) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . (s,(x gt y))) . z = s . z & (f . (s,(x lt y))) . z = s . z ) ) )
by A5, A1, A2, A6, A4, A8, A3, A7, Th24; verum