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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

reconsider b9 = b as Variable of f by Def2;

let x be Variable of f; :: thesis: for i being Integer holds

( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

let i be Integer; :: thesis: ( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

set v = ^ b9;

A2: (^ b9) . s = b ;

A3: ( (. x) . s >= i implies IFGT (i,((. x) . s),1,0) = 0 ) by XXREAL_0:def 11;

A4: ( (. x) . s < i implies IFGT (i,((. x) . s),1,0) = 1 ) by XXREAL_0:def 11;

A5: (gt ((. (i,A,f)),(. x))) . s = IFGT (((. (i,A,f)) . s),((. x) . s),1,0) by Def32;

A6: ( (. x) . s <= i implies IFGT (((. x) . s),i,1,0) = 0 ) by XXREAL_0:def 11;

A7: (gt ((. x),(. (i,A,f)))) . s = IFGT (((. x) . s),((. (i,A,f)) . s),1,0) by Def32;

A8: ( (. x) . s > i implies IFGT (((. x) . s),i,1,0) = 1 ) by XXREAL_0:def 11;

(. x) . s = s . ((^ x) . s) by Def19;

hence ( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) ) by A2, A8, A6, A4, A3, A7, A5, Th24; :: 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 being Variable of g

for i being Integer holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (g . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (g . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (g . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (g . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (g . (s,(x gt i))) . z = s . z & (g . (s,(x lt 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 holds

( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

reconsider b9 = b as Variable of f by Def2;

let x be Variable of f; :: thesis: for i being Integer holds

( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

let i be Integer; :: thesis: ( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) )

set v = ^ b9;

A2: (^ b9) . s = b ;

A3: ( (. x) . s >= i implies IFGT (i,((. x) . s),1,0) = 0 ) by XXREAL_0:def 11;

A4: ( (. x) . s < i implies IFGT (i,((. x) . s),1,0) = 1 ) by XXREAL_0:def 11;

A5: (gt ((. (i,A,f)),(. x))) . s = IFGT (((. (i,A,f)) . s),((. x) . s),1,0) by Def32;

A6: ( (. x) . s <= i implies IFGT (((. x) . s),i,1,0) = 0 ) by XXREAL_0:def 11;

A7: (gt ((. x),(. (i,A,f)))) . s = IFGT (((. x) . s),((. (i,A,f)) . s),1,0) by Def32;

A8: ( (. x) . s > i implies IFGT (((. x) . s),i,1,0) = 1 ) by XXREAL_0:def 11;

(. x) . s = s . ((^ x) . s) by Def19;

hence ( ( s . x > i implies (f . (s,(x gt i))) . b = 1 ) & ( s . x <= i implies (f . (s,(x gt i))) . b = 0 ) & ( s . x < i implies (f . (s,(x lt i))) . b = 1 ) & ( s . x >= i implies (f . (s,(x lt i))) . b = 0 ) & ( for z being Element of X st z <> b holds

( (f . (s,(x gt i))) . z = s . z & (f . (s,(x lt i))) . z = s . z ) ) ) by A2, A8, A6, A4, A3, A7, A5, Th24; :: thesis: verum