let m be non zero 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 Th17
.= (((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 Th14
.= (((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 Th14
.= (((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 Th14
.= ((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 Th11
.= (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 Th14
.= (Intval (z1 ^ <*d1*>)) + (- (Intval (z2 ^ <*d2*>))) by Th15
.= (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>)) ; :: thesis: verum