let A be Euclidean preIfWhileAlgebra; 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 ; 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; 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); 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; ( 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
; ((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);
( (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
;
(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
;
verum
end;
let s be Element of Funcs (X,INT); AOFA_000:def 37 [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; verum