let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set

for s being Element of Funcs (X,INT)

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let X be non empty countable set ; :: thesis: for s being Element of Funcs (X,INT)

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let s be Element of Funcs (X,INT); :: 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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let P be set ; :: thesis: for I being Element of A

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let I be Element of A; :: 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 P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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 P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P implies g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) )

given d being Function such that A1: d . b = 0 and

A2: d . n = 1 and

A3: d . i = 2 ; :: thesis: ( ex s being Element of Funcs (X,INT) st

( s in P & not ( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) or not s in P or g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) )

set J = i += 1;

set C = i leq n;

set S = Funcs (X,INT);

set h = g;

assume that

A4: 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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) and

A5: s in P ; :: thesis: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

defpred S_{1}[ Element of Funcs (X,INT)] means $1 in P;

reconsider s1 = g . (s,(i leq n)) as Element of Funcs (X,INT) ;

A6: S_{1}[s1]
by A4, A5;

deffunc H_{1}( Element of Funcs (X,INT)) -> Element of NAT = In (((($1 . n) + 1) - ($1 . i)),NAT);

defpred S_{2}[ Element of Funcs (X,INT)] means $1 . i <= $1 . n;

set T = (Funcs (X,INT)) \ (b,0);

A7: i <> n by A2, A3;

A8: for s being Element of Funcs (X,INT) st S_{1}[s] & s in (Funcs (X,INT)) \ (b,0) & S_{2}[s] holds

( S_{1}[g . (s,((I \; (i += 1)) \; (i leq n)))] & ( S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] implies g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) implies S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] ) & H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s) )

A18: ( s . i <= s . n implies s1 . b = 1 ) by Th35;

s1 . i = s . i by A1, A3, Th35;

then A19: ( s1 in (Funcs (X,INT)) \ (b,0) iff S_{2}[s1] )
by A1, A2, A17, A18, Th2, Th35;

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),s1 from AOFA_000:sch 4(A6, A19, A8);

hence g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) ; :: thesis: verum

for s being Element of Funcs (X,INT)

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let X be non empty countable set ; :: thesis: for s being Element of Funcs (X,INT)

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let s be Element of Funcs (X,INT); :: 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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let P be set ; :: thesis: for I being Element of A

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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

let I be Element of A; :: 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 P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P holds

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

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 P holds

( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) & s in P implies g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) )

given d being Function such that A1: d . b = 0 and

A2: d . n = 1 and

A3: d . i = 2 ; :: thesis: ( ex s being Element of Funcs (X,INT) st

( s in P & not ( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) ) or not s in P or g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) )

set J = i += 1;

set C = i leq n;

set S = Funcs (X,INT);

set h = g;

assume that

A4: 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 & g . (s,I) in P & g . (s,(i leq n)) in P & g . (s,(i += 1)) in P ) and

A5: s in P ; :: thesis: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))

defpred S

reconsider s1 = g . (s,(i leq n)) as Element of Funcs (X,INT) ;

A6: S

deffunc H

defpred S

set T = (Funcs (X,INT)) \ (b,0);

A7: i <> n by A2, A3;

A8: for s being Element of Funcs (X,INT) st S

( S

proof

A17:
( s . i > s . n implies s1 . b = 0 )
by Th35;
let s be Element of Funcs (X,INT); :: thesis: ( S_{1}[s] & s in (Funcs (X,INT)) \ (b,0) & S_{2}[s] implies ( S_{1}[g . (s,((I \; (i += 1)) \; (i leq n)))] & ( S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] implies g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) implies S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] ) & H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s) ) )

assume that

A9: S_{1}[s]
and

s in (Funcs (X,INT)) \ (b,0) and

A10: S_{2}[s]
; :: thesis: ( S_{1}[g . (s,((I \; (i += 1)) \; (i leq n)))] & ( S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] implies g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) implies S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] ) & H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s) )

set q = g . (s,(I \; (i += 1)));

set s1 = g . (s,I);

set q1 = g . ((g . (s,(I \; (i += 1)))),(i leq n));

A11: g . (s,(I \; (i += 1))) = g . ((g . (s,I)),(i += 1)) by AOFA_000:def 29;

(g . (s,I)) . i = s . i by A4, A9;

then (g . (s,(I \; (i += 1)))) . i = (s . i) + 1 by A11, Th28;

then A12: (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (s . i) + 1 by A1, A3, Th35;

reconsider ni = (s . n) - (s . i) as Element of NAT by A10, INT_1:3, XREAL_1:48;

A13: H_{1}(s) = ni + 1
;

A14: ( (g . (s,(I \; (i += 1)))) . i <= (g . (s,(I \; (i += 1)))) . n implies (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . b = 1 ) by Th35;

A15: g . ((g . (s,(I \; (i += 1)))),(i leq n)) = g . (s,((I \; (i += 1)) \; (i leq n))) by AOFA_000:def 29;

S_{1}[g . (s,I)]
by A4, A9;

then S_{1}[g . (s,(I \; (i += 1)))]
by A4, A11;

hence S_{1}[g . (s,((I \; (i += 1)) \; (i leq n)))]
by A4, A15; :: thesis: ( ( S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] implies g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) ) & ( g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) implies S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] ) & H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s) )

A16: ( (g . (s,(I \; (i += 1)))) . i > (g . (s,(I \; (i += 1)))) . n implies (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . b = 0 ) by Th35;

(g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (g . (s,(I \; (i += 1)))) . i by A1, A3, Th35;

hence ( S_{2}[g . (s,((I \; (i += 1)) \; (i leq n)))] iff g . (s,((I \; (i += 1)) \; (i leq n))) in (Funcs (X,INT)) \ (b,0) )
by A1, A2, A16, A14, A15, Th2, Th35; :: thesis: H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s)

(g . (s,I)) . n = s . n by A4, A9;

then (g . (s,(I \; (i += 1)))) . n = s . n by A7, A11, Th28;

then (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . n = s . n by A1, A2, Th35;

then H_{1}(g . ((g . (s,(I \; (i += 1)))),(i leq n))) = ni
by A12;

hence H_{1}(g . (s,((I \; (i += 1)) \; (i leq n)))) < H_{1}(s)
by A15, A13, NAT_1:13; :: thesis: verum

end;assume that

A9: S

s in (Funcs (X,INT)) \ (b,0) and

A10: S

set q = g . (s,(I \; (i += 1)));

set s1 = g . (s,I);

set q1 = g . ((g . (s,(I \; (i += 1)))),(i leq n));

A11: g . (s,(I \; (i += 1))) = g . ((g . (s,I)),(i += 1)) by AOFA_000:def 29;

(g . (s,I)) . i = s . i by A4, A9;

then (g . (s,(I \; (i += 1)))) . i = (s . i) + 1 by A11, Th28;

then A12: (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (s . i) + 1 by A1, A3, Th35;

reconsider ni = (s . n) - (s . i) as Element of NAT by A10, INT_1:3, XREAL_1:48;

A13: H

A14: ( (g . (s,(I \; (i += 1)))) . i <= (g . (s,(I \; (i += 1)))) . n implies (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . b = 1 ) by Th35;

A15: g . ((g . (s,(I \; (i += 1)))),(i leq n)) = g . (s,((I \; (i += 1)) \; (i leq n))) by AOFA_000:def 29;

S

then S

hence S

A16: ( (g . (s,(I \; (i += 1)))) . i > (g . (s,(I \; (i += 1)))) . n implies (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . b = 0 ) by Th35;

(g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (g . (s,(I \; (i += 1)))) . i by A1, A3, Th35;

hence ( S

(g . (s,I)) . n = s . n by A4, A9;

then (g . (s,(I \; (i += 1)))) . n = s . n by A7, A11, Th28;

then (g . ((g . (s,(I \; (i += 1)))),(i leq n))) . n = s . n by A1, A2, Th35;

then H

hence H

A18: ( s . i <= s . n implies s1 . b = 1 ) by Th35;

s1 . i = s . i by A1, A3, Th35;

then A19: ( s1 in (Funcs (X,INT)) \ (b,0) iff S

g iteration_terminates_for (I \; (i += 1)) \; (i leq n),s1 from AOFA_000:sch 4(A6, A19, A8);

hence g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n)) ; :: thesis: verum