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 P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
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 P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
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 P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
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 P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
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 P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for P being set
for I being Element of A st I is_terminating_wrt g,P 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 st s in P holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & P is_invariant_wrt i := t,g & P is_invariant_wrt I,g & P is_invariant_wrt i leq n,g & P is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,P
set Z = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let S be set ; :: thesis: for I being Element of A st I is_terminating_wrt g,S 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 st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & S is_invariant_wrt i := t,g & S is_invariant_wrt I,g & S is_invariant_wrt i leq n,g & S is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S
let I be Element of A; :: thesis: ( I is_terminating_wrt g,S 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 st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & S is_invariant_wrt i := t,g & S is_invariant_wrt I,g & S is_invariant_wrt i leq n,g & S is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S )
assume 00: I is_terminating_wrt g,S ; :: 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 st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & S is_invariant_wrt i := t,g & S is_invariant_wrt I,g & S is_invariant_wrt i leq n,g & S is_invariant_wrt i += 1,g holds
for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S
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 st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) & S is_invariant_wrt i := t,g & S is_invariant_wrt I,g & S is_invariant_wrt i leq n,g & S is_invariant_wrt i += 1,g implies for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S )
given d being Function such that 01: ( d . b = 0 & d . n = 1 & d . i = 2 ) ; :: thesis: ( ex s being Element of Funcs X,INT st
( s in S & not ( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) ) or not S is_invariant_wrt i := t,g or not S is_invariant_wrt I,g or not S is_invariant_wrt i leq n,g or not S is_invariant_wrt i += 1,g or for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S )
assume that
02: for s being Element of Funcs X,INT st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i ) and
04: ( S is_invariant_wrt i := t,g & S is_invariant_wrt I,g & S is_invariant_wrt i leq n,g & S is_invariant_wrt i += 1,g ) ; :: thesis: for-do (i := t),(i leq n),(i += 1),I is_terminating_wrt g,S
let s be Element of Funcs X,INT ; :: according to AOFA_000:def 38 :: thesis: ( not s in S or [s,(for-do (i := t),(i leq n),(i += 1),I)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g )
assume s in S ; :: thesis: [s,(for-do (i := t),(i leq n),(i += 1),I)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g
then 03: g . s,(i := t) in S by 04, AOFA_000:def 39;
set P = for-do (i := t),(i leq n),(i += 1),I;
set C = i leq n;
set J = I \; (i += 1);
set Q = while (i leq n),(I \; (i += 1));
for s being Element of Funcs X,INT st s in S holds
( (g . s,I) . n = s . n & (g . s,I) . i = s . i & g . s,I in S & g . s,(i leq n) in S & g . s,(i += 1) in S ) by 02, 04, AOFA_000:def 39;
then 06: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (g . s,(i := t)),(i leq n) by 01, 03, ThT12;
07: ( i += 1 is_terminating_wrt g,S & i leq n is_terminating_wrt g ) by AOFA_000:104, AOFA_000:107;
then 09: ( S is_invariant_wrt I \; (i += 1),g & I \; (i += 1) is_terminating_wrt g,S ) by 00, 04, AOFA_000:109, AOFA_000:111;
then for s being Element of Funcs X,INT st s in S & g . (g . s,(I \; (i += 1))),(i leq n) in (Funcs X,INT ) \ b,0 holds
g . s,(I \; (i += 1)) in S by AOFA_000:def 39;
then 08: [(g . s,(i := t)),(while (i leq n),(I \; (i += 1)))] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g by 03, 04, 06, 07, 09, AOFA_000:116;
( for-do (i := t),(i leq n),(i += 1),I = (i := t) \; (while (i leq n),(I \; (i += 1))) & [s,(i := t)] in TerminatingPrograms A,(Funcs X,INT ),((Funcs X,INT ) \ b,0 ),g ) by AOFA_000:def 36;
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 08, AOFA_000:def 35; :: thesis: verum