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 D0:
( d . b = 0 & d . n = 1 & 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) )
D1:
( b <> i & b <> n & i <> n )
by D0;
assume that
00:
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
A0:
s in P
; :: thesis: g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . s,(i leq n)
set h = g;
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
set C = i leq n;
set J = i += 1;
reconsider s1 = g . s,(i leq n) as Element of Funcs X,INT ;
defpred S1[ Element of Funcs X,INT ] means $1 in P;
defpred S2[ Element of Funcs X,INT ] means $1 . i <= $1 . n;
deffunc H1( Element of Funcs X,INT ) -> Element of NAT = In ((($1 . n) + 1) - ($1 . i)),NAT ;
AA:
S1[s1]
by A0, 00;
( ( s . i > s . n implies s1 . b = 0 ) & ( s . i > s . n or s . i <= s . n ) & s1 . i = s . i & s1 . n = s . n & ( s . i <= s . n implies s1 . b = 1 ) )
by D0, Th114;
then AB:
( s1 in (Funcs X,INT ) \ b,0 iff S2[s1] )
by LemTS;
C:
for s being Element of Funcs X,INT st S1[s] & s in (Funcs X,INT ) \ b,0 & S2[s] holds
( S1[g . s,((I \; (i += 1)) \; (i leq n))] & ( S2[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 S2[g . s,((I \; (i += 1)) \; (i leq n))] ) & H1(g . s,((I \; (i += 1)) \; (i leq n))) < H1(s) )
proof
let s be
Element of
Funcs X,
INT ;
:: thesis: ( S1[s] & s in (Funcs X,INT ) \ b,0 & S2[s] implies ( S1[g . s,((I \; (i += 1)) \; (i leq n))] & ( S2[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 S2[g . s,((I \; (i += 1)) \; (i leq n))] ) & H1(g . s,((I \; (i += 1)) \; (i leq n))) < H1(s) ) )
assume 01:
(
S1[
s] &
s in (Funcs X,INT ) \ b,
0 &
S2[
s] )
;
:: thesis: ( S1[g . s,((I \; (i += 1)) \; (i leq n))] & ( S2[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 S2[g . s,((I \; (i += 1)) \; (i leq n))] ) & H1(g . s,((I \; (i += 1)) \; (i leq n))) < H1(s) )
then reconsider ni =
(s . n) - (s . i) as
Element of
NAT by INT_1:16, XREAL_1:50;
set s1 =
g . s,
I;
set q =
g . s,
(I \; (i += 1));
set q1 =
g . (g . s,(I \; (i += 1))),
(i leq n);
03:
( (
(g . s,(I \; (i += 1))) . i > (g . s,(I \; (i += 1))) . n implies
(g . (g . s,(I \; (i += 1))),(i leq n)) . b = 0 ) & (
(g . s,(I \; (i += 1))) . i > (g . s,(I \; (i += 1))) . n or
(g . s,(I \; (i += 1))) . i <= (g . s,(I \; (i += 1))) . n ) &
(g . (g . s,(I \; (i += 1))),(i leq n)) . i = (g . s,(I \; (i += 1))) . i &
(g . (g . s,(I \; (i += 1))),(i leq n)) . n = (g . s,(I \; (i += 1))) . n & (
(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 D0, Th114;
02:
(
g . s,
(I \; (i += 1)) = g . (g . s,I),
(i += 1) &
g . (g . s,(I \; (i += 1))),
(i leq n) = g . s,
((I \; (i += 1)) \; (i leq n)) )
by AOFA_000:def 29;
S1[
g . s,
I]
by 01, 00;
then
S1[
g . s,
(I \; (i += 1))]
by 00, 02;
hence
S1[
g . s,
((I \; (i += 1)) \; (i leq n))]
by 00, 02;
:: thesis: ( ( S2[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 S2[g . s,((I \; (i += 1)) \; (i leq n))] ) & H1(g . s,((I \; (i += 1)) \; (i leq n))) < H1(s) )
thus
(
S2[
g . s,
((I \; (i += 1)) \; (i leq n))] iff
g . s,
((I \; (i += 1)) \; (i leq n)) in (Funcs X,INT ) \ b,
0 )
by 02, 03, LemTS;
:: thesis: H1(g . s,((I \; (i += 1)) \; (i leq n))) < H1(s)
(
(g . s,I) . i = s . i &
(g . s,I) . n = s . n )
by 01, 00;
then
(
(g . s,(I \; (i += 1))) . i = (s . i) + 1 &
(g . s,(I \; (i += 1))) . n = s . n )
by 02, D1, Th012;
then
(
(g . (g . s,(I \; (i += 1))),(i leq n)) . i = (s . i) + 1 &
(g . (g . s,(I \; (i += 1))),(i leq n)) . n = s . n )
by D0, Th114;
then
(
H1(
g . (g . s,(I \; (i += 1))),
(i leq n))
= ni &
H1(
s)
= ni + 1 )
by FUNCT_7:def 1;
hence
H1(
g . s,
((I \; (i += 1)) \; (i leq n)))
< H1(
s)
by 02, NAT_1:13;
:: thesis: verum
end;
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),s1
from AOFA_000:sch 4(AA, AB, C);
hence
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . s,(i leq n)
; :: thesis: verum