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, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) 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, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) 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, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g
let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for n, s, i being Variable of g st ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g
set S = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (b,0);
let n, s, i be Variable of g; :: thesis: ( ex d being Function st
( d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies (s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g )
given d being Function such that A1: d . n = 1 and
A2: d . s = 2 and
A3: d . i = 3 and
A4: d . b = 4 ; :: thesis: (s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))) is_terminating_wrt g
A5: s <> n by A1, A2;
s <> i by A2, A3;
then A6: for q being Element of Funcs (X,INT) holds
( (g . (q,(s *= i))) . n = q . n & (g . (q,(s *= i))) . i = q . i ) by A5, Th33;
A7: n <> b by A1, A4;
A8: b <> i by A3, A4;
let q be Element of Funcs (X,INT); :: according to AOFA_000:def 37 :: thesis: [q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g)
set t = . (2,A,g);
i <> n by A1, A3;
then ex d9 being Function st
( d9 . b = 0 & d9 . n = 1 & d9 . i = 2 ) by A8, A7, Th1;
then for-do ((i := (. (2,A,g))),(i leq n),(i += 1),(s *= i)) is_terminating_wrt g by A6, Th54, AOFA_000:104;
then A9: [(g . (q,(s := 1))),(for-do ((i := (. (2,A,g))),(i leq n),(i += 1),(s *= i)))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) ;
[q,(s := 1)] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by AOFA_000:def 36;
hence [q,((s := 1) \; (for-do ((i := 2),(i leq n),(i += 1),(s *= i))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by A9, AOFA_000:def 35; :: thesis: verum