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
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
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
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
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
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
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
for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
set h = g;
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 for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) ) )
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: for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
A5: z <> x by A2, A4;
let s be Element of Funcs (X,INT); :: thesis: ( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ) ) )
set I = (((z := x) \; (z %= y)) \; (x := y)) \; (y := z);
A6: y <> z by A3, A4;
A7: x <> y by A2, A3;

A8: now :: thesis: for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) )

let s be Element of Funcs (X,INT); :: thesis: ( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) )
reconsider s1 = g . (s,(z := x)) as Element of Funcs (X,INT) ;
reconsider s2 = g . (s1,(z %= y)) as Element of Funcs (X,INT) ;
reconsider s3 = g . (s2,(x := y)) as Element of Funcs (X,INT) ;
reconsider s4 = g . (s3,(y := z)) as Element of Funcs (X,INT) ;
A9: g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) = g . ((g . (s,(((z := x) \; (z %= y)) \; (x := y)))),(y := z)) by AOFA_000:def 29
.= g . ((g . ((g . (s,((z := x) \; (z %= y)))),(x := y))),(y := z)) by AOFA_000:def 29
.= s4 by AOFA_000:def 29 ;
A10: s1 . z = s . x by Th27;
A11: s2 . y = s1 . y by A6, Th44;
A12: s2 . z = (s1 . z) mod (s1 . y) by Th44;
A13: s3 . z = s2 . z by A5, Th27;
A14: s3 . x = s2 . y by Th27;
s1 . y = s . y by A6, Th27;
hence ( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) ) by A7, A9, A10, A11, A12, A14, A13, Th27; :: thesis: verum

end;

hence ( (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . y = (s . x) mod (s . y) ) ; :: thesis: for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s )
deffunc H₁( Element of Funcs (X,INT)) -> Element of NAT = In (($1 . y),NAT);
defpred S₁[ Element of Funcs (X,INT)] means $1 . y > 0 ;
set C = y gt 0;
A15: for s being Element of Funcs (X,INT) st S₁[s] holds
( ( S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H₁(g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H₁(s) )

proof

let s be Element of Funcs (X,INT); :: thesis: ( S₁[s] implies ( ( S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H₁(g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H₁(s) ) )
assume A16: s . y > 0 ; :: thesis: ( ( S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] implies g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] ) & H₁(g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H₁(s) )
reconsider s9 = g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) as Element of Funcs (X,INT) ;
A17: s9 . y = (s . x) mod (s . y) by A8;
then A18: 0 <= s9 . y by A16, NEWTON:64;
reconsider s99 = g . (s9,(y gt 0)) as Element of Funcs (X,INT) ;
A19: g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) = s99 by AOFA_000:def 29;
A20: ( s9 . y <= 0 implies s99 . b = 0 ) by Th38;
( s9 . y > 0 implies s99 . b = 1 ) by Th38;
hence ( S₁[g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))] iff g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0))) in (Funcs (X,INT)) \ (b,0) ) by A19, A20, Th2, Th38; :: thesis: H₁(g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H₁(s)
s99 . y = s9 . y by A1, A3, Th38;
then A21: H₁(s99) = s9 . y by A18, INT_1:3, SUBSET_1:def 8;
A22: s9 . y < s . y by A16, A17, NEWTON:65;
then H₁(s) = s . y by A18, INT_1:3, SUBSET_1:def 8;
hence H₁(g . (s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0)))) < H₁(s) by A22, A21, AOFA_000:def 29; :: thesis: verum

end;

let n, m be Element of NAT ; :: thesis: not ( m = s . y & ( s in (Funcs (X,INT)) \ (b,0) implies m > 0 ) & ( m > 0 implies s in (Funcs (X,INT)) \ (b,0) ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s )
assume A23: m = s . y ; :: thesis: ( ( s in (Funcs (X,INT)) \ (b,0) & not m > 0 ) or ( m > 0 & not s in (Funcs (X,INT)) \ (b,0) ) or g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s )
assume ( s in (Funcs (X,INT)) \ (b,0) iff m > 0 ) ; :: thesis: g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s
then A24: ( s in (Funcs (X,INT)) \ (b,0) iff S₁[s] ) by A23;
g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s from AOFA_000:sch 3(A24, A15);
hence g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),s ; :: thesis: verum