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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } )
set P = { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }
set C = y gt 0;
set I = (((z := x) \; (z %= y)) \; (x := y)) \; (y := z);
A5: { s where s is Element of Funcs (X,INT) : ( s . x > s . y & 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 > s . y & s . y >= 0 ) } or g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } )
set s1 = g . (s,(y gt 0));
assume s in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } ; :: thesis: g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }
then A6: ex s9 being Element of Funcs (X,INT) st
( s9 = s & s9 . x > s9 . y & s9 . y >= 0 ) ;
A7: (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 > s . y & s . y >= 0 ) } by A6, A7; :: thesis: verum
end;
A8: now :: thesis: for s being Element of Funcs (X,INT) st s in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } & g . ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))),(y gt 0)) in (Funcs (X,INT)) \ (b,0) holds
g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }
let s be Element of Funcs (X,INT); :: thesis: ( s in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } & g . ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))),(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } )
assume s in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } ; :: thesis: ( g . ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))),(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } )
then ex s9 being Element of Funcs (X,INT) st
( s9 = s & s9 . x > s9 . y & s9 . y >= 0 ) ;
then reconsider m = s . y as Element of NAT by INT_1:3;
assume g . ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))),(y gt 0)) in (Funcs (X,INT)) \ (b,0) ; :: thesis: g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) }
then (g . ((g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))),(y gt 0))) . b <> 0 by Th2;
then A9: (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y > 0 by Th38;
A10: (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y by A1, A2, A3, A4, Lm1;
A11: (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) by A1, A2, A3, A4, Lm1;
then m <> 0 by A9, INT_1:def 10;
then (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x > (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y by A11, A10, NEWTON:65;
hence g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } by A9; :: thesis: verum
end;
A12: now :: thesis: for s being Element of Funcs (X,INT) st g . (s,(y gt 0)) in { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } holds
g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0))
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 > s . y & s . y >= 0 ) } implies g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0)) )
set s1 = g . (s,(y gt 0));
A13: ( 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 > s . y & s . y >= 0 ) } ; :: thesis: g iteration_terminates_for ((((z := x) \; (z %= y)) \; (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 > s9 . y & s9 . y >= 0 ) ;
then reconsider m = (g . (s,(y gt 0))) . y as Element of NAT by INT_1:3;
( 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 A13, Th2, Th38;
hence g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0)) by A1, A2, A3, A4, Lm1; :: thesis: verum
end;
y gt 0 is_terminating_wrt g by AOFA_000:104;
hence while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) is_terminating_wrt g, { s where s is Element of Funcs (X,INT) : ( s . x > s . y & s . y >= 0 ) } by A5, A8, A12, AOFA_000:107, AOFA_000:118; :: thesis: verum