let output be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ShiftRows . (InvShiftRows . output) = output
ShiftRows . (InvShiftRows . output) in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P3: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( ShiftRows . (InvShiftRows . output) = s & len s = 4 ) ;
output in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P4: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( output = s & len s = 4 ) ;
now :: thesis: for i being Nat st 1 <= i & i <= len (ShiftRows . (InvShiftRows . output)) holds
(ShiftRows . (InvShiftRows . output)) . i = output . i
let i be Nat; :: thesis: ( 1 <= i & i <= len (ShiftRows . (InvShiftRows . output)) implies (ShiftRows . (InvShiftRows . output)) . i = output . i )
assume ( 1 <= i & i <= len (ShiftRows . (InvShiftRows . output)) ) ; :: thesis: (ShiftRows . (InvShiftRows . output)) . i = output . i
then XX2: i in Seg 4 by P3;
then consider xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
XX3: ( xi = output . i & (InvShiftRows . output) . i = Op-Shift (xi,(i - 1)) ) by DefInvShiftRows;
xi in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then YY1: ex s being Element of (8 -tuples_on BOOLEAN) * st
( xi = s & len s = 4 ) ;
consider yi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
XX4: ( yi = (InvShiftRows . output) . i & (ShiftRows . (InvShiftRows . output)) . i = Op-Shift (yi,(5 - i)) ) by DefShiftRows, XX2;
thus (ShiftRows . (InvShiftRows . output)) . i = Op-Shift (xi,((i - 1) + (5 - i))) by XX3, XX4, DESCIP_1:10, YY1
.= output . i by DESCIP_1:12, YY1, XX3 ; :: thesis: verum
end;
hence ShiftRows . (InvShiftRows . output) = output by P3, P4, FINSEQ_1:14; :: thesis: verum