let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for T being Subset of (Funcs X,INT )
for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for t being INT-Expression of A,f
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let X be non empty countable set ; :: thesis: for T being Subset of (Funcs X,INT )
for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for t being INT-Expression of A,f
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let T be Subset of (Funcs X,INT ); :: thesis: for f being Euclidean ExecutionFunction of A, Funcs X,INT ,T
for t being INT-Expression of A,f
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let f be Euclidean ExecutionFunction of A, Funcs X,INT ,T; :: thesis: for t being INT-Expression of A,f
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let t be INT-Expression of A,f; :: thesis: for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),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 I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for I being Element of A st I is_terminating_wrt g holds
for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let I be Element of A; :: thesis: ( I is_terminating_wrt g implies for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g )
assume A1: I is_terminating_wrt g ; :: thesis: for i, n being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let i, n be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) implies for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g )
i += 1 is_terminating_wrt g by AOFA_000:104;
then A2: I \; (i += 1) is_terminating_wrt g by A1, AOFA_000:110;
set Q = while (i leq n),(I \; (i += 1));
set P = for-do (i := t),(i leq n),(i += 1),I;
given d being Function such that A3: d . b = 0 and
A4: d . n = 1 and
A5: d . i = 2 ; :: thesis: ( ex s being Element of Funcs X,INT st
( (g . s,I) . n = s . n implies not (g . s,I) . i = s . i ) or for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g )
assume A6: for s being Element of Funcs X,INT holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ; :: thesis: for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g
let s be Element of Funcs X,INT ; :: according to AOFA_000:def 37 :: thesis: [s,(for-do (i := t),(i leq n),(i += 1),I)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g
A7: [s,(i := t)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by AOFA_000:def 36;
A8: i leq n is_terminating_wrt g by AOFA_000:104;
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (g . s,(i := t)),(i leq n) by A3, A4, A5, A6, Th52;
then [(g . s,(i := t)),(while (i leq n),(I \; (i += 1)))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by A8, A2, AOFA_000:114;
hence [s,(for-do (i := t),(i leq n),(i += 1),I)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by A7, AOFA_000:def 35; :: thesis: verum