let r be Element of 48 -tuples_on BOOLEAN; ex s1, s2, s3, s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( s1 = (DES-DIV8 r) . 1 & s2 = (DES-DIV8 r) . 2 & s3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((s1 ^ s2) ^ s3) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )
r is Element of Funcs ((Seg 48),BOOLEAN)
by FINSEQ_2:93;
then
dom r = Seg 48
by FUNCT_2:def 1;
then A1:
len r = 48
by FINSEQ_1:def 3;
1 in Seg 8
;
then reconsider SEG8E1 = 1 as Element of Seg 8 ;
2 in Seg 8
;
then reconsider SEG8E2 = 2 as Element of Seg 8 ;
3 in Seg 8
;
then reconsider SEG8E3 = 3 as Element of Seg 8 ;
4 in Seg 8
;
then reconsider SEG8E4 = 4 as Element of Seg 8 ;
5 in Seg 8
;
then reconsider SEG8E5 = 5 as Element of Seg 8 ;
6 in Seg 8
;
then reconsider SEG8E6 = 6 as Element of Seg 8 ;
7 in Seg 8
;
then reconsider SEG8E7 = 7 as Element of Seg 8 ;
8 in Seg 8
;
then reconsider SEG8E8 = 8 as Element of Seg 8 ;
set s1 = (DES-DIV8 r) . SEG8E1;
set s2 = (DES-DIV8 r) . SEG8E2;
set s3 = (DES-DIV8 r) . SEG8E3;
set s4 = (DES-DIV8 r) . SEG8E4;
set s5 = (DES-DIV8 r) . SEG8E5;
set s6 = (DES-DIV8 r) . SEG8E6;
set s7 = (DES-DIV8 r) . SEG8E7;
set s8 = (DES-DIV8 r) . SEG8E8;
take
(DES-DIV8 r) . SEG8E1
; ex s2, s3, s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & s2 = (DES-DIV8 r) . 2 & s3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ s2) ^ s3) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E2
; ex s3, s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & s3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ s3) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E3
; ex s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E4
; ex s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ s5) ^ s6) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E5
; ex s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & (DES-DIV8 r) . SEG8E5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ s6) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E6
; ex s7, s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & (DES-DIV8 r) . SEG8E5 = (DES-DIV8 r) . 5 & (DES-DIV8 r) . SEG8E6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ s7) ^ s8 )
take
(DES-DIV8 r) . SEG8E7
; ex s8 being Element of 6 -tuples_on BOOLEAN st
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & (DES-DIV8 r) . SEG8E5 = (DES-DIV8 r) . 5 & (DES-DIV8 r) . SEG8E6 = (DES-DIV8 r) . 6 & (DES-DIV8 r) . SEG8E7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7)) ^ s8 )
take
(DES-DIV8 r) . SEG8E8
; ( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & (DES-DIV8 r) . SEG8E5 = (DES-DIV8 r) . 5 & (DES-DIV8 r) . SEG8E6 = (DES-DIV8 r) . 6 & (DES-DIV8 r) . SEG8E7 = (DES-DIV8 r) . 7 & (DES-DIV8 r) . SEG8E8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7)) ^ ((DES-DIV8 r) . SEG8E8) )
r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7)) ^ ((DES-DIV8 r) . SEG8E8)
proof
A2:
(
(DES-DIV8 r) . SEG8E1 = Op-Left (
r,6) &
(DES-DIV8 r) . SEG8E2 = Op-Left (
(Op-Right (r,6)),6) &
(DES-DIV8 r) . SEG8E3 = Op-Left (
(Op-Right (r,12)),6) &
(DES-DIV8 r) . SEG8E4 = Op-Left (
(Op-Right (r,18)),6) &
(DES-DIV8 r) . SEG8E5 = Op-Left (
(Op-Right (r,24)),6) &
(DES-DIV8 r) . SEG8E6 = Op-Left (
(Op-Right (r,30)),6) &
(DES-DIV8 r) . SEG8E7 = Op-Left (
(Op-Right (r,36)),6) &
(DES-DIV8 r) . SEG8E8 = Op-Right (
r,42) )
by Def20;
((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2) = r | 12
by Th18, A1, A2;
then
(((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3) = r | 18
by Th18, A1, A2;
then
((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4) = r | 24
by Th18, A1, A2;
then
(((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5) = r | 30
by Th18, A1, A2;
then
((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6) = r | 36
by Th18, A1, A2;
then
(((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7) = r | 42
by Th18, A1, A2;
hence
r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7)) ^ ((DES-DIV8 r) . SEG8E8)
by A2, RFINSEQ:8;
verum
end;
hence
( (DES-DIV8 r) . SEG8E1 = (DES-DIV8 r) . 1 & (DES-DIV8 r) . SEG8E2 = (DES-DIV8 r) . 2 & (DES-DIV8 r) . SEG8E3 = (DES-DIV8 r) . 3 & (DES-DIV8 r) . SEG8E4 = (DES-DIV8 r) . 4 & (DES-DIV8 r) . SEG8E5 = (DES-DIV8 r) . 5 & (DES-DIV8 r) . SEG8E6 = (DES-DIV8 r) . 6 & (DES-DIV8 r) . SEG8E7 = (DES-DIV8 r) . 7 & (DES-DIV8 r) . SEG8E8 = (DES-DIV8 r) . 8 & r = ((((((((DES-DIV8 r) . SEG8E1) ^ ((DES-DIV8 r) . SEG8E2)) ^ ((DES-DIV8 r) . SEG8E3)) ^ ((DES-DIV8 r) . SEG8E4)) ^ ((DES-DIV8 r) . SEG8E5)) ^ ((DES-DIV8 r) . SEG8E6)) ^ ((DES-DIV8 r) . SEG8E7)) ^ ((DES-DIV8 r) . SEG8E8) )
; verum