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;
defpred S1[ Nat] means ( (len r) - $1 in dom r implies P1[r . ((len r) - $1)] );
defpred S2[ Nat] means ( $1 + 1 in dom r implies ex q being Element of F4() st r . ($1 + 1) = F7() . (q,F2()) );
A8:
S2[ 0 ]
by A5;
A9:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume
S2[
n]
;
S2[n + 1]
assume
(n + 1) + 1
in dom r
;
ex q being Element of F4() st r . ((n + 1) + 1) = F7() . (q,F2())
then A10:
(n + 1) + 1
<= len r
by FINSEQ_3:25;
A11:
n + 1
>= 1
by NAT_1:11;
A12:
n + 1
< len r
by A10, NAT_1:13;
then A13:
r . (n + 1) in F6()
by A7, A11;
A14:
r . ((n + 1) + 1) = F7()
. (
(r . (n + 1)),
(F3() \; F2()))
by A7, A11, A12;
reconsider q1 =
r . (n + 1) as
Element of
F4()
by A13;
reconsider q3 =
F7()
. (
q1,
F3()) as
Element of
F4() ;
take
q3
;
r . ((n + 1) + 1) = F7() . (q3,F2())
thus
r . ((n + 1) + 1) = F7()
. (
q3,
F2())
by A14, Def29;
verum
end;
A15:
S1[ 0 ]
by A1, A5, A6, A7, Th86;
A16:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A17:
S1[
n]
;
S1[n + 1]
assume A18:
(len r) - (n + 1) in dom r
;
P1[r . ((len r) - (n + 1))]
then reconsider j =
(len r) - (n + 1) as
Element of
NAT ;
A19:
j >= 1
by A18, FINSEQ_3:25;
n + 1
>= 0 + 1
by NAT_1:13;
then
j <= (len r) - 1
by XREAL_1:10;
then A20:
j + 1
<= ((len r) - 1) + 1
by XREAL_1:6;
A21:
1
<= 1
+ j
by NAT_1:11;
A22:
j < len r
by A20, NAT_1:13;
A23:
j + 1
in dom r
by A20, A21, FINSEQ_3:25;
A24:
r . j in F6()
by A7, A19, A22;
A25:
r . (j + 1) = F7()
. (
(r . j),
(F3() \; F2()))
by A7, A19, A22;
reconsider q1 =
r . j,
q2 =
r . (j + 1) as
Element of
F4()
by A23, A24, DTCONSTR:2;
reconsider q9 =
F7()
. (
q1,
F3()) as
Element of
F4() ;
consider j9 being
Nat such that A26:
j = 1
+ j9
by A19, NAT_1:10;
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A8, A9);
then consider qq being
Element of
F4()
such that A27:
r . (j9 + 1) = F7()
. (
qq,
F2())
by A18, A26;
q2 = F7()
. (
q9,
F2())
by A25, Def29;
then
P1[
F7()
. (
(F7() . (qq,F2())),
F3())]
by A4, A17, A20, A21, A26, A27, FINSEQ_3:25;
hence
P1[
r . ((len r) - (n + 1))]
by A3, A7, A19, A22, A26, A27;
verum
end;
A28:
for n being Nat holds S1[n]
from NAT_1:sch 2(A15, A16);
A29:
len r >= 0 + 1
by NAT_1:13;
then consider j being Nat such that
A30:
len r = 1 + j
by NAT_1:10;
(len r) - j in dom r
by A29, A30, FINSEQ_3:25;
hence
P1[F5()]
by A4, A5, A28, A30; verum