let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: for MixColumns being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 256 -tuples_on BOOLEAN holds AES256-DEC (SBT,MixColumns,(AES256-ENC (SBT,MixColumns,message,Key)),Key) = message
let MixColumns be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis: for message being Element of 128 -tuples_on BOOLEAN
for Key being Element of 256 -tuples_on BOOLEAN holds AES256-DEC (SBT,MixColumns,(AES256-ENC (SBT,MixColumns,message,Key)),Key) = message
let message be Element of 128 -tuples_on BOOLEAN; :: thesis: for Key being Element of 256 -tuples_on BOOLEAN holds AES256-DEC (SBT,MixColumns,(AES256-ENC (SBT,MixColumns,message,Key)),Key) = message
let Key be Element of 256 -tuples_on BOOLEAN; :: thesis: AES256-DEC (SBT,MixColumns,(AES256-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-KeyInitState256 Key as Element of 8 -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 = AES256-ENC (SBT,MixColumns,message,Key) as Element of 128 -tuples_on BOOLEAN ;
AES256-DEC (SBT,MixColumns,CBLOCK,Key) = (AES-Statearray ") . (AES-DEC (SBT,MixColumns,cipher,sKey)) by LMINV1
.= (AES-Statearray ") . text by LASTXX ;
hence AES256-DEC (SBT,MixColumns,(AES256-ENC (SBT,MixColumns,message,Key)),Key) = message by FUNCT_2:26; :: thesis: verum