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 n, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
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 n, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for n, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for n, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let n, x, y, z, i be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) implies ((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g )
given d being Function such that 00: ( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) ; :: thesis: ((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
D1: ( i <> n & b <> i & n <> b ) by 00;
D2: ( i <> x & i <> y & i <> z & n <> x & n <> y & n <> z ) by 00;
let s be Element of Funcs X,INT ; :: according to AOFA_000:def 37 :: thesis: [s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g
set s2 = g . s,((x := 0 ) \; (y := 1));
set I1 = z := x;
set I2 = x := y;
set I3 = y += z;
set I = ((z := x) \; (x := y)) \; (y += z);
02: [s,((x := 0 ) \; (y := 1))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by AOFA_000:def 36;
03: for q being Element of Funcs X,INT holds
( (g . q,(((z := x) \; (x := y)) \; (y += z))) . n = q . n & (g . q,(((z := x) \; (x := y)) \; (y += z))) . i = q . i )

proof

let q be Element of Funcs X,INT ; :: thesis: ( (g . q,(((z := x) \; (x := y)) \; (y += z))) . n = q . n & (g . q,(((z := x) \; (x := y)) \; (y += z))) . i = q . i )
thus (g . q,(((z := x) \; (x := y)) \; (y += z))) . n = (g . (g . q,((z := x) \; (x := y))),(y += z)) . n by AOFA_000:def 29
.= (g . q,((z := x) \; (x := y))) . n by D2, Th212
.= (g . (g . q,(z := x)),(x := y)) . n by AOFA_000:def 29
.= (g . q,(z := x)) . n by D2, Th211
.= q . n by D2, Th211 ; :: thesis: (g . q,(((z := x) \; (x := y)) \; (y += z))) . i = q . i
thus (g . q,(((z := x) \; (x := y)) \; (y += z))) . i = (g . (g . q,((z := x) \; (x := y))),(y += z)) . i by AOFA_000:def 29
.= (g . q,((z := x) \; (x := y))) . i by D2, Th212
.= (g . (g . q,(z := x)),(x := y)) . i by AOFA_000:def 29
.= (g . q,(z := x)) . i by D2, Th211
.= q . i by D2, Th211 ; :: thesis: verum

end;

ex d' being Function st
( d' . b = 0 & d' . n = 1 & d' . i = 2 ) by D1, Lem3;
then for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)) is_terminating_wrt g by 03, ThT4, AOFA_000:104;
then [(g . s,((x := 0 ) \; (y := 1))),(for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by AOFA_000:def 37;
hence [s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by 02, AOFA_000:def 35; :: thesis: verum