:: deftheorem defines Int_add_udfl BINARI_2:def 5 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_udfl (z1,z2) = ((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n));