set R1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*>;
set R2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*>;
set R3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*>;
set R4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*>;
set R5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*>;
set R6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*>;
set R7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*>;
set R8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*>;
( 8 <= 256 - 8 & 8 <= 256 - 16 & 8 <= 256 - 24 ) ;
then reconsider R1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm1;
( 8 <= 256 - 32 & 8 <= 256 - 40 & 8 <= 256 - 48 & 8 <= 256 - 56 & 40 = 32 + 8 & 48 = 32 + 16 & 56 = 32 + 24 ) ;
then reconsider R2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 64 & 8 <= 256 - 72 & 8 <= 256 - 80 & 8 <= 256 - 88 & 72 = 64 + 8 & 80 = 64 + 16 & 88 = 64 + 24 ) ;
then reconsider R3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 96 & 8 <= 256 - 104 & 8 <= 256 - 112 & 8 <= 256 - 120 & 104 = 96 + 8 & 112 = 96 + 16 & 120 = 96 + 24 ) ;
then reconsider R4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 128 & 8 <= 256 - 136 & 8 <= 256 - 144 & 8 <= 256 - 152 & 136 = 128 + 8 & 144 = 128 + 16 & 152 = 128 + 24 ) ;
then reconsider R5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 160 & 8 <= 256 - 168 & 8 <= 256 - 176 & 8 <= 256 - 184 & 168 = 160 + 8 & 176 = 160 + 16 & 184 = 160 + 24 ) ;
then reconsider R6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 192 & 8 <= 256 - 200 & 8 <= 256 - 208 & 8 <= 256 - 216 & 200 = 192 + 8 & 208 = 192 + 16 & 216 = 192 + 24 ) ;
then reconsider R7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm2;
( 8 <= 256 - 224 & 8 <= 256 - 232 & 8 <= 256 - 240 & 8 = 256 - 248 & 232 = 224 + 8 & 240 = 224 + 16 & 248 = 224 + 24 & 8 = 256 - 248 ) ;
then reconsider R8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Lm3;
set T1 = <*R1,R2,R3,R4*>;
set T2 = <*R5,R6,R7,R8*>;
set T = <*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>;
A4: (<*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>) . 1 = <*R1,R2,R3,R4*> . 1 & ... & (<*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>) . 4 = <*R1,R2,R3,R4*> . 4 by FINSEQ_3:154;
A5: (<*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>) . (4 + 1) = <*R5,R6,R7,R8*> . 1 & ... & (<*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>) . (4 + 4) = <*R5,R6,R7,R8*> . 4 by FINSEQ_3:155;
( len (<*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*>) = 8 & <*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*> is FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) ) by CARD_1:def 7;
then reconsider T = <*R1,R2,R3,R4*> ^ <*R5,R6,R7,R8*> as Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by FINSEQ_2:92;
take T ; :: thesis:
thus ( T . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & T . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & T . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & T . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & T . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & T . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & T . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & T . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> ) by A4, A5, FINSEQ_4:76; :: thesis: