let m be non zero Nat; 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 ; 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 ; (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
;
(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;
verum end; suppose A5:
d = TRUE
;
(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;
verum end; end;