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, 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))); :: thesis: 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; :: thesis: 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; :: thesis: verum