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 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 ; :: 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 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 ; :: 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 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; :: 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 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 ; :: thesis: 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; :: thesis: ( ( 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 x9 = x, y9 = y as Element of X ;
set v = ^ b9;
set t = gt (. x),(. y);
A1: (^ b9) . s = b by FUNCOP_1:13;
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 by FUNCOP_1:13;
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, FUNCOP_1:13; :: thesis: verum