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 being Variable of g
for i being integer number holds
( ( s . x <= i implies (g . s,(x leq i)) . b = 1 ) & ( s . x > i implies (g . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (g . s,(x geq i)) . b = 1 ) & ( s . x < i implies (g . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (g . s,(x leq i)) . z = s . z & (g . s,(x geq i)) . 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 being Variable of g
for i being integer number holds
( ( s . x <= i implies (g . s,(x leq i)) . b = 1 ) & ( s . x > i implies (g . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (g . s,(x geq i)) . b = 1 ) & ( s . x < i implies (g . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (g . s,(x leq i)) . z = s . z & (g . s,(x geq i)) . 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 being Variable of g
for i being integer number holds
( ( s . x <= i implies (g . s,(x leq i)) . b = 1 ) & ( s . x > i implies (g . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (g . s,(x geq i)) . b = 1 ) & ( s . x < i implies (g . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (g . s,(x leq i)) . z = s . z & (g . s,(x geq i)) . 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 being Variable of g
for i being integer number holds
( ( s . x <= i implies (g . s,(x leq i)) . b = 1 ) & ( s . x > i implies (g . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (g . s,(x geq i)) . b = 1 ) & ( s . x < i implies (g . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (g . s,(x leq i)) . z = s . z & (g . s,(x geq i)) . z = s . z ) ) )
let f be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x being Variable of f
for i being integer number holds
( ( s . x <= i implies (f . s,(x leq i)) . b = 1 ) & ( s . x > i implies (f . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (f . s,(x geq i)) . b = 1 ) & ( s . x < i implies (f . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . s,(x leq i)) . z = s . z & (f . s,(x geq i)) . z = s . z ) ) )
let x be Variable of f; :: thesis: for i being integer number holds
( ( s . x <= i implies (f . s,(x leq i)) . b = 1 ) & ( s . x > i implies (f . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (f . s,(x geq i)) . b = 1 ) & ( s . x < i implies (f . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . s,(x leq i)) . z = s . z & (f . s,(x geq i)) . z = s . z ) ) )
let i be integer number ; :: thesis: ( ( s . x <= i implies (f . s,(x leq i)) . b = 1 ) & ( s . x > i implies (f . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (f . s,(x geq i)) . b = 1 ) & ( s . x < i implies (f . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . s,(x leq i)) . z = s . z & (f . s,(x geq i)) . z = s . z ) ) )
reconsider b' = b as Variable of f by ELEM;
reconsider x' = x as Element of X ;
set v = ^ b';
set t = leq (. x),(. i,A,f);
04: (. i,A,f) . s = i by FUNCOP_1:13;
( (. x) . s = s . ((^ x) . s) & ^ x = (Funcs X,INT ) --> x ) by DEFvarexp;
then 01: ( s . x = (. x) . s & (^ b') . s = b ) by FUNCOP_1:13;
02: ( (. x) . s <= i implies IFGT ((. x) . s),i,0 ,1 = 1 ) by XXREAL_0:def 11;
03: ( (. x) . s > i implies IFGT ((. x) . s),i,0 ,1 = 0 ) by XXREAL_0:def 11;
05: ( (. x) . s >= i implies IFGT i,((. x) . s),0 ,1 = 1 ) by XXREAL_0:def 11;
06: ( (. x) . s < i implies IFGT i,((. x) . s),0 ,1 = 0 ) by XXREAL_0:def 11;
( (. x) leq (. i,A,f) = (^ b') := (leq (. x),(. i,A,f)) & (leq (. x),(. i,A,f)) . s = IFGT ((. x) . s),((. i,A,f) . s),0 ,1 & (. x) geq (. i,A,f) = (^ b') := (leq (. i,A,f),(. x)) & (leq (. i,A,f),(. x)) . s = IFGT ((. i,A,f) . s),((. x) . s),0 ,1 ) by DEFleq2;
hence ( ( s . x <= i implies (f . s,(x leq i)) . b = 1 ) & ( s . x > i implies (f . s,(x leq i)) . b = 0 ) & ( s . x >= i implies (f . s,(x geq i)) . b = 1 ) & ( s . x < i implies (f . s,(x geq i)) . b = 0 ) & ( for z being Element of X st z <> b holds
( (f . s,(x leq i)) . z = s . z & (f . s,(x geq i)) . z = s . z ) ) ) by 01, 02, 03, 04, 05, 06, Th100; :: thesis: verum