defpred S1[ Element of 128 -tuples_on BOOLEAN, set ] means ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( $2 = z & ( for i, j being Nat st i in Seg 4 & j in Seg 4 holds
(z . i) . j = mid ($1,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) );
A1: for x being Element of 128 -tuples_on BOOLEAN ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z]
proof
let x be Element of 128 -tuples_on BOOLEAN; :: thesis: ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z]
x in 128 -tuples_on BOOLEAN ;
then A01: ex s being Element of BOOLEAN * st
( x = s & len s = 128 ) ;
defpred S2[ Nat, set ] means ex zi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( $2 = zi & ( for j being Nat st j in Seg 4 holds
zi . j = mid (x,((1 + (($1 -' 1) * 8)) + ((j -' 1) * 32)),(((1 + (($1 -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) );
Q1: for k being Nat st k in Seg 4 holds
ex x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg 4 implies ex x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,x] )
assume k in Seg 4 ; :: thesis: ex x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,x]
then Q110: ( 1 <= k & k <= 4 ) by FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then k -' 1 = k - 1 by XREAL_0:def 2;
then k -' 1 <= 4 - 1 by Q110, XREAL_1:9;
then Q112: (k -' 1) * 8 <= 3 * 8 by XREAL_1:64;
defpred S3[ Nat, set ] means $2 = mid (x,((1 + ((k -' 1) * 8)) + (($1 -' 1) * 32)),(((1 + ((k -' 1) * 8)) + (($1 -' 1) * 32)) + 7));
Q12: for j being Nat st j in Seg 4 holds
ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi]
proof
let j be Nat; :: thesis: ( j in Seg 4 implies ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi] )
assume j in Seg 4 ; :: thesis: ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi]
then Q130: ( 1 <= j & j <= 4 ) by FINSEQ_1:1;
then 1 - 1 <= j - 1 by XREAL_1:9;
then j -' 1 = j - 1 by XREAL_0:def 2;
then j -' 1 <= 4 - 1 by Q130, XREAL_1:9;
then Q133: (j -' 1) * 32 <= 3 * 32 by XREAL_1:64;
((k -' 1) * 8) + ((j -' 1) * 32) <= 24 + 96 by Q133, Q112, XREAL_1:7;
then Q134: 1 + (((k -' 1) * 8) + ((j -' 1) * 32)) <= 1 + 120 by XREAL_1:7;
Q136: ((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7 <= 121 + 7 by Q134, XREAL_1:7;
1 + 0 <= 1 + (((k -' 1) * 8) + ((j -' 1) * 32)) by XREAL_1:7;
then Q14: ( 1 <= (1 + ((k -' 1) * 8)) + ((j -' 1) * 32) & (1 + ((k -' 1) * 8)) + ((j -' 1) * 32) <= len x ) by Q134, XXREAL_0:2, A01;
Q150: 1 + 0 <= ((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7 by XREAL_1:7;
reconsider mmd = mid (x,((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7)) as Element of BOOLEAN * by FINSEQ_1:def 11;
((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 0 <= ((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7 by XREAL_1:6;
then len (mid (x,((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7))) = ((((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7) -' ((1 + ((k -' 1) * 8)) + ((j -' 1) * 32))) + 1 by FINSEQ_6:118, Q14, Q136, A01, Q150
.= 7 + 1 by NAT_D:34
.= 8 ;
then mmd in 8 -tuples_on BOOLEAN ;
then reconsider xi = mid (x,((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7)) as Element of 8 -tuples_on BOOLEAN ;
xi = mid (x,((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ;
hence ex xi being Element of 8 -tuples_on BOOLEAN st S3[j,xi] ; :: thesis: verum
end;
consider zi being FinSequence of 8 -tuples_on BOOLEAN such that
Q13: ( dom zi = Seg 4 & ( for i being Nat st i in Seg 4 holds
S3[i,zi . i] ) ) from FINSEQ_1:sch 5(Q12);
 Q14: len zi = 4 by Q13, FINSEQ_1:def 3;
reconsider zi = zi as Element of (8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
zi in 4 -tuples_on (8 -tuples_on BOOLEAN) by Q14;
then reconsider zi = zi as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
for j being Nat st j in Seg 4 holds
zi . j = mid (x,((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((k -' 1) * 8)) + ((j -' 1) * 32)) + 7)) by Q13;
hence ex x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,x] ; :: thesis: verum
end;
consider z being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
Q2: ( dom z = Seg 4 & ( for i being Nat st i in Seg 4 holds
S2[i,z . i] ) ) from FINSEQ_1:sch 5(Q1);
 Q3: len z = 4 by Q2, FINSEQ_1:def 3;
reconsider z = z as Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
z in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by Q3;
then reconsider z = z as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
(z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
proof
let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) )
assume P11: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
then consider zi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
P12: ( z . i = zi & ( for j being Nat st j in Seg 4 holds
zi . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) ) by Q2;
thus (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) by P11, P12; :: thesis: verum
end;
hence ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z] ; :: thesis: verum
end;
consider I being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) such that
A2: for x being Element of 128 -tuples_on BOOLEAN holds S1[x,I . x] from FUNCT_2:sch 3(A1);
now :: thesis: for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((I . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
let input be Element of 128 -tuples_on BOOLEAN; :: thesis: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((I . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( I . input = z & ( for i, j being Nat st i in Seg 4 & j in Seg 4 holds
(z . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) ) by A2;
hence for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((I . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ; :: thesis: verum
end;
hence ex b1 being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st
for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ; :: thesis: verum