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) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
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) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
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) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
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) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x being Variable of g
for i being integer number holds
( ( s . x <= i implies g . s,(x leq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
let x be Variable of g; :: thesis: for i being integer number holds
( ( s . x <= i implies g . s,(x leq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
let i be integer number ; :: thesis: ( ( s . x <= i implies g . s,(x leq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x leq i) in (Funcs X,INT ) \ b,0 implies s . x <= i ) & ( s . x >= i implies g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) & ( g . s,(x geq i) in (Funcs X,INT ) \ b,0 implies s . x >= i ) )
( g . s,(x leq i) in (Funcs X,INT ) \ b,0 iff (g . s,(x leq i)) . b <> 0 ) by LemTS;
hence ( s . x <= i iff g . s,(x leq i) in (Funcs X,INT ) \ b,0 ) by Th014; :: thesis: ( s . x >= i iff g . s,(x geq i) in (Funcs X,INT ) \ b,0 )
( g . s,(x geq i) in (Funcs X,INT ) \ b,0 iff (g . s,(x geq i)) . b <> 0 ) by LemTS;
hence ( s . x >= i iff g . s,(x geq i) in (Funcs X,INT ) \ b,0 ) by Th014; :: thesis: verum