:: deftheorem defines ADD_MOD IDEA_1:def 4 :
for n, i, j being Nat holds ADD_MOD (i,j,n) = (i + j) mod (2 to_power n);