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 A1: d . b = 0 and
A2: d . n = 1 and
A3: d . x = 2 and
A4: d . y = 3 and
A5: d . z = 4 and
A6: 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
A7: i <> y by A4, A6;
A8: n <> z by A2, A5;
A9: n <> y by A2, A4;
A10: n <> x by A2, A3;
A11: i <> z by A5, A6;
set I = ((z := x) \; (x := y)) \; (y += z);
set I1 = z := x;
set I2 = x := y;
set I3 = y += z;
A12: i <> x by A3, A6;
A13: 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 A9, Th30
.= (g . (g . q,(z := x)),(x := y)) . n by AOFA_000:def 29
.= (g . q,(z := x)) . n by A10, Th27
.= q . n by A8, Th27 ; :: 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 A7, Th30
.= (g . (g . q,(z := x)),(x := y)) . i by AOFA_000:def 29
.= (g . q,(z := x)) . i by A12, Th27
.= q . i by A11, Th27 ; :: thesis: verum

end;

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));
i <> n by A2, A6;
then ex d9 being Function st
( d9 . b = 0 & d9 . n = 1 & d9 . i = 2 ) by A1, A2, A6, Th1;
then for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)) is_terminating_wrt g by A13, Th54, AOFA_000:104;
then A14: [(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;
[s,((x := 0 ) \; (y := 1))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by AOFA_000:def 36;
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 A14, AOFA_000:def 35; :: thesis: verum