set S = Funcs (F2(),INT);
reconsider s1 = F6() . (F9(),(F7() := F10())) as Element of Funcs (F2(),INT) ;
set C = F8() leq F7();
reconsider s2 = F6() . (s1,(F8() leq F7())) as Element of Funcs (F2(),INT) ;
A6:
P1[s2]
by A2, A3;
defpred S1[ Element of Funcs (F2(),INT)] means ( P1[$1] & ( F10() . F9() >= F9() . F8() implies ($1 . F7()) + 1 >= F9() . F8() ) & $1 . F8() = F9() . F8() );
A7:
s1 . F7() = F10() . F9()
by Th26;
then A8:
S1[s1]
by A2, A5, Th26, XREAL_1:39;
A9:
s2 . F7() = F10() . F9()
by A5, A7, Th35;
defpred S2[ Element of Funcs (F2(),INT)] means $1 . F7() >= $1 . F8();
set T = (Funcs (F2(),INT)) \ (F3(),0);
A10:
F6() complies_with_while_wrt (Funcs (F2(),INT)) \ (F3(),0)
by AOFA_000:def 32;
set II = F4() \; (F7() += (- 1));
A11:
F6() . (F9(),F5()) = F6() . (s1,(while ((F8() leq F7()),(F4() \; (F7() += (- 1))))))
by A1, AOFA_000:def 29;
A12:
s1 . F8() = F9() . F8()
by A5, Th26;
then A13:
s2 . F8() = F9() . F8()
by A5, Th35;
per cases
( F10() . F9() >= F9() . F8() or F10() . F9() < F9() . F8() )
;
suppose A14:
F10()
. F9()
>= F9()
. F8()
;
( P1[F6() . (F9(),F5())] & ( F10() . F9() >= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) - 1 ) & ( F10() . F9() < F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() )deffunc H1(
Element of
Funcs (
F2(),
INT))
-> Element of
NAT =
In (
((($1 . F7()) + 1) - ($1 . F8())),
NAT);
defpred S3[
Element of
Funcs (
F2(),
INT)]
means (
P1[$1] &
S2[$1] );
A15:
for
s being
Element of
Funcs (
F2(),
INT) st
S1[
s] &
s in (Funcs (F2(),INT)) \ (
F3(),
0) &
S2[
s] holds
S1[
F6()
. (
s,
(F4() \; (F7() += (- 1))))]
proof
let s be
Element of
Funcs (
F2(),
INT);
( S1[s] & s in (Funcs (F2(),INT)) \ (F3(),0) & S2[s] implies S1[F6() . (s,(F4() \; (F7() += (- 1))))] )
assume that A16:
S1[
s]
and
s in (Funcs (F2(),INT)) \ (
F3(),
0)
and A17:
S2[
s]
;
S1[F6() . (s,(F4() \; (F7() += (- 1))))]
thus
P1[
F6()
. (
s,
(F4() \; (F7() += (- 1))))]
by A3, A16;
( ( F10() . F9() >= F9() . F8() implies ((F6() . (s,(F4() \; (F7() += (- 1))))) . F7()) + 1 >= F9() . F8() ) & (F6() . (s,(F4() \; (F7() += (- 1))))) . F8() = F9() . F8() )
reconsider s99 =
F6()
. (
s,
F4()) as
Element of
Funcs (
F2(),
INT) ;
reconsider s999 =
F6()
. (
s99,
(F7() += (- 1))) as
Element of
Funcs (
F2(),
INT) ;
A18:
s999 = F6()
. (
s,
(F4() \; (F7() += (- 1))))
by AOFA_000:def 29;
A19:
s999 . F7()
= (s99 . F7()) - 1
by Th28;
s99 . F8()
= s . F8()
by A4, A16;
hence
( (
F10()
. F9()
>= F9()
. F8() implies
((F6() . (s,(F4() \; (F7() += (- 1))))) . F7()) + 1
>= F9()
. F8() ) &
(F6() . (s,(F4() \; (F7() += (- 1))))) . F8()
= F9()
. F8() )
by A4, A5, A16, A17, A19, A18, Th28;
verum
end; A20:
for
s being
Element of
Funcs (
F2(),
INT) st
S3[
s] holds
( (
S3[
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] implies
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))
in (Funcs (F2(),INT)) \ (
F3(),
0) ) & (
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S3[
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] ) &
H1(
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7()))))
< H1(
s) )
proof
let s be
Element of
Funcs (
F2(),
INT);
( S3[s] implies ( ( S3[F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] implies F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7()))) in (Funcs (F2(),INT)) \ (F3(),0) ) & ( F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7()))) in (Funcs (F2(),INT)) \ (F3(),0) implies S3[F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] ) & H1(F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))) < H1(s) ) )
reconsider s9 =
F6()
. (
s,
F4()) as
Element of
Funcs (
F2(),
INT) ;
reconsider s99 =
F6()
. (
s9,
(F7() += (- 1))) as
Element of
Funcs (
F2(),
INT) ;
reconsider s999 =
F6()
. (
s99,
(F8() leq F7())) as
Element of
Funcs (
F2(),
INT) ;
A21:
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))
= F6()
. (
(F6() . (s,(F4() \; (F7() += (- 1))))),
(F8() leq F7()))
by AOFA_000:def 29;
A22:
s99 . F8()
= s9 . F8()
by A5, Th28;
A23:
(
s99 . F7()
>= s99 . F8() implies
s999 . F3()
= 1 )
by Th35;
A24:
(
s99 . F7()
< s99 . F8() implies
s999 . F3()
= 0 )
by Th35;
assume A25:
S3[
s]
;
( ( S3[F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] implies F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7()))) in (Funcs (F2(),INT)) \ (F3(),0) ) & ( F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7()))) in (Funcs (F2(),INT)) \ (F3(),0) implies S3[F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] ) & H1(F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))) < H1(s) )
then reconsider j =
(s . F7()) - (s . F8()) as
Element of
NAT by INT_1:5;
A26:
s999 . F7()
= s99 . F7()
by A5, Th35;
A27:
s99 = F6()
. (
s,
(F4() \; (F7() += (- 1))))
by AOFA_000:def 29;
then
P1[
s99]
by A3, A25;
hence
(
S3[
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))] iff
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7())))
in (Funcs (F2(),INT)) \ (
F3(),
0) )
by A3, A5, A21, A27, A26, A24, A23, Th2, Th35;
H1(F6() . (s,((F4() \; (F7() += (- 1))) \; (F8() leq F7())))) < H1(s)
A28:
s99 . F7()
= (s9 . F7()) - 1
by Th28;
A29:
s9 . F8()
= s . F8()
by A4, A25;
A30:
s9 . F7()
= s . F7()
by A4, A25;
s999 . F8()
= s99 . F8()
by A5, Th35;
then
H1(
s999)
= j
by A26, A30, A29, A28, A22;
then
H1(
s999)
+ 1
= H1(
s)
;
hence
H1(
F6()
. (
s,
((F4() \; (F7() += (- 1))) \; (F8() leq F7()))))
< H1(
s)
by A21, A27, NAT_1:13;
verum
end; A31:
for
s being
Element of
Funcs (
F2(),
INT) st
S1[
s] holds
(
S1[
F6()
. (
s,
(F8() leq F7()))] & (
F6()
. (
s,
(F8() leq F7()))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S2[
F6()
. (
s,
(F8() leq F7()))] ) & (
S2[
F6()
. (
s,
(F8() leq F7()))] implies
F6()
. (
s,
(F8() leq F7()))
in (Funcs (F2(),INT)) \ (
F3(),
0) ) )
proof
let s be
Element of
Funcs (
F2(),
INT);
( S1[s] implies ( S1[F6() . (s,(F8() leq F7()))] & ( F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F8() leq F7()))] ) & ( S2[F6() . (s,(F8() leq F7()))] implies F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) ) ) )
A32:
(
s . F7()
< s . F8() implies
(F6() . (s,(F8() leq F7()))) . F3()
= 0 )
by Th35;
assume A33:
S1[
s]
;
( S1[F6() . (s,(F8() leq F7()))] & ( F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F8() leq F7()))] ) & ( S2[F6() . (s,(F8() leq F7()))] implies F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) ) )
hence
P1[
F6()
. (
s,
(F8() leq F7()))]
by A3;
( ( F10() . F9() >= F9() . F8() implies ((F6() . (s,(F8() leq F7()))) . F7()) + 1 >= F9() . F8() ) & (F6() . (s,(F8() leq F7()))) . F8() = F9() . F8() & ( F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F8() leq F7()))] ) & ( S2[F6() . (s,(F8() leq F7()))] implies F6() . (s,(F8() leq F7())) in (Funcs (F2(),INT)) \ (F3(),0) ) )
A34:
(
s . F7()
>= s . F8() implies
(F6() . (s,(F8() leq F7()))) . F3()
= 1 )
by Th35;
(F6() . (s,(F8() leq F7()))) . F7()
= s . F7()
by A5, Th35;
hence
( (
F10()
. F9()
>= F9()
. F8() implies
((F6() . (s,(F8() leq F7()))) . F7()) + 1
>= F9()
. F8() ) &
(F6() . (s,(F8() leq F7()))) . F8()
= F9()
. F8() & (
F6()
. (
s,
(F8() leq F7()))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S2[
F6()
. (
s,
(F8() leq F7()))] ) & (
S2[
F6()
. (
s,
(F8() leq F7()))] implies
F6()
. (
s,
(F8() leq F7()))
in (Funcs (F2(),INT)) \ (
F3(),
0) ) )
by A5, A33, A32, A34, Th2, Th35;
verum
end;
s2 . F3()
= 1
by A7, A12, A14, Th35;
then A35:
(
F6()
. (
s1,
(F8() leq F7()))
in (Funcs (F2(),INT)) \ (
F3(),
0) iff
S3[
F6()
. (
s1,
(F8() leq F7()))] )
by A2, A3, A5, A12, A9, A14, Th35;
A36:
F6()
iteration_terminates_for (F4() \; (F7() += (- 1))) \; (F8() leq F7()),
F6()
. (
s1,
(F8() leq F7()))
from AOFA_000:sch 3(A35, A20);
A37:
(
S1[
F6()
. (
s1,
(while ((F8() leq F7()),(F4() \; (F7() += (- 1))))))] & not
S2[
F6()
. (
s1,
(while ((F8() leq F7()),(F4() \; (F7() += (- 1))))))] )
from AOFA_000:sch 5(A8, A36, A15, A31);
then
((F6() . (F9(),F5())) . F7()) + 1
<= ((F9() . F8()) + 1) - 1
by A11, INT_1:7;
then
((F6() . (F9(),F5())) . F7()) + 1
= F9()
. F8()
by A11, A14, A37, XXREAL_0:1;
hence
(
P1[
F6()
. (
F9(),
F5())] & (
F10()
. F9()
>= F9()
. F8() implies
(F6() . (F9(),F5())) . F7()
= (F9() . F8()) - 1 ) & (
F10()
. F9()
< F9()
. F8() implies
(F6() . (F9(),F5())) . F7()
= F10()
. F9() ) &
(F6() . (F9(),F5())) . F8()
= F9()
. F8() )
by A1, A14, A37, AOFA_000:def 29;
verum end; suppose A38:
F10()
. F9()
< F9()
. F8()
;
( P1[F6() . (F9(),F5())] & ( F10() . F9() >= F9() . F8() implies (F6() . (F9(),F5())) . F7() = (F9() . F8()) - 1 ) & ( F10() . F9() < F9() . F8() implies (F6() . (F9(),F5())) . F7() = F10() . F9() ) & (F6() . (F9(),F5())) . F8() = F9() . F8() )then
s2 . F3()
= 0
by A7, A12, Th35;
then
s2 nin (Funcs (F2(),INT)) \ (
F3(),
0)
by Th2;
hence
(
P1[
F6()
. (
F9(),
F5())] & (
F10()
. F9()
>= F9()
. F8() implies
(F6() . (F9(),F5())) . F7()
= (F9() . F8()) - 1 ) & (
F10()
. F9()
< F9()
. F8() implies
(F6() . (F9(),F5())) . F7()
= F10()
. F9() ) &
(F6() . (F9(),F5())) . F8()
= F9()
. F8() )
by A10, A9, A13, A11, A6, A38;
verum end; end;