theorem Th11: :: BINARI_2:11

for m being non zero Nat
for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))