(****************************************************************************** * D A T A E N C R Y P T I O N S T A N D A R D *----------------------------------------------------------------------------- * INRIA - Unite de Recherche Rhone-Alpes * 655, avenue de l'Europe * 38330 Montbonnot Saint Martin * FRANCE *----------------------------------------------------------------------------- * Module : S_BOX_FUNCTIONS.lib * Auteur : Wendelin SERWE * Version : 1.6 * Date : 2015/09/04 14:05:18 *****************************************************************************) (* definition of the functions used by the S-boxes *) type S_BOX_FUNCTIONS is BIT4, BIT6 opns S1 : BIT6 -> BIT4 S2 : BIT6 -> BIT4 S3 : BIT6 -> BIT4 S4 : BIT6 -> BIT4 S5 : BIT6 -> BIT4 S6 : BIT6 -> BIT4 S7 : BIT6 -> BIT4 S8 : BIT6 -> BIT4 eqns (* * in the equations below, premisses are used rather than pattern * matching because '1' is a constructor for type BIT_CONCRETE * but not for type BIT_ABSTRACT *) forall BV6 : BIT6 ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S1 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S1 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S1 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S1 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S1 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S1 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S1 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S1 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S1 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S1 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S1 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S1 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S1 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S1 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S1 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S1 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S1 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S1 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S1 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S1 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S1 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S1 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S1 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S1 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S1 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S1 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S1 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S1 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S1 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S1 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S1 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S1 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S1 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S1 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S1 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S1 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S1 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S1 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S1 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S1 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S1 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S1 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S1 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S1 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S1 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S1 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S1 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S1 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S1 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S1 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S1 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S1 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S1 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S1 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S1 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S1 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S1 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S1 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S1 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S1 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S1 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S1 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S1 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S1 (BV6) = MK_4 (1, 1, 0, 1); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S2 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S2 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S2 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S2 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S2 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S2 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S2 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S2 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S2 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S2 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S2 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S2 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S2 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S2 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S2 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S2 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S2 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S2 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S2 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S2 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S2 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S2 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S2 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S2 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S2 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S2 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S2 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S2 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S2 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S2 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S2 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S2 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S2 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S2 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S2 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S2 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S2 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S2 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S2 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S2 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S2 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S2 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S2 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S2 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S2 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S2 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S2 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S2 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S2 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S2 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S2 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S2 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S2 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S2 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S2 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S2 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S2 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S2 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S2 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S2 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S2 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S2 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S2 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S2 (BV6) = MK_4 (1, 0, 0, 1); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S3 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S3 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S3 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S3 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S3 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S3 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S3 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S3 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S3 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S3 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S3 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S3 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S3 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S3 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S3 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S3 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S3 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S3 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S3 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S3 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S3 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S3 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S3 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S3 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S3 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S3 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S3 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S3 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S3 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S3 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S3 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S3 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S3 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S3 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S3 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S3 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S3 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S3 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S3 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S3 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S3 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S3 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S3 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S3 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S3 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S3 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S3 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S3 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S3 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S3 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S3 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S3 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S3 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S3 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S3 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S3 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S3 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S3 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S3 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S3 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S3 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S3 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S3 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S3 (BV6) = MK_4 (1, 1, 0, 0); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S4 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S4 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S4 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S4 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S4 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S4 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S4 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S4 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S4 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S4 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S4 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S4 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S4 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S4 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S4 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S4 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S4 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S4 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S4 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S4 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S4 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S4 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S4 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S4 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S4 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S4 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S4 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S4 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S4 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S4 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S4 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S4 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S4 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S4 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S4 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S4 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S4 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S4 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S4 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S4 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S4 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S4 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S4 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S4 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S4 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S4 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S4 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S4 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S4 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S4 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S4 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S4 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S4 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S4 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S4 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S4 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S4 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S4 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S4 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S4 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S4 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S4 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S4 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S4 (BV6) = MK_4 (1, 1, 1, 0); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S5 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S5 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S5 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S5 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S5 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S5 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S5 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S5 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S5 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S5 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S5 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S5 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S5 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S5 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S5 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S5 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S5 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S5 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S5 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S5 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S5 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S5 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S5 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S5 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S5 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S5 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S5 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S5 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S5 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S5 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S5 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S5 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S5 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S5 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S5 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S5 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S5 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S5 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S5 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S5 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S5 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S5 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S5 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S5 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S5 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S5 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S5 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S5 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S5 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S5 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S5 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S5 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S5 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S5 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S5 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S5 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S5 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S5 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S5 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S5 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S5 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S5 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S5 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S5 (BV6) = MK_4 (0, 0, 1, 1); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S6 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S6 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S6 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S6 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S6 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S6 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S6 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S6 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S6 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S6 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S6 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S6 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S6 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S6 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S6 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S6 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S6 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S6 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S6 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S6 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S6 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S6 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S6 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S6 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S6 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S6 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S6 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S6 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S6 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S6 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S6 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S6 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S6 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S6 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S6 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S6 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S6 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S6 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S6 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S6 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S6 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S6 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S6 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S6 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S6 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S6 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S6 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S6 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S6 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S6 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S6 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S6 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S6 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S6 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S6 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S6 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S6 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S6 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S6 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S6 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S6 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S6 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S6 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S6 (BV6) = MK_4 (1, 1, 0, 1); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S7 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S7 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S7 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S7 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S7 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S7 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S7 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S7 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S7 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S7 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S7 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S7 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S7 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S7 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S7 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S7 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S7 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S7 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S7 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S7 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S7 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S7 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S7 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S7 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S7 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S7 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S7 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S7 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S7 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S7 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S7 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S7 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S7 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S7 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S7 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S7 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S7 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S7 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S7 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S7 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S7 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S7 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S7 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S7 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S7 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S7 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S7 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S7 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S7 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S7 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S7 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S7 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S7 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S7 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S7 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S7 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S7 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S7 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S7 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S7 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S7 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S7 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S7 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S7 (BV6) = MK_4 (1, 1, 0, 0); ofsort BIT4 BV6 = MK_6 (0, 0, 0, 0, 0, 0) => S8 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 0) => S8 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (0, 0, 0, 1, 0, 0) => S8 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 0, 1, 1, 0) => S8 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 0) => S8 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 0) => S8 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 0) => S8 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 0) => S8 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 0, 0, 0) => S8 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 0) => S8 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 0) => S8 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 1, 0, 1, 1, 0) => S8 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 0, 0, 0) => S8 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 1, 0, 1, 0) => S8 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 0) => S8 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 1, 1, 1, 0) => S8 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 0, 0, 1) => S8 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (0, 0, 0, 0, 1, 1) => S8 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (0, 0, 0, 1, 0, 1) => S8 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (0, 0, 0, 1, 1, 1) => S8 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (0, 0, 1, 0, 0, 1) => S8 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (0, 0, 1, 0, 1, 1) => S8 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 0, 1) => S8 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (0, 0, 1, 1, 1, 1) => S8 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 0, 1) => S8 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (0, 1, 0, 0, 1, 1) => S8 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (0, 1, 0, 1, 0, 1) => S8 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (0, 1, 0, 1, 1, 1) => S8 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (0, 1, 1, 0, 0, 1) => S8 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (0, 1, 1, 0, 1, 1) => S8 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (0, 1, 1, 1, 0, 1) => S8 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (0, 1, 1, 1, 1, 1) => S8 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 0) => S8 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 0, 0, 1, 0) => S8 (BV6) = MK_4 (1, 0, 1, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 0) => S8 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 0) => S8 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 0) => S8 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 0, 1, 0, 1, 0) => S8 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 0) => S8 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 0) => S8 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 0, 0, 0) => S8 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 0, 0, 1, 0) => S8 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 0) => S8 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 1, 0, 1, 1, 0) => S8 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 0, 0, 0) => S8 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 0) => S8 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 0) => S8 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 1, 0) => S8 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 0, 0, 0, 1) => S8 (BV6) = MK_4 (0, 0, 1, 0); BV6 = MK_6 (1, 0, 0, 0, 1, 1) => S8 (BV6) = MK_4 (0, 0, 0, 1); BV6 = MK_6 (1, 0, 0, 1, 0, 1) => S8 (BV6) = MK_4 (1, 1, 1, 0); BV6 = MK_6 (1, 0, 0, 1, 1, 1) => S8 (BV6) = MK_4 (0, 1, 1, 1); BV6 = MK_6 (1, 0, 1, 0, 0, 1) => S8 (BV6) = MK_4 (0, 1, 0, 0); BV6 = MK_6 (1, 0, 1, 0, 1, 1) => S8 (BV6) = MK_4 (1, 0, 1, 0); BV6 = MK_6 (1, 0, 1, 1, 0, 1) => S8 (BV6) = MK_4 (1, 0, 0, 0); BV6 = MK_6 (1, 0, 1, 1, 1, 1) => S8 (BV6) = MK_4 (1, 1, 0, 1); BV6 = MK_6 (1, 1, 0, 0, 0, 1) => S8 (BV6) = MK_4 (1, 1, 1, 1); BV6 = MK_6 (1, 1, 0, 0, 1, 1) => S8 (BV6) = MK_4 (1, 1, 0, 0); BV6 = MK_6 (1, 1, 0, 1, 0, 1) => S8 (BV6) = MK_4 (1, 0, 0, 1); BV6 = MK_6 (1, 1, 0, 1, 1, 1) => S8 (BV6) = MK_4 (0, 0, 0, 0); BV6 = MK_6 (1, 1, 1, 0, 0, 1) => S8 (BV6) = MK_4 (0, 0, 1, 1); BV6 = MK_6 (1, 1, 1, 0, 1, 1) => S8 (BV6) = MK_4 (0, 1, 0, 1); BV6 = MK_6 (1, 1, 1, 1, 0, 1) => S8 (BV6) = MK_4 (0, 1, 1, 0); BV6 = MK_6 (1, 1, 1, 1, 1, 1) => S8 (BV6) = MK_4 (1, 0, 1, 1); endtype (* ------------------------------------------------------------------------- *)