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) ;
[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