:: deftheorem defines Absval BINARITH:def 4 :
for n being Nat
for x being Tuple of n, BOOLEAN holds Absval x = addnat $$ (Binary x);