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*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),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*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),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*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
set f = FALSE ;
set t = TRUE ;
A1:
Absval (z1 + z2) = ((Absval z1) + (Absval z2)) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m))
proof
set siki1 =
Absval (z1 + z2);
set siki2 =
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m);
((Absval (z1 + z2)) + (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m))) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m)) = Absval (z1 + z2)
;
hence
Absval (z1 + z2) = ((Absval z1) + (Absval z2)) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m))
by BINARITH:47;
:: thesis: verum
end;
A2: Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) =
Intval ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl z1,z2))*>)
by BINARITH:45
.=
(((Absval z1) + (Absval z2)) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m))) - (IFEQ ((d1 'xor' d2) 'xor' (add_ovfl z1,z2)),FALSE ,0 ,(2 to_power m))
by A1, Th12
;
A3: Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>) =
(('not' d1) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) '&' ((carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (m + 1))
by BINARITH:3
.=
(('not' d1) '&' ('not' d2)) '&' ((carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (m + 1))
by BINARITH:3
.=
(('not' d1) '&' ('not' d2)) '&' (add_ovfl z1,z2)
by BINARITH:44
;
A4: Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>) =
(d1 '&' ((z2 ^ <*d2*>) /. (m + 1))) '&' ('not' ((carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (m + 1)))
by BINARITH:3
.=
(d1 '&' d2) '&' ('not' ((carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (m + 1)))
by BINARITH:3
.=
(d1 '&' d2) '&' ('not' (add_ovfl z1,z2))
by BINARITH:44
;
A5:
Intval (z1 ^ <*d1*>) = (Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m))
by Th12;
A6:
Intval (z2 ^ <*d2*>) = (Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m))
by Th12;
per cases
( ( d1 = FALSE & d2 = FALSE ) or ( d1 = TRUE & d2 = FALSE ) or ( d1 = FALSE & d2 = TRUE ) or ( d1 = TRUE & d2 = TRUE ) )
by XBOOLEAN:def 3;
suppose A7:
(
d1 = FALSE &
d2 = FALSE )
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then A8:
(Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) =
(Absval z1) - 0
by FUNCOP_1:def 8
.=
Absval z1
;
A9:
(Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) =
(Absval z2) - 0
by A7, FUNCOP_1:def 8
.=
Absval z2
;
A10:
IFEQ ((d1 '&' d2) '&' ('not' (add_ovfl z1,z2))),
FALSE ,
0 ,
(2 to_power (m + 1)) = 0
by A7, FUNCOP_1:def 8;
thus
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
:: thesis: verumproof
per cases
( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE )
by XBOOLEAN:def 3;
suppose
add_ovfl z1,
z2 = FALSE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A6, A7, A8, Th12;
:: thesis: verum end; suppose A11:
add_ovfl z1,
z2 = TRUE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m) = 2
to_power m
by FUNCOP_1:def 8;
then ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) =
(((Absval z1) + (Absval z2)) - (2 * (2 to_power m))) + (2 to_power (m + 1))
by A2, A3, A4, A7, A10, A11, FUNCOP_1:def 8
.=
(((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m))) + (2 to_power (m + 1))
by POWER:30
.=
(((Absval z1) + (Absval z2)) - (2 to_power (m + 1))) + (2 to_power (m + 1))
by POWER:32
.=
(Absval z1) + (Absval z2)
;
hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A6, A8, A9, Th12;
:: thesis: verum end;
end; end; suppose A12:
(
d1 = TRUE &
d2 = FALSE )
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then A13:
(Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) =
(Absval z2) - 0
by FUNCOP_1:def 8
.=
Absval z2
;
thus
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
:: thesis: verumproof
per cases
( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE )
by XBOOLEAN:def 3;
suppose A14:
add_ovfl z1,
z2 = FALSE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m) = 0
by FUNCOP_1:def 8;
hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A5, A6, A12, A13, A14;
:: thesis: verum end; suppose
add_ovfl z1,
z2 = TRUE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A5, A6, A12;
:: thesis: verum end;
end; end; suppose A15:
(
d1 = FALSE &
d2 = TRUE )
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then A16:
(Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) =
(Absval z1) - 0
by FUNCOP_1:def 8
.=
Absval z1
;
thus
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
:: thesis: verumproof
per cases
( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE )
by XBOOLEAN:def 3;
suppose A17:
add_ovfl z1,
z2 = FALSE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m) = 0
by FUNCOP_1:def 8;
hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A5, A6, A15, A16, A17;
:: thesis: verum end; suppose
add_ovfl z1,
z2 = TRUE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A5, A6, A15;
:: thesis: verum end;
end; end; suppose A18:
(
d1 = TRUE &
d2 = TRUE )
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then A19:
(Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) = (Absval z2) - (2 to_power m)
by FUNCOP_1:def 8;
A20:
(Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>)) =
((Absval z1) + (Absval z2)) - (2 * (2 to_power m))
by A5, A6, A18, A19
.=
((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m))
by POWER:30
.=
((Absval z1) + (Absval z2)) - (2 to_power (m + 1))
by POWER:32
;
A21:
IFEQ ((('not' d1) '&' ('not' d2)) '&' (add_ovfl z1,z2)),
FALSE ,
0 ,
(2 to_power (m + 1)) = 0
by A18, FUNCOP_1:def 8;
thus
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
:: thesis: verumproof
per cases
( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE )
by XBOOLEAN:def 3;
suppose A22:
add_ovfl z1,
z2 = FALSE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m) = 0
by FUNCOP_1:def 8;
hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A2, A3, A4, A18, A20, A21, A22, FUNCOP_1:def 8;
:: thesis: verum end; suppose A23:
add_ovfl z1,
z2 = TRUE
;
:: thesis: ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))then
IFEQ (add_ovfl z1,z2),
FALSE ,
0 ,
(2 to_power m) = 2
to_power m
by FUNCOP_1:def 8;
then ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) =
((Absval z1) + (Absval z2)) - (2 * (2 to_power m))
by A2, A3, A4, A18, A23
.=
((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m))
by POWER:30
.=
((Absval z1) + (Absval z2)) - (2 to_power (m + 1))
by POWER:32
;
hence
((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0 ,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
by A20;
:: thesis: verum end;
end; end;