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₁[ Element of Funcs X,INT ] means $1 in P;
reconsider s1 = g . s,(i leq n) as Element of Funcs X,INT ;
A6: S₁[s1] by A4, A5;
deffunc H₁( Element of Funcs X,INT ) -> Element of NAT = In ((($1 . n) + 1) - ($1 . i)),NAT ;
defpred S₂[ 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₁[s] & s in (Funcs X,INT ) \ b,0 & S₂[s] holds
( S₁[g . s,((I \; (i += 1)) \; (i leq n))] & ( S₂[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₂[g . s,((I \; (i += 1)) \; (i leq n))] ) & H₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(s) )

proof

let s be Element of Funcs X,INT ; :: thesis: ( S₁[s] & s in (Funcs X,INT ) \ b,0 & S₂[s] implies ( S₁[g . s,((I \; (i += 1)) \; (i leq n))] & ( S₂[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₂[g . s,((I \; (i += 1)) \; (i leq n))] ) & H₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(s) ) )
assume that
A9: S₁[s] and
s in (Funcs X,INT ) \ b,0 and
A10: S₂[s] ; :: thesis: ( S₁[g . s,((I \; (i += 1)) \; (i leq n))] & ( S₂[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₂[g . s,((I \; (i += 1)) \; (i leq n))] ) & H₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(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:16, XREAL_1:50;
A13: H₁(s) = ni + 1 by FUNCT_7:def 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₁[g . s,I] by A4, A9;
then S₁[g . s,(I \; (i += 1))] by A4, A11;
hence S₁[g . s,((I \; (i += 1)) \; (i leq n))] by A4, A15; :: thesis: ( ( S₂[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₂[g . s,((I \; (i += 1)) \; (i leq n))] ) & H₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(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 \; (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₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(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₁(g . (g . s,(I \; (i += 1))),(i leq n)) = ni by A12, FUNCT_7:def 1;
hence H₁(g . s,((I \; (i += 1)) \; (i leq n))) < H₁(s) by A15, A13, NAT_1:13; :: thesis: verum

end;

A17: ( s . i > s . n implies s1 . b = 0 ) by Th35;
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₂[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