deffunc H1( Nat, Subset of F1()) -> Subset of F1() = F4($2);
consider f being sequence of (bool F1()) such that
A4:
f . 0 = F3()
and
A5:
for n being Nat holds f . (n + 1) = H1(n,f . n)
from NAT_1:sch 12();
defpred S1[ Nat] means f . $1 c= F2();
A6:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A7:
S1[
n]
;
S1[n + 1]
f . (n + 1) = F4(
(f . n))
by A5;
hence
S1[
n + 1]
by A3, A7;
verum end;
A8:
S1[ 0 ]
by A2, A4;
A9:
for n being Nat holds S1[n]
from NAT_1:sch 2(A8, A6);
A10:
for i being Nat holds f . i c= f . (i + 1)
A11:
dom f = NAT
by FUNCT_2:def 1;
A12:
rng f is c=-linear
A17:
rng f c= bool F2()
rng f <> {}
by A4, A11, FUNCT_1:def 3;
then consider m being set such that
A18:
m in rng f
and
A19:
for C being set st C in rng f holds
C c= m
by A1, A17, A12, FINSET_1:12;
deffunc H2( Nat) -> Element of bool F1() = f . |.($1 - 1).|;
defpred S2[ set ] means ( $1 in NAT & f . $1 = m );
m in f .: NAT
by A18, RELSET_1:22;
then
ex k being Element of NAT st S2[k]
by FUNCT_2:65;
then A20:
ex k being Nat st S2[k]
;
consider k being Nat such that
A21:
S2[k]
and
A22:
for n being Nat st S2[n] holds
k <= n
from NAT_1:sch 5(A20);
consider z being FinSequence of bool F1() such that
A23:
len z = k + 1
and
A24:
for j being Nat st j in dom z holds
z . j = H2(j)
from FINSEQ_2:sch 1();
A25:
0 + 1 <= len z
by A23, NAT_1:13;
then A26:
1 in Seg (k + 1)
by A23, FINSEQ_1:1;
take
z
; ( len z > 0 & z /. 1 = F3() & ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus
0 < len z
by A23; ( z /. 1 = F3() & ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
A27:
dom z = Seg (k + 1)
by A23, FINSEQ_1:def 3;
thus z /. 1 =
z . 1
by A25, FINSEQ_4:15
.=
f . |.(1 - 1).|
by A24, A27, A26
.=
F3()
by A4, ABSVALUE:2
; ( ( for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus A28:
for i being Nat st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i))
( F4((z /. (len z))) = z /. (len z) & ( for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )proof
let i be
Nat;
( i > 0 & i < len z implies z /. (i + 1) = F4((z /. i)) )
assume that A29:
i > 0
and A30:
i < len z
;
z /. (i + 1) = F4((z /. i))
A31:
(
0 + 1
< i + 1 &
i + 1
<= k + 1 )
by A23, A29, A30, NAT_1:13, XREAL_1:6;
then A32:
i + 1
in Seg (k + 1)
by FINSEQ_1:1;
A33:
0 + 1
<= i
by A29, NAT_1:13;
then
i in Seg (k + 1)
by A23, A30, FINSEQ_1:1;
then A34:
(
z . i = f . |.(i - 1).| &
i in dom z )
by A24, A27;
1
- 1
<= i - 1
by A33, XREAL_1:9;
then A35:
0 <= (i - 1) * 1
;
thus z /. (i + 1) =
z . (i + 1)
by A23, A31, FINSEQ_4:15
.=
f . |.((i + 1) - 1).|
by A24, A27, A32
.=
f . |.((i - 1) + 1).|
.=
f . (|.(i - 1).| + |.1.|)
by A35, ABSVALUE:11
.=
f . (|.(i - 1).| + 1)
by ABSVALUE:def 1
.=
F4(
(f . |.(i - 1).|))
by A5
.=
F4(
(z /. i))
by A34, PARTFUN1:def 6
;
verum
end;
thus
F4((z /. (len z))) = z /. (len z)
for i, j being Nat st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j )
let i, j be Nat; ( i > 0 & i < j & j <= len z implies ( z /. i c= F2() & z /. i c< z /. j ) )
assume that
A40:
0 < i
and
A41:
i < j
and
A42:
j <= len z
; ( z /. i c= F2() & z /. i c< z /. j )
A43:
0 + 1 <= i
by A40, NAT_1:13;
then reconsider l = i - 1 as Element of NAT by INT_1:5;
A44:
i <= len z
by A41, A42, XXREAL_0:2;
then A45:
i in Seg (k + 1)
by A23, A43, FINSEQ_1:1;
A46: z /. i =
z . i
by A43, A44, FINSEQ_4:15
.=
f . |.(i - 1).|
by A24, A27, A45
.=
f . l
by ABSVALUE:def 1
;
hence
z /. i c= F2()
by A9; z /. i c< z /. j
A47:
for i being Nat st 1 <= i & i < len z holds
z /. i c= z /. (i + 1)
proof
let i be
Nat;
( 1 <= i & i < len z implies z /. i c= z /. (i + 1) )
assume that A48:
1
<= i
and A49:
i < len z
;
z /. i c= z /. (i + 1)
A50:
i in Seg (k + 1)
by A23, A48, A49, FINSEQ_1:1;
A51:
1
- 1
<= i - 1
by A48, XREAL_1:9;
then A52:
i - 1 is
Element of
NAT
by INT_1:3;
A53:
( 1
<= i + 1 &
i + 1
<= len z )
by A48, A49, NAT_1:13;
then A54:
i + 1
in Seg (k + 1)
by A23, FINSEQ_1:1;
A55:
z /. (i + 1) =
z . (i + 1)
by A53, FINSEQ_4:15
.=
f . |.((i + 1) - 1).|
by A24, A27, A54
.=
f . ((i - 1) + 1)
by ABSVALUE:def 1
;
z /. i =
z . i
by A48, A49, FINSEQ_4:15
.=
f . |.(i - 1).|
by A24, A27, A50
.=
f . (i - 1)
by A51, ABSVALUE:def 1
;
hence
z /. i c= z /. (i + 1)
by A10, A55, A52;
verum
end;
hence
z /. i c= z /. j
by A41, A42, A43, Th1; XBOOLE_0:def 8 not z /. i = z /. j
defpred S3[ Nat] means ( i + $1 <= len z implies z /. i = z /. (i + $1) );
A56:
( i <= i + 1 & i + 1 <= j )
by A41, NAT_1:13;
k + 1 in Seg (k + 1)
by FINSEQ_1:4;
then A57:
k + 1 in dom z
by A23, FINSEQ_1:def 3;
A58:
i < len z
by A41, A42, XXREAL_0:2;
assume
z /. i = z /. j
; contradiction
then A59: z /. i =
z /. (i + 1)
by A42, A43, A47, A56, Th2
.=
F4((z /. i))
by A28, A40, A58
;
A60:
now for n being Nat st S3[n] holds
S3[n + 1]let n be
Nat;
( S3[n] implies S3[n + 1] )assume A61:
S3[
n]
;
S3[n + 1]thus
S3[
n + 1]
verum end;
consider n0 being Nat such that
A62:
i + n0 = len z
by A41, A42, NAT_1:10, XXREAL_0:2;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
A63:
i + n0 = len z
by A62;
A64:
S3[ 0 ]
;
for n being Nat holds S3[n]
from NAT_1:sch 2(A64, A60);
then f . l =
z /. (k + 1)
by A23, A46, A63
.=
z . (k + 1)
by A57, PARTFUN1:def 6
.=
f . |.((k + 1) - 1).|
by A24, A27, FINSEQ_1:4
.=
m
by A21, ABSVALUE:def 1
;
then
k <= l
by A22;
then
len z <= l + 1
by A23, XREAL_1:6;
hence
contradiction
by A41, A42, XXREAL_0:2; verum