consider r being non empty FinSequence of F4() such that
A5:
r . 1 = F7() . (F5(),F2())
and
A6:
r . (len r) nin F6()
and
A7:
for i being Nat st 1 <= i & i < len r holds
( r . i in F6() & r . (i + 1) = F7() . ((r . i),(F3() \; F2())) )
by A2;
A8:
F7() . (F5(),(while (F2(),F3()))) = r . (len r)
by A5, A6, A7, Th86;
defpred S1[ Nat] means ( $1 + 1 in dom r implies ( P1[r . ($1 + 1)] & ( $1 + 1 < len r implies P2[r . ($1 + 1)] ) & ex q being Element of F4() st
( P1[q] & r . ($1 + 1) = F7() . (q,F2()) ) ) );
( 0 + 1 < len r implies r . (0 + 1) in F6() )
by A7;
then A9:
S1[ 0 ]
by A1, A4, A5;
A10:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A11:
S1[
n]
;
S1[n + 1]
assume A12:
(n + 1) + 1
in dom r
;
( P1[r . ((n + 1) + 1)] & ( (n + 1) + 1 < len r implies P2[r . ((n + 1) + 1)] ) & ex q being Element of F4() st
( P1[q] & r . ((n + 1) + 1) = F7() . (q,F2()) ) )
then A13:
(n + 1) + 1
<= len r
by FINSEQ_3:25;
A14:
(n + 1) + 1
>= 1
by NAT_1:11;
A15:
n + 1
>= 1
by NAT_1:11;
A16:
n + 1
< len r
by A13, NAT_1:13;
then A17:
n + 1
in dom r
by A15, FINSEQ_3:25;
A18:
r . (n + 1) in F6()
by A7, A15, A16;
A19:
r . ((n + 1) + 1) = F7()
. (
(r . (n + 1)),
(F3() \; F2()))
by A7, A15, A16;
reconsider q1 =
r . (n + 1),
q2 =
r . ((n + 1) + 1) as
Element of
F4()
by A12, A17, DTCONSTR:2;
reconsider q3 =
F7()
. (
q1,
F3()) as
Element of
F4() ;
A20:
q2 = F7()
. (
q3,
F2())
by A19, Def29;
A21:
P1[
q3]
by A3, A11, A15, A16, A18, FINSEQ_3:25;
hence
P1[
r . ((n + 1) + 1)]
by A4, A20;
( ( (n + 1) + 1 < len r implies P2[r . ((n + 1) + 1)] ) & ex q being Element of F4() st
( P1[q] & r . ((n + 1) + 1) = F7() . (q,F2()) ) )
hereby ex q being Element of F4() st
( P1[q] & r . ((n + 1) + 1) = F7() . (q,F2()) )
end;
take
q3
;
( P1[q3] & r . ((n + 1) + 1) = F7() . (q3,F2()) )
thus
(
P1[
q3] &
r . ((n + 1) + 1) = F7()
. (
q3,
F2()) )
by A3, A11, A15, A16, A18, A19, Def29, FINSEQ_3:25;
verum
end;
A22:
for n being Nat holds S1[n]
from NAT_1:sch 2(A9, A10);
A23:
len r >= 0 + 1
by NAT_1:13;
then consider j being Nat such that
A24:
len r = 1 + j
by NAT_1:10;
A25:
j + 1 in dom r
by A23, A24, FINSEQ_3:25;
hence
P1[F7() . (F5(),(while (F2(),F3())))]
by A8, A22, A24; P2[F7() . (F5(),(while (F2(),F3())))]
ex q being Element of F4() st
( P1[q] & r . (j + 1) = F7() . (q,F2()) )
by A22, A25;
hence
P2[F7() . (F5(),(while (F2(),F3())))]
by A4, A6, A8, A24; verum