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 . 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 . 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 . 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 . 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 . 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 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 := 1),(i leq n),(i += 1),(s *= x))) 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 *= x))) . n = q . n & (g . (q,(s *= x))) . 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 := 1),(i leq n),(i += 1),(s *= x))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g)

set t = . (1,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 := (. (1,A,g))),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g by A6, Th54, AOFA_000:104;

then A9: [(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) ;

[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 := 1),(i leq n),(i += 1),(s *= x))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by A9, AOFA_000:def 35; :: thesis: verum

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 . 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 . 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 . 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 . 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 . 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 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 := 1),(i leq n),(i += 1),(s *= x))) 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 *= x))) . n = q . n & (g . (q,(s *= x))) . 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 := 1),(i leq n),(i += 1),(s *= x))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g)

set t = . (1,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 := (. (1,A,g))),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g by A6, Th54, AOFA_000:104;

then A9: [(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) ;

[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 := 1),(i leq n),(i += 1),(s *= x))))] in TerminatingPrograms (A,(Funcs (X,INT)),((Funcs (X,INT)) \ (b,0)),g) by A9, AOFA_000:def 35; :: thesis: verum