:: deftheorem defines B6toN64 DESCIP_1:def 21 :
for t being Element of 6 -tuples_on BOOLEAN holds B6toN64 t = (((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5));