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 A1: 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 A2: d . b = 0 and

A3: d . n = 1 and

A4: 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 )

set C = i leq n;

set J = I \; (i += 1);

assume that

A5: 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

A6: S is_invariant_wrt i := t,g and

A7: S is_invariant_wrt I,g and

A8: S is_invariant_wrt i leq n,g and

A9: 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 A10: g . (s,(i := t)) in S by A6;

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 A5, A7, A8, A9;

then A11: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . ((g . (s,(i := t))),(i leq n)) by A2, A3, A4, A10, Th53;

set Q = while ((i leq n),(I \; (i += 1)));

A12: i leq n is_terminating_wrt g by AOFA_000:104;

A13: [s,(i := t)] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by AOFA_000:def 36;

S is_invariant_wrt I \; (i += 1),g by A7, A9, AOFA_000:109;

then A14: 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 ;

i += 1 is_terminating_wrt g,S by AOFA_000:107;

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 A1, A7, A8, A10, A11, A12, A14, AOFA_000:111, AOFA_000:116;

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 A13, AOFA_000:def 35; :: thesis: verum

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 A1: 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 A2: d . b = 0 and

A3: d . n = 1 and

A4: 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 )

set C = i leq n;

set J = I \; (i += 1);

assume that

A5: 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

A6: S is_invariant_wrt i := t,g and

A7: S is_invariant_wrt I,g and

A8: S is_invariant_wrt i leq n,g and

A9: 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 A10: g . (s,(i := t)) in S by A6;

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 A5, A7, A8, A9;

then A11: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . ((g . (s,(i := t))),(i leq n)) by A2, A3, A4, A10, Th53;

set Q = while ((i leq n),(I \; (i += 1)));

A12: i leq n is_terminating_wrt g by AOFA_000:104;

A13: [s,(i := t)] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by AOFA_000:def 36;

S is_invariant_wrt I \; (i += 1),g by A7, A9, AOFA_000:109;

then A14: 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 ;

i += 1 is_terminating_wrt g,S by AOFA_000:107;

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 A1, A7, A8, A10, A11, A12, A14, AOFA_000:111, AOFA_000:116;

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 A13, AOFA_000:def 35; :: thesis: verum