let SBT be Permutation of (8 -tuples_on BOOLEAN); for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for message, Key being Element of 128 -tuples_on BOOLEAN holds AES128-DEC (SBT,MixColumns,(AES128-ENC (SBT,MixColumns,message,Key)),Key) = message
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); for message, Key being Element of 128 -tuples_on BOOLEAN holds AES128-DEC (SBT,MixColumns,(AES128-ENC (SBT,MixColumns,message,Key)),Key) = message
let message, Key be Element of 128 -tuples_on BOOLEAN; AES128-DEC (SBT,MixColumns,(AES128-ENC (SBT,MixColumns,message,Key)),Key) = message
reconsider text = AES-Statearray . message as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider sKey = AES-KeyInitState128 Key as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider cipher = AES-ENC (SBT,MixColumns,text,sKey) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider CBLOCK = AES128-ENC (SBT,MixColumns,message,Key) as Element of 128 -tuples_on BOOLEAN ;
AES128-DEC (SBT,MixColumns,CBLOCK,Key) =
(AES-Statearray ") . (AES-DEC (SBT,MixColumns,cipher,sKey))
by LMINV1
.=
(AES-Statearray ") . text
by LASTXX
;
hence
AES128-DEC (SBT,MixColumns,(AES128-ENC (SBT,MixColumns,message,Key)),Key) = message
by FUNCT_2:26; verum