for SBT being 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