set C = F7() leq F8();
set S = Funcs (F2(),INT);
reconsider s1 = F6() . (F9(),(F7() := F10())) as Element of Funcs (F2(),INT) ;
reconsider s2 = F6() . (s1,(F7() leq F8())) 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:
s2 . F7() = F10() . F9()
by A5, Th35;
defpred S2[ Element of Funcs (F2(),INT)] means $1 . F7() <= $1 . F8();
set T = (Funcs (F2(),INT)) \ (F3(),0);
A9:
F6() complies_with_while_wrt (Funcs (F2(),INT)) \ (F3(),0)
by AOFA_000:def 32;
set II = F4() \; (F7() += 1);
A10:
F6() . (F9(),F5()) = F6() . (s1,(while ((F7() leq F8()),(F4() \; (F7() += 1)))))
by A1, AOFA_000:def 29;
(F10() . F9()) - 1 < F10() . F9()
by XREAL_1:44;
then A11:
S1[s1]
by A2, A5, A7, Th26, XXREAL_0:2;
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 . F8()) + 1) - ($1 . F7())),
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 s9 =
F6()
. (
s,
F4()) as
Element of
Funcs (
F2(),
INT) ;
reconsider s99 =
F6()
. (
s9,
(F7() += 1)) as
Element of
Funcs (
F2(),
INT) ;
A18:
s99 = F6()
. (
s,
(F4() \; (F7() += 1)))
by AOFA_000:def 29;
A19:
s99 . F7()
= (s9 . F7()) + 1
by Th28;
s9 . 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)) \; (F7() leq F8())))] implies
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8())))
in (Funcs (F2(),INT)) \ (
F3(),
0) ) & (
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8())))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S3[
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8())))] ) &
H1(
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8()))))
< H1(
s) )
proof
let s be
Element of
Funcs (
F2(),
INT);
( S3[s] implies ( ( S3[F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))] implies F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8()))) in (Funcs (F2(),INT)) \ (F3(),0) ) & ( F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8()))) in (Funcs (F2(),INT)) \ (F3(),0) implies S3[F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))] ) & H1(F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))) < 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,
(F7() leq F8())) as
Element of
Funcs (
F2(),
INT) ;
A21:
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8())))
= F6()
. (
(F6() . (s,(F4() \; (F7() += 1)))),
(F7() leq F8()))
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)) \; (F7() leq F8())))] implies F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8()))) in (Funcs (F2(),INT)) \ (F3(),0) ) & ( F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8()))) in (Funcs (F2(),INT)) \ (F3(),0) implies S3[F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))] ) & H1(F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))) < H1(s) )
then reconsider j =
(s . F8()) - (s . F7()) 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)) \; (F7() leq F8())))] iff
F6()
. (
s,
((F4() \; (F7() += 1)) \; (F7() leq F8())))
in (Funcs (F2(),INT)) \ (
F3(),
0) )
by A3, A5, A21, A27, A26, A24, A23, Th2, Th35;
H1(F6() . (s,((F4() \; (F7() += 1)) \; (F7() leq F8())))) < 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)) \; (F7() leq F8()))))
< 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,
(F7() leq F8()))] & (
F6()
. (
s,
(F7() leq F8()))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S2[
F6()
. (
s,
(F7() leq F8()))] ) & (
S2[
F6()
. (
s,
(F7() leq F8()))] implies
F6()
. (
s,
(F7() leq F8()))
in (Funcs (F2(),INT)) \ (
F3(),
0) ) )
proof
let s be
Element of
Funcs (
F2(),
INT);
( S1[s] implies ( S1[F6() . (s,(F7() leq F8()))] & ( F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F7() leq F8()))] ) & ( S2[F6() . (s,(F7() leq F8()))] implies F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) ) ) )
A32:
(
s . F7()
> s . F8() implies
(F6() . (s,(F7() leq F8()))) . F3()
= 0 )
by Th35;
assume A33:
S1[
s]
;
( S1[F6() . (s,(F7() leq F8()))] & ( F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F7() leq F8()))] ) & ( S2[F6() . (s,(F7() leq F8()))] implies F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) ) )
hence
P1[
F6()
. (
s,
(F7() leq F8()))]
by A3;
( ( F10() . F9() <= F9() . F8() implies ((F6() . (s,(F7() leq F8()))) . F7()) - 1 <= F9() . F8() ) & (F6() . (s,(F7() leq F8()))) . F8() = F9() . F8() & ( F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) implies S2[F6() . (s,(F7() leq F8()))] ) & ( S2[F6() . (s,(F7() leq F8()))] implies F6() . (s,(F7() leq F8())) in (Funcs (F2(),INT)) \ (F3(),0) ) )
A34:
(
s . F7()
<= s . F8() implies
(F6() . (s,(F7() leq F8()))) . F3()
= 1 )
by Th35;
(F6() . (s,(F7() leq F8()))) . F7()
= s . F7()
by A5, Th35;
hence
( (
F10()
. F9()
<= F9()
. F8() implies
((F6() . (s,(F7() leq F8()))) . F7()) - 1
<= F9()
. F8() ) &
(F6() . (s,(F7() leq F8()))) . F8()
= F9()
. F8() & (
F6()
. (
s,
(F7() leq F8()))
in (Funcs (F2(),INT)) \ (
F3(),
0) implies
S2[
F6()
. (
s,
(F7() leq F8()))] ) & (
S2[
F6()
. (
s,
(F7() leq F8()))] implies
F6()
. (
s,
(F7() leq F8()))
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,
(F7() leq F8()))
in (Funcs (F2(),INT)) \ (
F3(),
0) iff
S3[
F6()
. (
s1,
(F7() leq F8()))] )
by A2, A3, A5, A12, A8, A14, Th35;
A36:
F6()
iteration_terminates_for (F4() \; (F7() += 1)) \; (F7() leq F8()),
F6()
. (
s1,
(F7() leq F8()))
from AOFA_000:sch 3(A35, A20);
A37:
(
S1[
F6()
. (
s1,
(while ((F7() leq F8()),(F4() \; (F7() += 1)))))] & not
S2[
F6()
. (
s1,
(while ((F7() leq F8()),(F4() \; (F7() += 1)))))] )
from AOFA_000:sch 5(A11, A36, A15, A31);
then
(F6() . (F9(),F5())) . F7()
>= (F9() . F8()) + 1
by A10, INT_1:7;
then
((F6() . (F9(),F5())) . F7()) - 1
>= ((F9() . F8()) + 1) - 1
by XREAL_1:13;
then
((F6() . (F9(),F5())) . F7()) - 1
= F9()
. F8()
by A10, 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 A9, A8, A13, A10, A6, A38;
verum end;