let m be non empty 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:3
.=
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 Th11
.=
(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 Th11
.=
(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 Th9
.=
(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 Th9
.=
((((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 Th14
.=
((((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 Th10
.=
(((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 Th12
.=
((((- (Absval z)) + (2 to_power m)) - 1) - (IFEQ ('not' d),FALSE ,0 ,(2 to_power m))) + 1
by Th15
.=
((- (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 Th12
.=
(- (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;