theorem Th18: :: BINARITH:18

for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN holds add_ovfl (z1,z2) = (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1)