bv_abs[N:posnat] : THEORY BEGIN IMPORTING int2bv[N] BV : bvec[N] abs(bv:bvec[N] | bv2int(bv) > minint[N]) : {bv2: bvec[N] | bv2int(bv2) = abs(bv2int(bv))} = IF bv^(N-1) THEN int2bv_fun(-bv2int(bv)) ELSE bv ENDIF END bv_abs