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 x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) 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 x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) 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 x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x, n, s, i being Variable of g st ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds
(s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let x, n, s, i be Variable of g; :: thesis: ( ex d being Function st
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies (s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g )
given d being Function such that 00: ( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) ; :: thesis: (s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g
D1: ( s <> i & s <> n & i <> n & b <> i & n <> b ) by 00;
set t = . 1,A,g;
let q be Element of Funcs X,INT ; :: according to AOFA_000:def 37 :: thesis: [q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g
02: [q,(s := 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,(s *= x)) . n = q . n & (g . q,(s *= x)) . i = q . i ) by D1, Th213;
ex d' being Function st
( d' . b = 0 & d' . n = 1 & d' . i = 2 ) by D1, Lem3;
then for-do (i := (. 1,A,g)),(i leq n),(i += 1),(s *= x) is_terminating_wrt g by 03, ThT4, AOFA_000:104;
then [(g . q,(s := 1)),(for-do (i := (. 1,A,g)),(i leq n),(i += 1),(s *= x))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by AOFA_000:def 37;
hence [q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by 02, AOFA_000:def 35; :: thesis: verum