let A be Euclidean preIfWhileAlgebra; 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 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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
let X be 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 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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
let s be 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 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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
let b be Element of X; for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) 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); 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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
let I be 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) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
let i, n be Variable of g; ( ex d being Function st
( d . b = 0 & d . n = 1 & d . i = 2 ) & ( for s being Element of Funcs (X,INT) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i ) ) 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
; ( ex s being Element of Funcs (X,INT) st
( (g . (s,I)) . n = s . n implies not (g . (s,I)) . i = s . i ) 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 A4:
for s being Element of Funcs (X,INT) holds
( (g . (s,I)) . n = s . n & (g . (s,I)) . i = s . i )
; g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
deffunc H1( Element of Funcs (X,INT)) -> Element of NAT = In (((($1 . n) + 1) - ($1 . i)),NAT);
defpred S1[ Element of Funcs (X,INT)] means $1 . i <= $1 . n;
set T = (Funcs (X,INT)) \ (b,0);
A5:
i <> n
by A2, A3;
A6:
for s being Element of Funcs (X,INT) st S1[s] holds
( ( S1[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 S1[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);
( S1[s] implies ( ( S1[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 S1[g . (s,((I \; (i += 1)) \; (i leq n)))] ) & H1(g . (s,((I \; (i += 1)) \; (i leq n)))) < H1(s) ) )
set s1 =
g . (
s,
I);
set q =
g . (
s,
(I \; (i += 1)));
set q1 =
g . (
(g . (s,(I \; (i += 1)))),
(i leq n));
A7:
g . (
s,
(I \; (i += 1)))
= g . (
(g . (s,I)),
(i += 1))
by AOFA_000:def 29;
(g . (s,I)) . i = s . i
by A4;
then
(g . (s,(I \; (i += 1)))) . i = (s . i) + 1
by A7, Th28;
then A8:
(g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (s . i) + 1
by A1, A3, Th35;
A9:
(
(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;
assume
S1[
s]
;
( ( S1[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 S1[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:3, XREAL_1:48;
A10:
g . (
(g . (s,(I \; (i += 1)))),
(i leq n))
= g . (
s,
((I \; (i += 1)) \; (i leq n)))
by AOFA_000:def 29;
A11:
(
(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;
(g . ((g . (s,(I \; (i += 1)))),(i leq n))) . i = (g . (s,(I \; (i += 1)))) . i
by A1, A3, Th35;
hence
(
S1[
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, A9, A11, A10, Th2, Th35;
H1(g . (s,((I \; (i += 1)) \; (i leq n)))) < H1(s)
A12:
H1(
s)
= ni + 1
;
(g . (s,I)) . n = s . n
by A4;
then
(g . (s,(I \; (i += 1)))) . n = s . n
by A5, A7, Th28;
then
(g . ((g . (s,(I \; (i += 1)))),(i leq n))) . n = s . n
by A1, A2, Th35;
then
H1(
g . (
(g . (s,(I \; (i += 1)))),
(i leq n)))
= ni
by A8;
hence
H1(
g . (
s,
((I \; (i += 1)) \; (i leq n))))
< H1(
s)
by A10, A12, NAT_1:13;
verum
end;
reconsider s1 = g . (s,(i leq n)) as Element of Funcs (X,INT) ;
A13:
( s . i > s . n implies s1 . b = 0 )
by Th35;
A14:
( s . i <= s . n implies s1 . b = 1 )
by Th35;
s1 . i = s . i
by A1, A3, Th35;
then A15:
( s1 in (Funcs (X,INT)) \ (b,0) iff S1[s1] )
by A1, A2, A13, A14, Th2, Th35;
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),s1
from AOFA_000:sch 3(A15, A6);
hence
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),g . (s,(i leq n))
; verum