:: deftheorem Def5 defines NEG_N IDEA_1:def 5 :
for n, i being Nat st i is_expressible_by n holds
NEG_N (i,n) = (2 to_power n) - i;