let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
let X be non empty countable set ; :: 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, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
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, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let x, y, z be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) implies while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } )
set P = { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } ;
given d being Function such that A1: d . b = 0 and
A2: d . x = 1 and
A3: d . y = 2 and
A4: d . z = 3 ; :: thesis: while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
set C = y gt 0 ;
set I = (((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z);

A5: now

let s be Element of Funcs X,INT ; :: thesis: ( s in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } & g . (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))),(y gt 0 ) in (Funcs X,INT ) \ b,0 implies g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } )
assume s in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } ; :: thesis: ( g . (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))),(y gt 0 ) in (Funcs X,INT ) \ b,0 implies g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } )
then ex s9 being Element of Funcs X,INT st
( s9 = s & s9 . x >= 0 & s9 . y >= 0 ) ;
then reconsider n = s . x, m = s . y as Element of NAT by INT_1:16;
assume g . (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))),(y gt 0 ) in (Funcs X,INT ) \ b,0 ; :: thesis: g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
A6: (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))) . x = m by A1, A2, A3, A4, Lm2;
(g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))) . y = abs ((s . x) - (s . y)) by A1, A2, A3, A4, Lm2;
hence g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } by A6; :: thesis: verum

end;

A7: now

let s be Element of Funcs X,INT ; :: thesis: ( g . s,(y gt 0 ) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } implies g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),g . s,(y gt 0 ) )
set s1 = g . s,(y gt 0 );
A8: ( s . y <= 0 implies (g . s,(y gt 0 )) . b = 0 ) by Th38;
assume g . s,(y gt 0 ) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } ; :: thesis: g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),g . s,(y gt 0 )
then ex s9 being Element of Funcs X,INT st
( s9 = g . s,(y gt 0 ) & s9 . x >= 0 & s9 . y >= 0 ) ;
then reconsider n = (g . s,(y gt 0 )) . x, m = (g . s,(y gt 0 )) . y as Element of NAT by INT_1:16;
A9: n = n ;
( s . y > 0 implies (g . s,(y gt 0 )) . b = 1 ) by Th38;
then ( g . s,(y gt 0 ) in (Funcs X,INT ) \ b,0 iff m > 0 ) by A8, Th2, Th38;
hence g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),g . s,(y gt 0 ) by A1, A2, A3, A4, A9, Lm2; :: thesis: verum

end;

A10: { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } is_invariant_wrt y gt 0 ,g

proof

let s be Element of Funcs X,INT ; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } or g . s,(y gt 0 ) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } )
set s1 = g . s,(y gt 0 );
assume s in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } ; :: thesis: g . s,(y gt 0 ) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
then A11: ex s9 being Element of Funcs X,INT st
( s9 = s & s9 . x >= 0 & s9 . y >= 0 ) ;
A12: (g . s,(y gt 0 )) . y = s . y by A1, A3, Th38;
(g . s,(y gt 0 )) . x = s . x by A1, A2, Th38;
hence g . s,(y gt 0 ) in { s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } by A11, A12; :: thesis: verum

end;

y gt 0 is_terminating_wrt g by AOFA_000:104;
hence while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) } by A10, A5, A7, AOFA_000:107, AOFA_000:118; :: thesis: verum