for SBT being Permutation of (8 -tuples_on BOOLEAN)
for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) holds
AES-DEC (SBT,MCFunc,(AES-ENC (SBT,MCFunc,text,Key)),Key) = text