:: deftheorem defines AES192-DEC AESCIP_1:def 22 :
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 cipher being Element of 128 -tuples_on BOOLEAN
for Key being Element of 192 -tuples_on BOOLEAN holds AES192-DEC (SBT,MixColumns,cipher,Key) = (AES-Statearray ") . (AES-DEC (SBT,MixColumns,(AES-Statearray . cipher),(AES-KeyInitState192 Key)));