theorem
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*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_ovfl (('not' (z2 ^ <*d2*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))