defpred S1[ Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))] means for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = ($1 . i) . j & keyij = ($2 . i) . j & ($3 . i) . j = Op-XOR (textij,keyij) );
A1:
for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[text,key,z]
proof
let text,
key be
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[text,key,z]
text in 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then Q01:
ex
s being
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * st
(
text = s &
len s = 4 )
;
key in 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then Q02:
ex
s being
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * st
(
key = s &
len s = 4 )
;
defpred S2[
Nat,
set ]
means ex
zk being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) st
( $2
= zk & ( for
j being
Nat st
j in Seg 4 holds
ex
textij,
keyij being
Element of 8
-tuples_on BOOLEAN st
(
textij = (text . $1) . j &
keyij = (key . $1) . j &
zk . j = Op-XOR (
textij,
keyij) ) ) );
Q1:
for
k being
Nat st
k in Seg 4 holds
ex
zk being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) st
S2[
k,
zk]
proof
let k be
Nat;
( k in Seg 4 implies ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk] )
assume Q11:
k in Seg 4
;
ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk]
then
k in dom text
by Q01, FINSEQ_1:def 3;
then
text . k in rng text
by FUNCT_1:3;
then
text . k in 4
-tuples_on (8 -tuples_on BOOLEAN)
;
then Q13:
ex
s being
Element of
(8 -tuples_on BOOLEAN) * st
(
text . k = s &
len s = 4 )
;
then reconsider textk =
text . k as
Element of
(8 -tuples_on BOOLEAN) * ;
k in dom key
by Q02, FINSEQ_1:def 3, Q11;
then
key . k in rng key
by FUNCT_1:3;
then
key . k in 4
-tuples_on (8 -tuples_on BOOLEAN)
;
then Q16:
ex
s being
Element of
(8 -tuples_on BOOLEAN) * st
(
key . k = s &
len s = 4 )
;
then reconsider keyk =
key . k as
Element of
(8 -tuples_on BOOLEAN) * ;
defpred S3[
Nat,
set ]
means ex
textij,
keyij being
Element of 8
-tuples_on BOOLEAN st
(
textij = textk . $1 &
keyij = keyk . $1 & $2
= Op-XOR (
textij,
keyij) );
Q18:
for
j being
Nat st
j in Seg 4 holds
ex
xi being
Element of 8
-tuples_on BOOLEAN st
S3[
j,
xi]
consider zk being
FinSequence of 8
-tuples_on BOOLEAN such that Q22:
(
dom zk = Seg 4 & ( for
j being
Nat st
j in Seg 4 holds
S3[
j,
zk . j] ) )
from FINSEQ_1:sch 5(Q18);
Q23:
len zk = 4
by Q22, FINSEQ_1:def 3;
reconsider zk =
zk as
Element of
(8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
zk in 4
-tuples_on (8 -tuples_on BOOLEAN)
by Q23;
then reconsider zk =
zk as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
for
j being
Nat st
j in Seg 4 holds
ex
textij,
keyij being
Element of 8
-tuples_on BOOLEAN st
(
textij = textk . j &
keyij = keyk . j &
zk . j = Op-XOR (
textij,
keyij) )
by Q22;
hence
ex
zk being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) st
S2[
k,
zk]
;
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)) ;
take
z
;
S1[text,key,z]
for
i,
j being
Nat st
i in Seg 4 &
j in Seg 4 holds
ex
textij,
keyij being
Element of 8
-tuples_on BOOLEAN st
(
textij = (text . i) . j &
keyij = (key . i) . j &
(z . i) . j = Op-XOR (
textij,
keyij) )
hence
S1[
text,
key,
z]
;
verum
end;
consider I being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) such that
A2:
for x, y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds S1[x,y,I . (x,y)]
from BINOP_1:sch 3(A1);
take
I
; for text, key being 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
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((I . (text,key)) . i) . j = Op-XOR (textij,keyij) )
thus
for text, key being 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
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((I . (text,key)) . i) . j = Op-XOR (textij,keyij) )
by A2; verum