let m be non zero Nat; :: thesis: for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))
let z be Tuple of m, BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))
let d be Element of BOOLEAN ; :: thesis: (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))
set OV = IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)));
set UD = IFEQ ((Int_add_udfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)));
A1: Int_add_udfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>)) = (((('not' z) ^ <*('not' d)*>) /. (m + 1)) '&' FALSE) '&' ('not' ((carry ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))) /. (m + 1))) by BINARITH:2
.= FALSE ;
A2: (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = (Intval ((('not' z) ^ <*('not' d)*>) + (Bin1 (m + 1)))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) by Th9
.= (Intval ((('not' z) ^ <*('not' d)*>) + (Bin1 (m + 1)))) + (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) by Th9
.= (Intval ((('not' z) ^ <*('not' d)*>) + ((Bin1 m) ^ <*FALSE*>))) + (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) by Th7
.= (Intval ((('not' z) ^ <*('not' d)*>) + ((Bin1 m) ^ <*FALSE*>))) + (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)))) by Th7
.= ((((Intval (('not' z) ^ <*('not' d)*>)) + (Intval ((Bin1 m) ^ <*FALSE*>))) - (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_udfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)))) by Th12
.= ((((Intval (('not' z) ^ <*('not' d)*>)) + 1) - (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_udfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)))) by Th8
.= (((Intval (('not' z) ^ <*('not' d)*>)) + 1) + (IFEQ ((Int_add_udfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1))))) - ((IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)))) - (IFEQ ((Int_add_ovfl ((('not' z) ^ <*('not' d)*>),((Bin1 m) ^ <*FALSE*>))),FALSE,0,(2 to_power (m + 1)))))
.= ((Intval (('not' z) ^ <*('not' d)*>)) + 1) + 0 by A1, FUNCOP_1:def 8
.= ((Absval ('not' z)) - (IFEQ (('not' d),FALSE,0,(2 to_power m)))) + 1 by Th10
.= ((((- (Absval z)) + (2 to_power m)) - 1) - (IFEQ (('not' d),FALSE,0,(2 to_power m)))) + 1 by Th13
.= ((- (Absval z)) + (2 to_power m)) - (IFEQ (('not' d),FALSE,0,(2 to_power m))) ;
A3: - (Intval (z ^ <*d*>)) = - ((Absval z) - (IFEQ (d,FALSE,0,(2 to_power m)))) by Th10
.= (- (Absval z)) + (IFEQ (d,FALSE,0,(2 to_power m))) ;

per cases ( d = FALSE or d = TRUE ) by XBOOLEAN:def 3;

suppose A4: d = FALSE ; :: thesis: (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))

then (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = ((- (Absval z)) + (2 to_power m)) - (2 to_power m) by A2, FUNCOP_1:def 8
.= (- (Absval z)) + 0 ;
hence (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>)) by A3, A4, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A5: d = TRUE ; :: thesis: (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))

then (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = ((- (Absval z)) + (2 to_power m)) - 0 by A2, FUNCOP_1:def 8
.= (- (Absval z)) + (2 to_power m) ;
hence (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>)) by A3, A5, FUNCOP_1:def 8; :: thesis: verum

end;

end;