let m be non empty Nat; :: thesis: 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*>))
let z1, z2 be Tuple of m,BOOLEAN ; :: thesis: 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*>))
let d1, d2 be Element of BOOLEAN ; :: thesis: (((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*>))
set OV1 = IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0 ,(2 to_power (m + 1));
set UD1 = IFEQ (Int_add_udfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0 ,(2 to_power (m + 1));
set OV2 = IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1));
set NEG = (Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>;
thus (((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*>) + (Neg2 (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))) by Th19
.= (((Intval ((z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>))) + (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))) by Th16
.= (((Intval ((z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>)),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))) by Th16
.= (((Intval ((z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>)),FALSE ,0 ,(2 to_power (m + 1)))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1))) by Th16
.= ((Intval (z1 ^ <*d1*>)) + (Intval ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1))) by Th13
.= (Intval (z1 ^ <*d1*>)) + ((Intval ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl ('not' z2),(Bin1 m)))*>)) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1))))
.= (Intval (z1 ^ <*d1*>)) + ((Intval (Neg2 (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0 ,(2 to_power (m + 1)))) by Th16
.= (Intval (z1 ^ <*d1*>)) + (- (Intval (z2 ^ <*d2*>))) by Th17
.= (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>)) ; :: thesis: verum