:: Binary Arithmetics. Addition and Subtraction of Integers
:: by Yasuho Mizuhara and Takaya Nishiyama
::
:: Received March 18, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, FINSEQ_2, MARGREL1, SUBSET_1, FINSEQ_1, PARTFUN1,
RELAT_1, FUNCT_1, FUNCOP_1, XBOOLEAN, ARYTM_3, INT_1, BINARITH, ARYTM_1,
POWER, ORDINAL4, CARD_1, TARSKI, BINOP_2, SETWISEO, BINARI_2, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, NUMBERS, FUNCT_1,
NAT_1, NAT_D, INT_1, PARTFUN1, BINOP_1, SETWOP_2, SERIES_1, FUNCOP_1,
FINSEQ_1, FINSEQ_2, FINSEQ_4, BINOP_2, XBOOLEAN, MARGREL1, BINARITH;
constructors PARTFUN1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, FINSEQ_4,
FINSOP_1, SERIES_1, BINARITH, BINOP_2, NAT_D, RELSET_1, TREES_3,
FUNCOP_1;
registrations ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN,
MARGREL1, FINSEQ_2, CARD_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities XBOOLEAN;
theorems BINARITH, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCOP_1, POWER, NAT_1,
FINSOP_1, BINOP_2, XBOOLEAN, PARTFUN1, XREAL_0, CARD_1;
schemes FINSEQ_2, NAT_1;
begin
reserve i,n for Nat;
reserve m for non zero Nat;
reserve p,q for Tuple of n, BOOLEAN;
reserve d,d1,d2 for Element of BOOLEAN;
Lm1: len p = n & len q = n & (for i st i in Seg n holds p/.i = q/.i)
implies p = q
proof
assume that
A1: len p = n and
A2: len q = n and
A3: for i st i in Seg n holds p/.i = q/.i;
A4: dom p = Seg n by A1,FINSEQ_1:def 3;
for i being Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume
A5: i in dom p;
then A6: i in dom q by A2,A4,FINSEQ_1:def 3;
A7: p/.i=p.i by A5,PARTFUN1:def 6;
q/.i = q.i by A6,PARTFUN1:def 6;
hence thesis by A3,A4,A5,A7;
end;
hence thesis by A1,A2,FINSEQ_2:9;
end;
definition
let n be Nat;
func Bin1 (n) -> Tuple of n, BOOLEAN means
:Def1:
for i st i in Seg n holds it/.i = IFEQ(i,1,TRUE,FALSE);
existence
proof
deffunc F(set) = IFEQ($1,1,TRUE,FALSE);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92;
then reconsider z as Tuple of n, BOOLEAN;
take z;
let i;
assume
A4: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by PARTFUN1:def 6
.= IFEQ(i,1,TRUE,FALSE) by A2,A3,A4;
end;
uniqueness
proof
let z1, z2 be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds z1/.i = IFEQ(i,1,TRUE,FALSE) and
A6: for i st i in Seg n holds z2/.i = IFEQ(i,1,TRUE,FALSE);
A7: len z1 = n by CARD_1:def 7;
A8: len z2 = n by CARD_1:def 7;
A9: dom z1 = Seg n by A7,FINSEQ_1:def 3;
now
let j be Nat;
assume
A10: j in dom z1;
then A11: j in dom z2 by A8,A9,FINSEQ_1:def 3;
thus z1.j = z1/.j by A10,PARTFUN1:def 6
.= IFEQ(j,1,TRUE,FALSE) by A5,A9,A10
.= z2/.j by A6,A9,A10
.= z2.j by A11,PARTFUN1:def 6;
end;
hence thesis by A7,A8,FINSEQ_2:9;
end;
end;
definition
let n be non zero Nat, x be Tuple of n, BOOLEAN;
func Neg2 (x) -> Tuple of n,BOOLEAN equals
'not' x + Bin1 (n);
correctness;
end;
definition
let n be Nat, x be Tuple of n, BOOLEAN;
func Intval (x) -> Integer equals
:Def3:
Absval (x) if x/.n = FALSE
otherwise Absval (x) - 2 to_power n;
correctness;
end;
definition
let n be non zero Nat, z1,z2 be Tuple of n, BOOLEAN;
func Int_add_ovfl(z1,z2) -> Element of BOOLEAN equals
'not' (z1/.n) '&' 'not' (z2/.n) '&' (carry(z1,z2)/.n);
correctness;
end;
definition
let n be non zero Nat, z1,z2 be Tuple of n, BOOLEAN;
func Int_add_udfl(z1,z2) -> Element of BOOLEAN equals
(z1/.n) '&' (z2/.n) '&' 'not' (carry(z1,z2)/.n);
correctness;
end;
theorem
for z1 being Tuple of 2, BOOLEAN holds
z1=<*FALSE*>^<*FALSE*> implies Intval(z1) = 0
proof
let z1 be Tuple of 2,BOOLEAN;
assume
A1: z1 = <*FALSE*>^<*FALSE*>;
consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:100;
A3: z1 = <*FALSE,FALSE*> by A1,FINSEQ_1:def 9;
then A4: z1/.1 = FALSE by FINSEQ_4:17;
A5: z1/.2 = FALSE by A3,FINSEQ_4:17;
1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:3,5;
then
A6: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by BINARITH:def 3
.= 0 by A4,FUNCOP_1:def 8;
2 in Seg 2 by FINSEQ_1:3;
then A7: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by
BINARITH:def 3
.= 0 by A5,FUNCOP_1:def 8;
(Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:17;
then Absval(z1) = addnat $$ (<* 0,0 *>) by A2,A6,A7,BINARITH:def 4
.= addnat $$ (<* 0 *>^<* 0 *>) by FINSEQ_1:def 9
.= addnat.(addnat$$<* 0 *>,addnat$$<* 0 *>) by FINSOP_1:5
.= addnat.(0,addnat$$<* 0 *>) by FINSOP_1:11
.= addnat.(0,0) by FINSOP_1:11
.= 0 + 0 by BINOP_2:def 23
.= 0;
hence thesis by A5,Def3;
end;
theorem Th2:
for z1 being Tuple of 2, BOOLEAN holds
z1=<*TRUE*>^<*FALSE*> implies Intval(z1) = 1
proof
let z1 be Tuple of 2,BOOLEAN;
assume
A1: z1 = <*TRUE*>^<*FALSE*>;
consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:100;
A3: z1 = <*TRUE,FALSE*> by A1,FINSEQ_1:def 9;
then A4: z1/.1 = TRUE by FINSEQ_4:17;
A5: z1/.2 = FALSE by A3,FINSEQ_4:17;
1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:3,5;
then
A6: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by BINARITH:def 3
.= 2 to_power(1-'1) by A4,FUNCOP_1:def 8;
1 - 1 = 0;
then 1 -' 1 = 0 by XREAL_0:def 2;
then A7: (Binary(z1))/.1 = 1 by A6,POWER:24;
2 in Seg 2 by FINSEQ_1:3;
then A8: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by
BINARITH:def 3
.= 0 by A5,FUNCOP_1:def 8;
(Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:17;
then Absval(z1) = addnat $$ (<* 1,0 *>) by A2,A7,A8,BINARITH:def 4
.= addnat $$ (<* 1 *>^<* 0 *>) by FINSEQ_1:def 9
.= addnat.(addnat$$<* 1 *>,addnat$$<* 0 *>) by FINSOP_1:5
.= addnat.(1,addnat$$<* 0 *>) by FINSOP_1:11
.= addnat.(1,0) by FINSOP_1:11
.= 1 + 0 by BINOP_2:def 23
.= 1;
hence thesis by A5,Def3;
end;
theorem
for z1 being Tuple of 2, BOOLEAN holds
z1=<*FALSE*>^<*TRUE*> implies Intval(z1) = -2
proof
let z1 be Tuple of 2,BOOLEAN;
assume
A1: z1 = <*FALSE*>^<*TRUE*>;
consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:100;
A3: z1 = <*FALSE,TRUE*> by A1,FINSEQ_1:def 9;
then A4: z1/.1 = FALSE by FINSEQ_4:17;
A5: z1/.2 = TRUE by A3,FINSEQ_4:17;
then A6: Intval(z1) = Absval(z1) - 2 to_power (1 + 1) by Def3
.= Absval(z1) - (2 to_power 1 * 2 to_power 1) by POWER:27
.= Absval(z1) - (2 * 2 to_power 1) by POWER:25
.= Absval(z1) - (2 * 2) by POWER:25
.= Absval(z1) - 4;
1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:3,5;
then
A7: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by BINARITH:def 3
.= 0 by A4,FUNCOP_1:def 8;
2 in Seg 2 by FINSEQ_1:3;
then A8: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by
BINARITH:def 3
.= 2 to_power(2-'1) by A5,FUNCOP_1:def 8;
2 - 1 = 1;
then 2 -' 1 = 1 by XREAL_0:def 2;
then A9: (Binary(z1))/.2 = 2 by A8,POWER:25;
(Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:17;
then Absval(z1) = addnat $$ (<* 0,2 *>) by A2,A7,A9,BINARITH:def 4
.= addnat $$ (<* 0 *>^<* 2 *>) by FINSEQ_1:def 9
.= addnat.(addnat$$<* 0 *>,addnat$$<* 2 *>) by FINSOP_1:5
.= addnat.(0,addnat$$<* 2 *>) by FINSOP_1:11
.= addnat.(0,2) by FINSOP_1:11
.= 0 + 2 by BINOP_2:def 23
.= 2;
hence thesis by A6;
end;
theorem
for z1 being Tuple of 2, BOOLEAN holds
z1=<*TRUE*>^<*TRUE*> implies Intval(z1) = -1
proof
let z1 be Tuple of 2,BOOLEAN;
assume
A1: z1 = <*TRUE*>^<*TRUE*>;
consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:100;
A3: z1 = <*TRUE,TRUE*> by A1,FINSEQ_1:def 9;
then A4: z1/.1 <> FALSE by FINSEQ_4:17;
A5: z1/.2 <> FALSE by A3,FINSEQ_4:17;
then A6: Intval(z1) = Absval(z1) - 2 to_power (1 + 1) by Def3
.= Absval(z1) - (2 to_power 1 * 2 to_power 1) by POWER:27
.= Absval(z1) - (2 * 2 to_power 1) by POWER:25
.= Absval(z1) - (2 * 2) by POWER:25
.= Absval(z1) - 4;
1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:3,5;
then
A7: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by BINARITH:def 3
.= 2 to_power(1-'1) by A4,FUNCOP_1:def 8;
1 - 1 = 0;
then 1 -' 1 = 0 by XREAL_0:def 2;
then A8: (Binary(z1))/.1 = 1 by A7,POWER:24;
2 in Seg 2 by FINSEQ_1:3;
then A9: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by
BINARITH:def 3
.= 2 to_power(2-'1) by A5,FUNCOP_1:def 8;
2 - 1 = 1;
then 2 -' 1 = 1 by XREAL_0:def 2;
then A10: (Binary(z1))/.2 = 2 by A9,POWER:25;
(Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:17;
then Absval(z1) = addnat $$ (<* 1,2 *>) by A2,A8,A10,BINARITH:def 4
.= addnat $$ (<* 1 *>^<* 2 *>) by FINSEQ_1:def 9
.= addnat.(addnat$$<* 1 *>,addnat$$<* 2 *>) by FINSOP_1:5
.= addnat.(1,addnat$$<* 2 *>) by FINSOP_1:11
.= addnat.(1,2) by FINSOP_1:11
.= 1 + 2 by BINOP_2:def 23
.= 3;
hence thesis by A6;
end;
theorem Th5:
for i st i in Seg n & i = 1 holds (Bin1(n))/.i = TRUE
proof
let i be Nat such that
A1: i in Seg n and
A2: i = 1;
thus (Bin1(n))/.i = IFEQ(i,1,TRUE,FALSE) by A1,Def1
.= TRUE by A2,FUNCOP_1:def 8;
end;
theorem Th6:
for i st i in Seg n & i <> 1 holds (Bin1(n))/.i = FALSE
proof
let i be Nat such that
A1: i in Seg n and
A2: i <> 1;
thus (Bin1(n))/.i = IFEQ(i,1,TRUE,FALSE) by A1,Def1
.= FALSE by A2,FUNCOP_1:def 8;
end;
theorem Th7:
Bin1 (m+1) = Bin1 (m)^<*FALSE*>
proof
A1: len(Bin1(m+1)) = m+1 & len(Bin1(m)^<*FALSE*>) = m+1 by CARD_1:def 7;
for i st i in Seg (m+1) holds (Bin1(m+1))/.i = (Bin1(m)^<*FALSE*>)/.i
proof
let i such that
A2: i in Seg (m+1);
per cases by A2,FINSEQ_2:7;
suppose
A3: i in Seg m;
thus (Bin1(m+1))/.i = (Bin1(m)^<*FALSE*>)/.i
proof
per cases;
suppose
A4: i = 1;
(Bin1(m)^<*FALSE*>)/.i = (Bin1(m))/.i by A3,BINARITH:1
.= TRUE by A3,A4,Th5;
hence thesis by A2,A4,Th5;
end;
suppose
A5: i <> 1;
(Bin1(m)^<*FALSE*>)/.i = (Bin1(m))/.i by A3,BINARITH:1
.= FALSE by A3,A5,Th6;
hence thesis by A2,A5,Th6;
end;
end;
end;
suppose
A6: i = m+1;
1 <> m + 1 by NAT_1:14;
then (Bin1(m+1))/.i = FALSE by A2,A6,Th6;
hence thesis by A6,BINARITH:2;
end;
end;
hence thesis by A1,Lm1;
end;
theorem Th8:
for m holds Intval (Bin1(m)^<*FALSE*>) = 1
proof
defpred P[non zero Nat] means Intval (Bin1($1)^<*FALSE*>) = 1;
A1: P[1]
proof
consider k being Element of BOOLEAN such that
A2: Bin1(1) = <* k *> by FINSEQ_2:97;
A3: (Bin1(1))/.1 = k by A2,FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then Bin1(1) = <*TRUE*> by A2,A3,Th5;
hence thesis by Th2;
end;
A4: now
let m be non zero Nat such that
A5: P[m];
(Bin1(m)^<*FALSE*>)/.(m+1) = FALSE by BINARITH:2;
then A6: Absval(Bin1(m)^<*FALSE*>) = 1 by A5,Def3;
(Bin1(m+1)^<*FALSE*>)/.(m+1+1) = FALSE by BINARITH:2;
then Intval(Bin1(m+1)^<*FALSE*>) = Absval(Bin1(m+1)^<*FALSE*>) by Def3
.= Absval(Bin1(m)^<*FALSE*>^<*FALSE*>) by Th7
.= Absval(Bin1(m)^<*FALSE*>)
+ IFEQ(FALSE,FALSE,0,2 to_power(m+1)) by BINARITH:20
.= 1 + 0 by A6,FUNCOP_1:def 8
.= 1;
hence P[m+1];
end;
thus for m holds P[m] from NAT_1:sch 10(A1,A4);
end;
theorem Th9:
for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
'not' (z^<* d *>) = 'not' z^<* 'not' d *>
proof
let z be Tuple of m,BOOLEAN;
let d;
A1: len('not' (z^<*d*>))= m+1 & len('not' z^<*'not' d*>) = m+1 by
CARD_1:def 7;
for i st i in Seg (m+1) holds
('not' (z^<*d*>))/.i = ('not' z^<*'not' d*>)/.i
proof
let i such that
A2: i in Seg (m+1);
per cases by A2,FINSEQ_2:7;
suppose
A3: i in Seg m;
A4: ('not' (z^<*d*>))/.i = 'not' ((z^<*d*>)/.i) by A2,BINARITH:def 1
.= 'not' (z/.i) by A3,BINARITH:1;
('not' z^<*'not' d*>)/.i = ('not' z)/.i by A3,BINARITH:1
.= 'not' (z/.i) by A3,BINARITH:def 1;
hence thesis by A4;
end;
suppose
A5: i = m + 1;
('not' (z^<*d*>))/.i = 'not' ((z^<*d*>)/.i) by A2,BINARITH:def 1
.= 'not' d by A5,BINARITH:2;
hence thesis by A5,BINARITH:2;
end;
end;
hence thesis by A1,Lm1;
end;
theorem Th10:
for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
Intval(z^<*d*>) =
Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat)
proof
let z be Tuple of m, BOOLEAN;
let d;
per cases by XBOOLEAN:def 3;
suppose
A1: d = FALSE;
then (z^<*d*>)/.(m+1) = FALSE by BINARITH:2;
then A2: Intval(z^<*d*>) = Absval(z^<*d*>) by Def3
.= Absval(z)+IFEQ(d,FALSE,0,2 to_power(m)) by BINARITH:20
.= Absval(z)+0 by A1,FUNCOP_1:def 8
.= Absval(z);
Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat)
= Absval(z) - 0 by A1,FUNCOP_1:def 8
.= Absval(z);
hence thesis by A2;
end;
suppose
A3: d = TRUE;
then (z^<*d*>)/.(m+1) <> FALSE by BINARITH:2;
then Intval(z^<*d*>) = Absval(z^<*d*>) - 2 to_power(m+1) by Def3
.= Absval(z) + IFEQ(d,FALSE,0,2 to_power m)-2 to_power(m+1)
by BINARITH:20
.= Absval(z) + 2 to_power m - 2 to_power(m+1)
by A3,FUNCOP_1:def 8
.= Absval(z) + 2 to_power m - (2 to_power m * 2 to_power 1) by POWER:27
.= Absval(z) + 2 to_power m - 2*2 to_power m by POWER:25
.= Absval(z) - 2 to_power m;
hence thesis by A3,FUNCOP_1:def 8;
end;
end;
theorem Th11:
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*>)
proof
let z1,z2 be Tuple of m,BOOLEAN;
let d1,d2 be Element of BOOLEAN;
set f = FALSE, 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),
siki2 = IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m);
siki1 + siki2 - siki2 = siki1;
hence thesis by BINARITH:21;
end;
A2: Intval(z1^<*d1*> + z2^<*d2*>)
= Intval((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>) by BINARITH:19
.= 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,Th10;
A3: Int_add_ovfl(z1^<*d1*>,z2^<*d2*>)
= 'not' d1 '&' 'not' ((z2^<*d2*>)/.(m+1)) '&'
((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:2
.= 'not' d1 '&' 'not' d2 '&' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1))
by BINARITH:2
.= 'not' d1 '&' 'not' d2 '&' add_ovfl(z1,z2) by BINARITH:18;
A4: Int_add_udfl(z1^<*d1*>,z2^<*d2*>) = d1 '&' ((z2^<*d2*>)/.(m+1)) '&'
'not' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:2
.= d1 '&' d2 '&' 'not' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:2
.= d1 '&' d2 '&' 'not' add_ovfl(z1,z2) by BINARITH:18;
A5: Intval(z1^<*d1*>) = Absval(z1)-IFEQ(d1,FALSE,0,2 to_power m) by Th10;
A6: Intval(z2^<*d2*>) = Absval(z2)-IFEQ(d2,FALSE,0,2 to_power m) by Th10;
per cases by XBOOLEAN:def 3;
suppose
A7: d1 = f & d2 = f;
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)),f,0,2 to_power(m+1))
= 0 by A7,FUNCOP_1:def 8;
thus thesis
proof
per cases by XBOOLEAN:def 3;
suppose
add_ovfl(z1,z2) = f;
hence thesis by A2,A3,A4,A6,A7,A8,Th10;
end;
suppose
A11: add_ovfl(z1,z2) = t;
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:25
.= (Absval(z1) + Absval(z2))
- 2 to_power (m+1) + 2 to_power(m+1) by POWER:27
.= Absval(z1) + Absval(z2);
hence thesis by A6,A8,A9,Th10;
end;
end;
end;
suppose
A12: d1 = t & d2 = f;
then A13: Absval(z2) - IFEQ(d2,FALSE,0,2 to_power m)
= Absval(z2) - 0 by FUNCOP_1:def 8
.= Absval(z2);
thus thesis
proof
per cases by XBOOLEAN:def 3;
suppose
A14: add_ovfl(z1,z2) = f;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by FUNCOP_1:def 8;
hence thesis by A2,A3,A4,A5,A6,A12,A13,A14;
end;
suppose
add_ovfl(z1,z2) = t;
hence thesis by A2,A3,A4,A5,A6,A12;
end;
end;
end;
suppose
A15: d1 = f & d2 = t;
then A16: Absval(z1) - IFEQ(d1,FALSE,0,2 to_power m)
= Absval(z1) - 0 by FUNCOP_1:def 8
.= Absval(z1);
thus thesis
proof
per cases by XBOOLEAN:def 3;
suppose
A17: add_ovfl(z1,z2) = f;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by FUNCOP_1:def 8;
hence thesis by A2,A3,A4,A5,A6,A15,A16,A17;
end;
suppose
add_ovfl(z1,z2) = t;
hence thesis by A2,A3,A4,A5,A6,A15;
end;
end;
end;
suppose
A18: d1 = t & d2 = t;
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)-IFEQ(d1,FALSE,0,2 to_power m) + Intval(z2^<*d2*>)
by A5
.= (Absval(z1) + Absval(z2)) - (2*2 to_power m) by A6,A18,A19
.= (Absval(z1) + Absval(z2)) - (2 to_power 1*2 to_power m) by POWER:25
.= (Absval(z1) + Absval(z2)) - 2 to_power(m+1) by POWER:27;
A21: IFEQ(('not' d1 '&' 'not' d2 '&' add_ovfl(z1,z2)),f,0,2 to_power(m+1 ))
= 0 by A18,FUNCOP_1:def 8;
thus thesis
proof
per cases by XBOOLEAN:def 3;
suppose
A22: add_ovfl(z1,z2) = f;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by FUNCOP_1:def 8;
hence thesis by A2,A3,A4,A18,A20,A21,A22,FUNCOP_1:def 8;
end;
suppose
A23: add_ovfl(z1,z2) = t;
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:25
.= (Absval(z1) + Absval(z2)) - 2 to_power(m+1) by POWER:27;
hence thesis by A20;
end;
end;
end;
end;
theorem Th12:
for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
Intval(z1^<*d1*>+z2^<*d2*>) = Intval(z1^<*d1*>) + Intval(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))
proof
let z1,z2 be Tuple of m,BOOLEAN;
let d1,d2;
set A = Intval(z1^<*d1*>+z2^<*d2*>),
B = IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1)),
C = IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1)),
D = Intval(z1^<*d1*>) + Intval(z2^<*d2*>);
A + B - C = D by Th11;
hence thesis;
end;
theorem Th13:
for m for x being Tuple of m, BOOLEAN holds
Absval('not' x) = - Absval(x) + 2 to_power m - 1
proof
defpred P[Nat] means for x being Tuple of $1, BOOLEAN holds
Absval('not' x) = - Absval(x) + 2 to_power $1 - 1;
A1: P[1]
proof
let x be Tuple of 1, BOOLEAN;
per cases by BINARITH:14;
suppose
A2: x = <*FALSE*>;
then A3: x/.1 = FALSE by FINSEQ_4:16;
consider k being Element of BOOLEAN such that
A4: 'not' x = <* k *> by FINSEQ_2:97;
A5: ('not' x)/.1 = k by A4,FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then A6: ('not' x)/.1 = 'not' FALSE by A3,BINARITH:def 1
.= TRUE;
- Absval(x) + 2 to_power 1 - 1 = - 0 + 2 to_power 1 - 1 by A2,BINARITH:15
.= 0 + 2 - 1 by POWER:25
.= 1;
hence thesis by A4,A5,A6,BINARITH:16;
end;
suppose
A7: x = <*TRUE*>;
then A8: x/.1 = TRUE by FINSEQ_4:16;
consider k being Element of BOOLEAN such that
A9: 'not' x = <* k *> by FINSEQ_2:97;
A10: ('not' x)/.1 = k by A9,FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then A11: ('not' x)/.1 = 'not' TRUE by A8,BINARITH:def 1
.= FALSE;
- Absval(x) + 2 to_power 1 - 1 = - 1 + 2 to_power 1 - 1 by A7,BINARITH:16
.= - 1 + 2 - 1 by POWER:25
.= 0;
hence thesis by A9,A10,A11,BINARITH:15;
end;
end;
A12: now
let m;
assume
A13: P[m];
now
let x be Tuple of m+1, BOOLEAN;
consider t being (Element of m-tuples_on BOOLEAN),
d being Element of BOOLEAN such that
A14: x = t^<*d*> by FINSEQ_2:117;
A15: Absval('not' x) = Absval('not' t^<*'not' d*>) by A14,Th9
.= Absval('not' t) + IFEQ('not' d,FALSE,0,2 to_power m) by BINARITH:20
.= - Absval(t) + 2 to_power m - 1
+ IFEQ('not' d,FALSE,0,2 to_power m) by A13;
A16: - Absval(x) + 2 to_power(m+1) - 1
= - (Absval(t) + IFEQ(d,FALSE,0,2 to_power m))
+ 2 to_power(m+1) - 1 by A14,BINARITH:20;
thus Absval('not' x) = - Absval(x) + 2 to_power (m+1) - 1
proof
per cases by XBOOLEAN:def 3;
suppose
A17: d = FALSE;
then A18: Absval
('not' x) = - Absval(t) + 2 to_power m - 1 + 2 to_power m
by A15,FUNCOP_1:def 8
.= - Absval(t) + 2*2 to_power m - 1
.= - Absval(t) + 2 to_power 1*2 to_power m - 1 by POWER:25
.= - Absval(t) + 2 to_power(m+1) - 1 by POWER:27;
- Absval(x) + 2 to_power(m+1) - 1
= -(Absval(t) + 0) + 2 to_power(m+1) - 1 by A16,A17,FUNCOP_1:def 8
.= - Absval(t) + 2 to_power(m+1) - 1;
hence thesis by A18;
end;
suppose
A19: d = TRUE;
then A20: Absval('not' x)
= - Absval(t) + 2 to_power m - 1 + 0 by A15,FUNCOP_1:def 8
.= - Absval(t) + 2 to_power m - 1;
- Absval(x) + 2 to_power(m+1) - 1
= -(Absval(t) + 2 to_power m) + 2 to_power(m+1) - 1
by A16,A19,FUNCOP_1:def 8
.= - Absval(t) - 2 to_power m + 2 to_power 1*2 to_power m - 1
by POWER:27
.= - Absval(t) - 2 to_power m + 2*2 to_power m - 1
by POWER:25
.= - Absval(t) + 2 to_power m - 1;
hence thesis by A20;
end;
end;
end;
hence P[m+1];
end;
thus for m holds P[m] from NAT_1:sch 10(A1,A12);
end;
theorem Th14:
for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
Neg2(z^<*d*>) = Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>
proof
let z be Tuple of m, BOOLEAN;
let d;
thus Neg2(z^<*d*>) = 'not' z^<*'not' d*> + Bin1(m+1) by Th9
.= 'not' z^<*'not' d*> + Bin1(m)^<*FALSE*> by Th7
.= ('not' z + Bin1(m))^<*'not' d 'xor' FALSE 'xor' add_ovfl('not'
z,Bin1(m))*> by BINARITH:19
.= Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>;
end;
theorem Th15:
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*>)
proof
let z be Tuple of m, BOOLEAN;
let d;
set OV = IFEQ(Int_add_ovfl('not' z^<*'not' d*>,Bin1(m)^<*FALSE*>),FALSE,0,
2 to_power(m+1)),
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*>) + OV by Th7
.= Intval('not' z^<*'not'
d*>) + Intval(Bin1(m)^<*FALSE*>) - OV + UD + OV by Th12
.= (Intval('not' z^<*'not' d*>) + 1) - OV + UD + OV by Th8
.= (Intval('not' z^<*'not' d*>) + 1 + UD) - (OV - OV)
.= 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 by XBOOLEAN:def 3;
suppose
A4: d = FALSE;
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 thesis by A3,A4,FUNCOP_1:def 8;
end;
suppose
A5: d = TRUE;
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 thesis by A3,A5,FUNCOP_1:def 8;
end;
end;
theorem
for m for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
Neg2(Neg2(z^<*d*>)) = z^<*d*>
proof
defpred P[non zero Nat] means for z being Tuple of $1, BOOLEAN
for d being Element of BOOLEAN holds Neg2(Neg2(z^<*d*>)) = z^<*d*>;
A1: P[1]
proof
let z be Tuple of 1, BOOLEAN;
let d be Element of BOOLEAN;
set NZD = 'not' d 'xor' 'not' (z/.1);
set DPI = d '&' (z/.1), NZ1 = ('not' z)/.1;
set B1 = (Bin1(1))/.1;
A2: 1 in Seg 1 by FINSEQ_1:3;
A3: 'not' d 'xor' FALSE 'xor' add_ovfl('not' z,Bin1(1))
= 'not' d 'xor' ((NZ1 '&' B1) 'or'
(NZ1 '&' ((carry('not' z,Bin1(1)))/.1)) 'or'
(B1 '&' ((carry('not' z,Bin1(1)))/.1))) by BINARITH:def 6
.= 'not' d 'xor' ((NZ1 '&' B1) 'or' (NZ1 '&' FALSE) 'or'
(B1 '&' ((carry('not' z,Bin1(1)))/.1))) by BINARITH:def 2
.= 'not' d 'xor' ((NZ1 '&' B1) 'or'
FALSE 'or' (B1 '&' FALSE)) by BINARITH:def 2
.= 'not' d 'xor' (TRUE '&' NZ1) by A2,Th5
.= 'not' d 'xor' 'not' (z/.1) by A2,BINARITH:def 1;
A4: 'not' NZD 'xor' FALSE 'xor' add_ovfl('not' ('not' z + Bin1(1)),Bin1(1))
= 'not' NZD 'xor' (((('not' ('not' z + Bin1(1)))/.1) '&' B1) 'or'
((('not' ('not' z + Bin1(1)))/.1) '&'
((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1)) 'or'
(B1 '&' ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1))) by BINARITH:def 6
.= 'not' NZD 'xor'
(((('not' ('not' z + Bin1(1)))/.1) '&' ((Bin1(1))/.1)) 'or'
((('not' ('not' z + Bin1(1)))/.1) '&' FALSE) 'or'
(((Bin1(1))/.1) '&' ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1)))
by BINARITH:def 2
.= 'not' NZD 'xor'
(((('not' ('not' z + Bin1(1)))/.1) '&' ((Bin1(1))/.1)) 'or'
FALSE 'or' (B1 '&' FALSE)) by BINARITH:def 2
.=
'not' NZD 'xor' (TRUE '&' (('not' ('not' z + Bin1(1)))/.1)) by A2,Th5
.= 'not' NZD 'xor' 'not' ((('not' z + Bin1(1)))/.1) by A2,BINARITH:def 1
.= 'not' NZD 'xor' 'not' ((('not' z)/.1) 'xor' ((Bin1(1))/.1)
'xor' ((carry('not' z,Bin1(1)))/.1)) by A2,BINARITH:def 5
.= 'not' NZD 'xor' 'not' ((('not' z)/.1) 'xor' ((Bin1(1))/.1)
'xor' FALSE) by BINARITH:def 2
.= 'not' NZD 'xor' 'not' (NZ1 'xor' TRUE) by A2,Th5
.= 'not' NZD 'xor' 'not' (z/.1) by A2,BINARITH:def 1;
A5: Neg2(Neg2(z^<*d*>)) =
'not' ('not' z^<*'not' d*> + Bin1(1 + 1)) + Bin1(1 + 1) by Th9
.= 'not' ('not' z^<*'not' d*> + Bin1(1)^<*FALSE*>) + Bin1(1 + 1) by Th7
.= 'not' (('not' z + Bin1(1))
^<*'not' d 'xor' FALSE 'xor' add_ovfl('not' z,Bin1(1))*>)
+ Bin1(1 + 1) by BINARITH:19
.= 'not' ('not' z + Bin1(1))^<*'not' NZD*> + Bin1(1 + 1) by A3,Th9
.= 'not' ('not' z + Bin1(1))^<*'not' NZD*> + Bin1(1)^<*FALSE*> by Th7
.= ('not' ('not' z + Bin1(1))+ Bin1(1)) ^<*'not' NZD 'xor' 'not' (z/.1)*>
by A4,BINARITH:19;
then A6: (Neg2(Neg2(z^<*d*>)))/.1
= ('not' ('not' z + Bin1(1))+ Bin1(1))/.1 by A2,BINARITH:1
.= (('not' ('not' z + Bin1(1)))/.1) 'xor' ((Bin1(1))/.1) 'xor'
((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1) by A2,BINARITH:def 5
.= (('not' ('not' z + Bin1(1)))/.1) 'xor' ((Bin1(1))/.1) 'xor' FALSE
by BINARITH:def 2
.= (('not' ('not' z + Bin1(1)))/.1) 'xor' TRUE by A2,Th5
.= 'not' 'not' ((('not' z + Bin1(1)))/.1) by A2,BINARITH:def 1
.= (('not' z)/.1) 'xor' ((Bin1(1))/.1) 'xor' ((carry('not'
z,Bin1(1)))/.1) by A2,BINARITH:def 5
.= NZ1 'xor' ((Bin1(1))/.1) 'xor' FALSE by BINARITH:def 2
.= NZ1 'xor' TRUE by A2,Th5
.= 'not' 'not' (z/.1) by A2,BINARITH:def 1
.= z/.1;
reconsider p = d, q = z/.1 as boolean object;
A7: (Neg2(Neg2(z^<*d*>)))/.2 =
('not' d 'or' 'not' 'not' (z/.1)) '&' ('not' 'not' d
'or' 'not' (z/.1)) 'xor' 'not' (z/.1) by A5,BINARITH:2
.= ('not' p 'or' q) '&' p 'or' ('not' p 'or' q) '&'
'not' q 'xor' 'not' (z/.1) by XBOOLEAN:8
.= (p '&' 'not' p) 'or' p '&' q 'or' ('not' q '&' ('not' p 'or' q))
'xor' 'not' (z/.1) by XBOOLEAN:8
.= (d '&' 'not' d) 'or' (d '&' (z/.1)) 'or'
(('not' (z/.1) '&' 'not' d) 'or' ('not' (z/.1) '&'
(z/.1))) 'xor' 'not' (z/.1) by XBOOLEAN:8
.= FALSE 'or' (d '&' (z/.1)) 'or'
(('not' (z/.1) '&' 'not' d) 'or' ('not' (z/.1) '&'
(z/.1))) 'xor' 'not' (z/.1) by XBOOLEAN:138
.= DPI 'or' (('not' (z/.1) '&' 'not' d) 'or' FALSE)
'xor' 'not' (z/.1) by XBOOLEAN:138
.= (('not' d 'or' 'not' (z/.1)) '&' ('not' (z/.1) '&' ((z/.1) 'or' d)))
'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
.= (('not' d 'or' 'not' (z/.1)) '&' (('not' (z/.1) '&' (z/.1)) 'or'
('not' (z/.1) '&' d))) 'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
'not' 'not' (z/.1)) by XBOOLEAN:8
.= (('not' d 'or' 'not' (z/.1)) '&' (FALSE 'or' ('not'
(z/.1) '&' d))) 'or' (((d '&' (z/.1)) 'or' ('not' (z/.1) '&' 'not' d)) '&'
'not' 'not' (z/.1)) by XBOOLEAN:138
.= ((('not' (z/.1) '&' d) '&' 'not' d) 'or' (('not'
(z/.1) '&' d) '&' 'not' (z/.1)))
'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
'not' 'not' (z/.1)) by XBOOLEAN:8
.= (('not' (z/.1) '&' (d '&' 'not' d)) 'or' (('not'
(z/.1) '&' d) '&' 'not' (z/.1)))
'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
.= (('not' (z/.1) '&' FALSE) 'or' (('not'
(z/.1) '&' d) '&' 'not' (z/.1)))
'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
'not' 'not' (z/.1)) by XBOOLEAN:138
.= (d '&' ('not' (z/.1) '&' 'not' (z/.1)))
'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
.= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' ((z/.1) '&' d)) 'or'
((z/.1) '&' ('not' (z/.1) '&' 'not' d))) by XBOOLEAN:8
.= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' (z/.1) '&' d) 'or'
((z/.1) '&' ('not' (z/.1) '&' 'not' d)))
.= (d '&' 'not' (z/.1))
'or' (((z/.1) '&' d) 'or' ((z/.1) '&' 'not' (z/.1) '&' 'not' d))
.= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' d) 'or' (FALSE '&' 'not' d))
by XBOOLEAN:138
.= d '&' ('not' (z/.1) 'or' (z/.1)) by XBOOLEAN:8
.= TRUE '&' d by XBOOLEAN:102
.= d;
consider k1,k2 being Element of BOOLEAN such that
A8: Neg2(Neg2(z^<*d*>)) = <* k1,k2 *> by FINSEQ_2:100;
A9: (Neg2(Neg2(z^<*d*>)))/.1 = k1 & (Neg2(Neg2(z^<*d*>)))/.2 = k2 by A8,
FINSEQ_4:17;
consider k being Element of BOOLEAN such that
A10: z = <*k*> by FINSEQ_2:97;
Neg2(Neg2(z^<*d*>)) = <* k,d *> by A6,A7,A8,A9,A10,FINSEQ_4:16;
hence thesis by A10,FINSEQ_1:def 9;
end;
A11: now
let m;
assume
A12: P[m];
now
let z be Tuple of m+1, BOOLEAN;
let d be Element of BOOLEAN;
consider t being (Element of m-tuples_on BOOLEAN),
k being Element of BOOLEAN such that
A13: z = t^<*k*> by FINSEQ_2:117;
set A = add_ovfl('not' t,Bin1(m)), B = add_ovfl('not' Neg2(t),Bin1(m));
Neg2(Neg2(t^<*k*>))
= Neg2(Neg2(t)^<*'not' k 'xor' add_ovfl('not' t,Bin1(m))*>) by Th14
.= Neg2(Neg2(t))^<*'not' ('not' k 'xor' add_ovfl('not'
t,Bin1(m))) 'xor' add_ovfl('not' Neg2(t),Bin1(m))*> by Th14;
then A14: (Neg2(Neg2(t^<*k*>)))/.(m+1)
= 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) 'xor'
add_ovfl('not' Neg2(t),Bin1(m)) by BINARITH:2;
A15: (t^<*k*>)/.(m+1) = k by BINARITH:2;
reconsider p = k, q = A as boolean object;
'not' ('not' k 'xor' A) 'xor' B
= (p '&' ('not' p 'or' 'not' q) 'or' ('not' p 'or' 'not'
q) '&' q) 'xor' B by XBOOLEAN:8
.= (k '&' 'not' A 'or' A '&' ('not' k 'or' 'not'
A)) 'xor' B by XBOOLEAN:11
.= (A 'xor' k) 'xor' B by XBOOLEAN:11
.= k 'xor' (A 'xor' B) by XBOOLEAN:73;
then A16: k 'xor' (A 'xor' B) = k 'xor' FALSE by A12,A14,A15;
A17: k 'xor' (k 'xor' (A 'xor' B))
= (k 'xor' k) 'xor' (A 'xor' B) by XBOOLEAN:73
.= FALSE 'xor' (A 'xor' B) by XBOOLEAN:138
.= A 'xor' B;
A18: k 'xor' (k 'xor' FALSE) = FALSE by XBOOLEAN:138;
A19: A 'xor' (A 'xor' B) = (A 'xor' A) 'xor' B by XBOOLEAN:73
.= FALSE 'xor' B by XBOOLEAN:138
.= B;
A20: m + 1 in Seg(m+1) by FINSEQ_1:3;
A21: add_ovfl('not' z,Bin1(m+1))
= add_ovfl('not' t^<*'not' k*>,Bin1(m+1)) by A13,Th9
.= add_ovfl('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>) by Th7
.= ((('not' t^<*'not' k*>)/.(m+1)) '&'
((Bin1(m)^<*FALSE*>)/.(m+1))) 'or' ((('not' t^<*'not' k*>)/.(m+1)) '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
(((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:def 6
.= ((('not' t^<*'not' k*>)/.(m+1)) '&' FALSE) 'or'
((('not' t^<*'not' k*>)/.(m+1)) '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
(((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:2
.= FALSE 'or' ((('not' t^<*'not' k*>)/.(m+1)) '&' ((carry('not' t^<*'not'
k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or' (FALSE '&' ((carry('not' t^<*'not'
k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:2
.= 'not' k '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:2
.= 'not' k '&' A by BINARITH:18;
A22: add_ovfl('not' (Neg2(z)),Bin1(m+1))
= add_ovfl('not' (Neg2(z)),Bin1(m)^<*FALSE*>) by Th7
.= ((('not' (Neg2(z)))/.(m+1)) '&' ((Bin1(m)^<*FALSE*>)/.(m+1))) 'or'
((('not' (Neg2(z)))/.(m+1)) '&'
((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
(((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:def 6
.= ((('not' (Neg2(z)))/.(m+1)) '&' FALSE) 'or'
((('not' (Neg2(z)))/.(m+1)) '&'
((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
(((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:2
.= FALSE 'or' ((('not' (Neg2(z)))/.(m+1)) '&'
((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
(FALSE '&' ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1)))
by BINARITH:2
.= (('not' ('not' t^<*'not' k*> + Bin1(m+1)))/.(m+1)) '&'
((carry('not' ('not' (t^<*k*>) + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.(m+1))
by A13,Th9
.= (('not' ('not' t^<*'not' k*> + Bin1(m+1)))/.(m+1)) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.(m+1))
by Th9
.= (('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.
(m+1)) by Th7
.= (('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by Th7
.= 'not' ((('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by A20,BINARITH:def 1
.= 'not' ((('not' t^<*'not' k*>)/.(m+1)) 'xor' ((Bin1(m)^<*FALSE*>)/.(m+1))
'xor' ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by A20,BINARITH:def 5
.= 'not' ('not' k 'xor' ((Bin1(m)^<*FALSE*>)/.(m+1)) 'xor'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:2
.= 'not' ('not' k 'xor' FALSE 'xor'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:2
.= 'not' ('not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m))) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:18
.= 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) '&'
((carry('not' (('not' t + Bin1(m))
^<*'not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m))*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:19
.= 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) '&'
((carry(('not' ('not' t + Bin1(m))
^<*'not' ('not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m)))*>),
Bin1(m)^<*FALSE*>))/.(m+1)) by Th9
.= (('not' k 'or' 'not' A) '&' (k 'or' 'not' 'not'
A)) '&' A by A16,A17,A18,A19,BINARITH:18
.= ('not' k 'or' 'not' A) '&' (A '&' (k 'or' A))
.= A '&' ('not' A 'or' 'not' k) by XBOOLEAN:6
.= A '&' 'not' k by XBOOLEAN:11;
set C = 'not' k '&' A;
reconsider p = d, q = C as boolean object;
A23: 'not' ('not' d 'xor' C) 'xor' C
= ((p '&' ('not' p 'or' 'not' q)) 'or' (('not' p 'or' 'not'
q) '&' q)) 'xor' C by XBOOLEAN:8
.= ((d '&' 'not' C) 'or' (C '&' ('not' d 'or' 'not'
C))) 'xor' C by XBOOLEAN:11
.= C 'xor' d 'xor' C by XBOOLEAN:11
.= d 'xor' (C 'xor' C) by XBOOLEAN:73
.= d 'xor' FALSE by XBOOLEAN:138
.= d;
thus Neg2(Neg2(z^<*d*>))
= Neg2(Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m+1))*>) by Th14
.= Neg2(Neg2(z))^<*'not' ('not' d 'xor' add_ovfl('not'
z,Bin1(m+1))) 'xor' add_ovfl('not' Neg2(z),Bin1(m+1))*> by Th14
.= z^<*d*> by A12,A13,A21,A22,A23;
end;
hence P[m+1];
end;
thus for m holds P[m] from NAT_1:sch 10(A1,A11);
end;
definition
let n be non zero Nat, x, y be Tuple of n, BOOLEAN;
func x - y -> Tuple of n, BOOLEAN means
:Def6:
for i st i in Seg n holds
it/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
existence
proof
deffunc F(Nat) = (x/.$1) 'xor' ((Neg2(y))/.$1)
'xor' ((carry(x,Neg2(y)))/.$1);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92;
then reconsider z as Tuple of n, BOOLEAN;
take z;
let i;
assume
A4: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by PARTFUN1:def 6
.= (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) by A2,A3,A4;
end;
uniqueness
proof
let z1, z2 be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds
z1/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) and
A6: for i st i in Seg n holds
z2/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
A7: len z1 = n by CARD_1:def 7;
A8: len z2 = n by CARD_1:def 7;
A9: dom z1 = Seg n by A7,FINSEQ_1:def 3;
now
let j be Nat;
assume
A10: j in dom z1;
Seg n = Seg len z2 by CARD_1:def 7;
then A11: j in dom z2 by A9,A10,FINSEQ_1:def 3;
thus z1.j = z1/.j by A10,PARTFUN1:def 6
.= (x/.j) 'xor' ((Neg2(y))/.j) 'xor' ((carry(x,Neg2(y)))/.j) by A5,A9
,A10
.= z2/.j by A6,A9,A10
.= z2.j by A11,PARTFUN1:def 6;
end;
hence thesis by A7,A8,FINSEQ_2:9;
end;
end;
theorem Th17:
for x,y being Tuple of m, BOOLEAN holds x - y = x + Neg2(y)
proof
let x,y be Tuple of m, BOOLEAN;
for i st i in Seg m holds (x - y)/.i
= (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) by Def6;
hence thesis by BINARITH:def 5;
end;
theorem
for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
z1^<*d1*> - z2^<*d2*>
= (z1 + Neg2(z2))^<*d1 'xor' 'not' d2 'xor' add_ovfl('not'
z2,Bin1(m)) 'xor' add_ovfl(z1,Neg2(z2))*>
proof
let z1,z2 be Tuple of m, BOOLEAN;
let d1,d2;
thus z1^<*d1*> - z2^<*d2*> = z1^<*d1*> + Neg2(z2^<*d2*>) by Th17
.= z1^<*d1*> + Neg2(z2)^<*'not' d2 'xor' add_ovfl('not'
z2,Bin1(m))*> by Th14
.= (z1 + Neg2(z2))
^<*d1 'xor' ('not' d2 'xor' add_ovfl('not' z2,Bin1(m))) 'xor'
add_ovfl(z1,Neg2(z2))*> by BINARITH:19
.= (z1 + Neg2(z2))
^<*d1 'xor' 'not' d2 'xor' add_ovfl('not' z2,Bin1(m)) 'xor'
add_ovfl(z1,Neg2(z2))*> by XBOOLEAN:73;
end;
theorem
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*>)
proof
let z1,z2 be Tuple of m, BOOLEAN;
let d1,d2;
set OV1 = IFEQ(Int_add_ovfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,
2 to_power(m+1)),
UD1 = IFEQ(Int_add_udfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,
2 to_power(m+1)),
OV2 = IFEQ(Int_add_ovfl('not' (z2^<*d2*>),Bin1(m+1)),FALSE,0,
2 to_power(m+1)),
NEG = Neg2(z2)^<*'not' d2 'xor' add_ovfl('not' z2,Bin1(m))*>;
thus Intval(z1^<*d1*>-z2^<*d2*>) + OV1 - UD1 + OV2
= Intval(z1^<*d1*>+Neg2(z2^<*d2*>)) + OV1 - UD1 + OV2 by Th17
.= Intval(z1^<*d1*>+NEG) + OV1 - UD1 + OV2 by Th14
.= Intval(z1^<*d1*>+NEG)
+ IFEQ(Int_add_ovfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1))
- UD1 + OV2 by Th14
.= Intval(z1^<*d1*>+NEG)
+ IFEQ(Int_add_ovfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1))
- IFEQ(Int_add_udfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1)) + OV2 by Th14
.= Intval(z1^<*d1*>) + Intval(NEG) + OV2 by Th11
.= Intval(z1^<*d1*>) + (Intval(NEG) + OV2)
.= Intval(z1^<*d1*>) + (Intval(Neg2(z2^<*d2*>)) + OV2) by Th14
.= Intval(z1^<*d1*>) + (- Intval(z2^<*d2*>)) by Th15
.= Intval(z1^<*d1*>) - Intval(z2^<*d2*>);
end;