:: Binary Arithmetics. Addition
:: by Takaya Nishiyama and Yasuho Mizuhara
::
:: Received October 8, 1993
:: Copyright (c) 1993-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, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSEQ_1, ORDINAL4,
PARTFUN1, RELAT_1, ARYTM_3, CARD_1, MARGREL1, XBOOLEAN, XCMPLX_0,
FUNCT_1, XXREAL_0, ARYTM_1, FUNCOP_1, POWER, BINOP_2, SETWISEO, REAL_1,
BINARITH;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XBOOLEAN,
MARGREL1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, BINOP_2, SETWISEO,
FUNCOP_1, SETWOP_2, SERIES_1, FINSEQ_1, FINSEQ_2, XXREAL_0, NAT_1, NAT_D,
TREES_3;
constructors BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, BINOP_2, MARGREL1,
PARTFUN1, FINSOP_1, SERIES_1, RFINSEQ, REAL_1, NAT_D, RELSET_1, FINSEQ_2,
TREES_3, FUNCOP_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2,
XBOOLEAN, MARGREL1, FINSEQ_2, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FINSEQ_1, TARSKI;
equalities FINSEQ_1, XBOOLEAN;
theorems NAT_1, INT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_1, TARSKI, POWER,
FINSOP_1, XBOOLE_0, BINOP_2, XREAL_1, XXREAL_0, XBOOLEAN, FUNCOP_1,
PARTFUN1, FINSEQ_3, XREAL_0, NAT_D, CARD_1;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
begin
theorem Th1:
for i,n being Nat, D being non empty set, d being Element of D, z
being Tuple of n,D st i in Seg n holds (z^<*d*>)/.i=z/.i
proof
let i,n be Nat, D be non empty set, d be Element of D, z be Tuple of n,D
such that
A1: i in Seg n;
len z = n by CARD_1:def 7;
then i in dom z by A1,FINSEQ_1:def 3;
hence thesis by FINSEQ_4:68;
end;
theorem Th2:
for n being Nat, D being non empty set, d being Element of D, z
being Tuple of n,D holds (z^<*d*>)/.(n+1)=d
proof
let n be Nat, D be non empty set, d be Element of D, z be Tuple of n,D;
len<*d*> = 1 by FINSEQ_1:39;
then 0+1 in Seg len <*d*>;
then
A1: 0+1 in dom <*d*> by FINSEQ_1:def 3;
len(z) = n by CARD_1:def 7;
hence (z^<*d*>)/.(n+1) = <*d*>/.1 by A1,FINSEQ_4:69
.= d by FINSEQ_4:16;
end;
definition
let x, y be Element of BOOLEAN;
redefine func x 'or' y -> Element of BOOLEAN; :: redefines 'or' (XBOOLEAN, definition)
correctness
proof
x 'or' y = FALSE or x 'or' y = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
redefine func x 'xor' y -> Element of BOOLEAN; :: redefines 'xor' (XBOOLEAN, definition)
correctness
proof
x 'xor' y = FALSE or x 'xor' y = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
end;
reserve x,y,z for boolean object;
theorem
x 'or' FALSE = x;
theorem
'not' (x '&' y) = 'not' x 'or' 'not' y;
theorem
'not' (x 'or' y) = 'not' x '&' 'not' y;
theorem
x '&' y = 'not' ('not' x 'or' 'not' y);
theorem
TRUE 'xor' x = 'not' x;
theorem
FALSE 'xor' x = x;
theorem
x '&' x = x;
theorem
x 'or' TRUE = TRUE;
theorem
(x 'or' y) 'or' z = x 'or' (y 'or' z);
theorem
x 'or' x = x;
theorem
TRUE 'xor' FALSE = TRUE;
reserve i,j,k for Nat;
reserve n for non zero Nat;
reserve x,y,z1,z2 for Tuple of n, BOOLEAN;
definition
let n be Nat, x be Tuple of n, BOOLEAN;
func 'not' x -> Tuple of n, BOOLEAN means
for i st i in Seg n holds it/.i = 'not' (x/.i);
existence
proof
deffunc F(Nat) = 'not' (x/.$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;
reconsider z as Tuple of n, BOOLEAN by A1,CARD_1:def 7;
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
.= 'not' (x/.i) by A2,A3,A4;
end;
uniqueness
proof
let y, z be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds y/.i = 'not' (x/.i) and
A6: for i st i in Seg n holds z/.i = 'not' (x/.i);
A7: len y = n by CARD_1:def 7;
then
A8: dom y = Seg n by FINSEQ_1:def 3;
A9: len z = n by CARD_1:def 7;
now
let j be Nat;
assume
A10: j in dom y;
then
A11: j in dom z by A9,A8,FINSEQ_1:def 3;
thus y.j = y/.j by A10,PARTFUN1:def 6
.= 'not' (x/.j) by A5,A8,A10
.= z/.j by A6,A8,A10
.= z.j by A11,PARTFUN1:def 6;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
definition
let n be non zero Nat, x, y be Tuple of n, BOOLEAN;
func carry(x, y) -> Tuple of n, BOOLEAN means
:Def2:
it/.1 = FALSE & for i
being Nat st 1 <= i & i < n holds it/.(i+1) = (x/.i) '&' (y/.i) 'or' (x/.i) '&'
(it/.i) 'or' (y/.i) '&' (it/.i);
existence
proof
deffunc G(Nat,Element of BOOLEAN) = (x/.($1+1)) '&' (y/.($1+1)) 'or' (x/.(
$1+1)) '&' $2 'or' (y/.($1+1)) '&' $2;
consider f being sequence of BOOLEAN such that
A1: f.0 = FALSE and
A2: for i being Nat holds f.(i+1) = G(i,f.i) from NAT_1:sch 12;
deffunc F(Nat) = f.($1-1);
consider z being FinSequence such that
A3: len z = n and
A4: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_1:sch 2;
z is FinSequence of BOOLEAN
proof
let a be object;
assume a in rng z;
then consider b be object such that
A5: b in dom z and
A6: a = z.b by FUNCT_1:def 3;
A7: b in Seg n by A3,A5,FINSEQ_1:def 3;
reconsider b as Element of NAT by A5;
b>=1 by A7,FINSEQ_1:1;
then reconsider c = b-1 as Element of NAT by INT_1:5;
z.b = f.c by A4,A5;
hence thesis by A6;
end;
then reconsider z as Tuple of n, BOOLEAN by A3,CARD_1:def 7;
take z;
0+1 <= n by NAT_1:13;
then 1 in Seg n;
then
A8: 1 in dom z by A3,FINSEQ_1:def 3;
hence z/.1 = z.1 by PARTFUN1:def 6
.= f.(1-1) by A4,A8
.= FALSE by A1;
let i be Nat;
assume that
A9: 1 <= i and
A10: i < n;
consider j be Nat such that
A11: j+1 = i by A9,NAT_1:6;
j+1 in Seg n by A9,A10,A11;
then
A12: j+1 in dom z by A3,FINSEQ_1:def 3;
then
A13: z/.(j+1) = z.(j+1) by PARTFUN1:def 6
.= f.(j+1-1) by A4,A12
.= f.j;
A14: i+1-1=i;
1 <= i+1 & i+1 <= n by A9,A10,NAT_1:13;
then
A15: i + 1 in dom z by A3,FINSEQ_3:25;
hence z/.(i+1) = z.(i+1) by PARTFUN1:def 6
.= f.(j+1) by A4,A11,A14,A15
.= (x/.i) '&' (y/.i) 'or' (x/.i) '&' (z/.i) 'or' (y/.i) '&' (z/.i) by A2
,A11,A13;
end;
uniqueness
proof
let z1, z2 be Tuple of n, BOOLEAN such that
A16: z1/.1 = FALSE and
A17: for i being Nat st 1 <= i & i < n holds z1/.(i+1) = (x/.i) '&' (y
/.i) 'or' (x/.i) '&' (z1/.i) 'or' (y/.i) '&' (z1/.i) and
A18: z2/.1 = FALSE and
A19: for i being Nat st 1 <= i & i < n holds z2/.(i+1) = (x/.i) '&' (y
/.i) 'or' (x/.i) '&' (z2/.i) 'or' (y/.i) '&' (z2/.i);
A20: len z2 = n by CARD_1:def 7;
A21: len z1 = n by CARD_1:def 7;
then
A22: dom z1 = Seg n by FINSEQ_1:def 3;
now
defpred P[Nat] means $1 in Seg n implies z1/.$1 = z2/.$1;
A23: dom z1 = Seg n & dom z2 = Seg n by A21,A20,FINSEQ_1:def 3;
A24: now
let k such that
A25: P[k];
thus P[k+1]
proof
assume
A26: k+1 in Seg n;
per cases;
suppose
k = 0;
hence thesis by A16,A18;
end;
suppose
A27: k <> 0;
k+1 <= n & k < k+1 by A26,FINSEQ_1:1,XREAL_1:29;
then
A28: k < n by XXREAL_0:2;
A29: k >= 0+1 by A27,NAT_1:13;
hence
z1/.(k+1) = (x/.k) '&' (y/.k) 'or' (x/.k) '&' (z1/.k) 'or' (y
/.k) '&' (z1/.k) by A17,A28
.= z2/.(k+1) by A19,A25,A29,A28;
end;
end;
end;
A30: P[0] by FINSEQ_1:1;
A31: for k holds P[k] from NAT_1:sch 2 (A30,A24);
let j be Nat such that
A32: j in dom z1;
thus z1.j = z1/.j by A32,PARTFUN1:def 6
.= z2/.j by A22,A32,A31
.= z2.j by A32,A23,PARTFUN1:def 6;
end;
hence thesis by A21,A20,FINSEQ_2:9;
end;
end;
definition
let n be Nat, x be Tuple of n, BOOLEAN;
func Binary(x) -> Tuple of n, NAT means
:Def3:
for i st i in Seg n holds it /.i = IFEQ(x/.i,FALSE,0,2 to_power(i-'1));
existence
proof
deffunc F(Nat) = IFEQ( x/.$1,FALSE,0,2 to_power($1-'1));
consider z being FinSequence of NAT 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;
reconsider z as Tuple of n, NAT by A1,CARD_1:def 7;
take z;
let j;
assume
A4: j in Seg n;
then j in dom z by A1,FINSEQ_1:def 3;
hence z/.j = z.j by PARTFUN1:def 6
.= IFEQ(x/.j,FALSE,0,2 to_power(j-'1)) by A2,A3,A4;
end;
uniqueness
proof
let z1, z2 be Tuple of n, NAT such that
A5: for i st i in Seg n holds z1/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-' 1)) and
A6: for i st i in Seg n holds z2/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-' 1));
A7: len z1 = n by CARD_1:def 7;
then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
then
A10: dom z2 = Seg n by FINSEQ_1:def 3;
now
let j be Nat;
assume
A11: j in dom z1;
hence z1.j = z1/.j by PARTFUN1:def 6
.= IFEQ( x/.j,FALSE,0,2 to_power(j-'1)) by A5,A8,A11
.= z2/.j by A6,A8,A11
.= z2.j by A8,A10,A11,PARTFUN1:def 6;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
definition
let n be Nat, x be Tuple of n, BOOLEAN;
func Absval (x) -> Element of NAT equals
addnat $$ Binary (x);
correctness;
end;
definition
let n, x, y;
func x + y -> Tuple of n, BOOLEAN means
:Def5:
for i st i in Seg n holds it /.i = (x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i);
existence
proof
deffunc F(Nat) = (x/.$1) 'xor' (y/.$1) 'xor' (carry(x,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;
reconsider z as Tuple of n, BOOLEAN by A1,CARD_1:def 7;
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' (y/.i) 'xor' (carry(x,y)/.i) by A2,A3,A4;
end;
uniqueness
proof
let z1, z2 such that
A5: for i st i in Seg n holds z1/.i = (x/.i) 'xor' (y/.i) 'xor' (carry
(x,y)/.i) and
A6: for i st i in Seg n holds z2/.i = (x/.i) 'xor' (y/.i) 'xor' (carry
(x,y)/.i);
A7: len z1 = n by CARD_1:def 7;
then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
then
A10: dom z2 = Seg n by FINSEQ_1:def 3;
now
let j be Nat;
assume
A11: j in dom z1;
hence z1.j = z1/.j by PARTFUN1:def 6
.= (x/.j) 'xor' (y/.j) 'xor' (carry(x,y)/.j) by A5,A8,A11
.= z2/.j by A6,A8,A11
.= z2.j by A8,A10,A11,PARTFUN1:def 6;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
definition
let n,z1,z2;
func add_ovfl(z1,z2) -> Element of BOOLEAN equals
(z1/.n) '&' (z2/.n) 'or' (
z1/.n) '&' (carry(z1,z2)/.n) 'or' (z2/.n) '&' (carry(z1,z2)/.n);
correctness;
end;
definition
let n,z1,z2;
pred z1,z2 are_summable means
add_ovfl(z1,z2) = FALSE;
end;
theorem Th14:
for z1 being Tuple of 1,BOOLEAN holds z1= <*FALSE*> or z1=<*TRUE *>
proof
let z1 be Tuple of 1,BOOLEAN;
A1: ex B being Element of BOOLEAN st z1=<*B*> by FINSEQ_2:97;
per cases by XBOOLEAN:def 3;
suppose
z1/.1 = FALSE;
hence thesis by A1,FINSEQ_4:16;
end;
suppose
z1/.1 = TRUE;
hence thesis by A1,FINSEQ_4:16;
end;
end;
theorem Th15:
for z1 being Tuple of 1,BOOLEAN holds z1=<*FALSE*> implies Absval(z1) = 0
proof
let z1 be Tuple of 1,BOOLEAN;
A1: ex k being Element of NAT st Binary( z1 ) = <* k *> by FINSEQ_2:97;
assume z1=<*FALSE*>;
then
A2: z1/.1 = FALSE by FINSEQ_4:16;
1 in Seg 1;
then (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def3
.= 0 by A2,FUNCOP_1:def 8;
hence Absval(z1) = addnat $$ <* 0 *> by A1,FINSEQ_4:16
.= 0 by FINSOP_1:11;
end;
theorem Th16:
for z1 being Tuple of 1,BOOLEAN st z1=<*TRUE*> holds Absval(z1)= 1
proof
let z1 be Tuple of 1,BOOLEAN;
A1: 1 - 1 = 0;
assume z1=<*TRUE*>;
then
A2: z1/.1 <> FALSE by FINSEQ_4:16;
1 in Seg 1;
then
A3: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def3
.= 2 to_power(1-'1) by A2,FUNCOP_1:def 8;
ex k being Element of NAT st Binary( z1 ) = <* k *> by FINSEQ_2:97;
hence Absval(z1) = addnat $$ <* 2 to_power(1-'1) *> by A3,FINSEQ_4:16
.= 2 to_power(1-'1) by FINSOP_1:11
.= 2 to_power(0) by A1,XREAL_0:def 2
.= 1 by POWER:24;
end;
definition
let n1,n2 be Nat;
let D be non empty set;
let z1 be Tuple of n1,D;
let z2 be Tuple of n2,D;
redefine func z1 ^ z2 -> Tuple of n1+n2,D; :: redefines ^ (FINSEQ_1, definition)
coherence by FINSEQ_2:107;
end;
definition
let D be non empty set;
let d be Element of D;
redefine func <* d *> -> Tuple of 1,D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
<*d*> in 1-tuples_on D by FINSEQ_2:98;
hence thesis;
end;
end;
theorem Th17:
for z1,z2 being Tuple of n,BOOLEAN holds for d1,d2 being Element
of BOOLEAN holds for i being Nat holds i in Seg n implies carry(z1^<*d1*>,z2^<*
d2*>)/.i = carry(z1,z2)/.i
proof
let z1,z2 be Tuple of n,BOOLEAN;
let d1,d2 be Element of BOOLEAN;
defpred P[Nat] means $1 in Seg n implies carry(z1^<*d1*>,z2^<*d2*>)/.$1 =
carry(z1,z2)/.$1;
let i be Nat;
A1: for i being non zero Nat st P[i] holds P[i+1]
proof
let i be non zero Nat;
assume
A2: P[i];
assume i+1 in Seg n;
then i+1 > i & i+1 <= n by FINSEQ_1:1,XREAL_1:29;
then
A3: i < n by XXREAL_0:2;
n <= n+1 by NAT_1:11;
then
A4: i < n+1 by A3,XXREAL_0:2;
A5: 1 <= i by NAT_1:14;
then i in Seg n by A3;
then (z1^<*d1*>)/.i = z1/.i & (z2^<*d2*>)/.i = z2/.i by Th1;
hence
carry(z1^<*d1*>,z2^<*d2*>)/.(i+1) = ((z1/.i) '&' (z2/.i)) 'or' (z1/.i
) '&' (carry(z1,z2)/.i) 'or' (z2/.i) '&' (carry(z1,z2)/.i) by A2,A5,A3,A4
,Def2
.= carry(z1,z2)/.(i+1) by A5,A3,Def2;
end;
A6: P[1]
proof
assume 1 in Seg n;
thus carry(z1^<*d1*>,z2^<*d2*>)/.1 = FALSE by Def2
.= carry(z1,z2)/.1 by Def2;
end;
A7: for i being non zero Nat holds P[i] from NAT_1:sch 10(A6,A1);
assume
A8: i in Seg n;
then i is non zero by FINSEQ_1:1;
hence thesis by A8,A7;
end;
theorem Th18:
for z1,z2 being Tuple of n,BOOLEAN, d1,d2 being Element of
BOOLEAN holds add_ovfl(z1,z2) = carry(z1^<*d1*>,z2^<*d2*>)/.(n+1)
proof
let z1,z2 be Tuple of n,BOOLEAN, d1,d2 be Element of BOOLEAN;
A1: 1 <= n & n < n+1 by NAT_1:14,XREAL_1:29;
A2: n in Seg n by FINSEQ_1:3;
then
A3: z2/.n = (z2^<*d2*>)/.n by Th1;
carry(z1^<*d1*>,z2^<*d2*>)/.n = carry(z1,z2)/.n & z1/.n = (z1^<*d1*>)/.n
by A2,Th1,Th17;
hence thesis by A3,A1,Def2;
end;
theorem Th19:
for z1,z2 being Tuple of n,BOOLEAN, d1,d2 being Element of
BOOLEAN holds z1^<*d1*> + z2^<*d2*> = (z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,
z2)*>
proof
let z1,z2 be Tuple of n,BOOLEAN, d1,d2 be Element of BOOLEAN;
for i st i in Seg (n+1) holds ((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,
z2)*>)/.i = ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^
<*d2*>)/.i)
proof
A1: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:9;
let i such that
A2: i in Seg (n+1);
per cases by A2,A1,XBOOLE_0:def 3;
suppose
A3: i in Seg n;
hence ((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>)/.i = (z1+z2)/.i
by Th1
.= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Def5
.= ((z1^<*d1*>)/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Th1
.= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1,z2)/.i)
by A3,Th1
.= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2
^<*d2*>)/.i) by A3,Th17;
end;
suppose
i in {. n+1 .};
then
A4: i=n+1 by TARSKI:def 1;
hence (((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>)/.i) = d1 'xor' d2
'xor' add_ovfl(z1,z2) by Th2
.= d1 'xor' d2 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A4,Th18
.= d1 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i)
by A4,Th2
.= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2
^<*d2*>)/.i) by A4,Th2;
end;
end;
hence thesis by Def5;
end;
theorem Th20:
for z being Tuple of n,BOOLEAN, d being Element of BOOLEAN holds
Absval(z^<*d*>) = Absval(z)+IFEQ(d,FALSE,0,2 to_power n)
proof
let z be Tuple of n,BOOLEAN, d be Element of BOOLEAN;
for i st i in Seg (n+1) holds ((Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n)
)*>)/.i) = IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1))
proof
A1: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:9;
let i such that
A2: i in Seg (n+1);
per cases by A2,A1,XBOOLE_0:def 3;
suppose
A3: i in Seg n;
hence (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>)/.i = (Binary(z))/.i
by Th1
.= IFEQ(z/.i,FALSE,0,2 to_power(i-'1)) by A3,Def3
.= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A3,Th1;
end;
suppose
i in {. n+1 .};
then
A4: i=n+1 by TARSKI:def 1;
hence
(Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>)/.i = IFEQ(d,FALSE,0,2
to_power(n)) by Th2
.= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(n)) by A4,Th2
.= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A4,NAT_D:34;
end;
end;
hence Absval(z^<*d*>) = addnat $$ (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))
*>) by Def3
.= addnat.(addnat$$Binary(z),IFEQ(d,FALSE,0,2 to_power(n))) by FINSOP_1:4
.= Absval(z)+IFEQ(d,FALSE,0,2 to_power n) by BINOP_2:def 23;
end;
theorem Th21:
for n for z1,z2 being Tuple of n,BOOLEAN holds Absval(z1+z2) +
IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n)) = Absval(z1) + Absval(z2)
proof
defpred P[non zero Nat] means for z1,z2 being Tuple of $1, BOOLEAN holds
Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power $1) = Absval(z1) +
Absval(z2);
set f = FALSE, t = TRUE;
A1: for n being non zero Nat st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let z1,z2 be Tuple of n+1,BOOLEAN;
consider t1 being (Element of n-tuples_on BOOLEAN), d1 being Element of
BOOLEAN such that
A3: z1 = t1^<*d1*> by FINSEQ_2:117;
consider t2 being (Element of n-tuples_on BOOLEAN), d2 being Element of
BOOLEAN such that
A4: z2 = t2^<*d2*> by FINSEQ_2:117;
reconsider
C1= IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n+1)), C2= IFEQ(d1
'xor' d2 'xor' add_ovfl(t1,t2),FALSE,0,2 to_power n), C3= IFEQ(d1,FALSE,0,2
to_power n), C4= IFEQ(d2,FALSE,0,2 to_power n), C5= IFEQ(add_ovfl(t1,t2),FALSE,
0,2 to_power(n)) as Real;
A5: add_ovfl(z1,z2) = d1 '&' ((t2^<*d2*>)/.(n+1)) 'or' ((t1^<*d1*>)/.(n+1
)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' ((t2^<*d2*>)/.(n+1)) '&' (carry
(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by A3,A4,Th2
.= d1 '&' d2 'or' ((t1^<*d1*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)
/.(n+1)) 'or' ((t2^<*d2*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by
Th2
.= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' ((t2
^<*d2*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th2
.= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' d2
'&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th2
.= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' (carry(t1^<*d1*>,
t2^<*d2*>)/.(n+1)) by Th18
.= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2)
by Th18;
A6: C2 + C1 = C5 + C3 + C4
proof
now
per cases;
suppose
A7: d1=f;
then
A8: C3=0 by FUNCOP_1:def 8;
now
per cases;
suppose
A9: d2=f;
then C4=0 by FUNCOP_1:def 8;
hence thesis by A5,A7,A9,FUNCOP_1:def 8;
end;
suppose
A10: d2 <> f;
then
A11: C4=2 to_power n by FUNCOP_1:def 8;
now
per cases;
suppose
A12: add_ovfl(t1,t2)=f;
then C5=0 by FUNCOP_1:def 8;
hence thesis by A5,A7,A12,FUNCOP_1:def 8;
end;
suppose
A13: add_ovfl(t1,t2)<>f;
d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1
,t2) by A7,A10,XBOOLEAN:def 3
.= f by A13,XBOOLEAN:def 3;
then
A14: C2=0 by FUNCOP_1:def 8;
A15: C5=2 to_power(n) by A13,FUNCOP_1:def 8;
d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = f 'or' f 'or' t '&' add_ovfl(t1,t2) by A7,A10,XBOOLEAN:def 3
.= t by A13,XBOOLEAN:def 3;
then C1=2 to_power(n+1) by A5,FUNCOP_1:def 8;
hence C2 + C1 = 2 to_power n * 2 to_power 1 by A14,POWER:27
.= 2 * 2 to_power n by POWER:25
.= C5 + C3 + C4 by A8,A11,A15;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A16: d1 <>f;
then
A17: C3=2 to_power n by FUNCOP_1:def 8;
now
per cases;
suppose
A18: d2=f;
then
A19: C4=0 by FUNCOP_1:def 8;
now
per cases;
suppose
add_ovfl(t1,t2)=f;
hence thesis by A5,A18,A19,FUNCOP_1:def 8;
end;
suppose
A20: add_ovfl(t1,t2)<>f;
d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1
,t2) by A16,A18,XBOOLEAN:def 3
.= f by A20,XBOOLEAN:def 3;
then
A21: C2=0 by FUNCOP_1:def 8;
A22: C5=2 to_power(n) by A20,FUNCOP_1:def 8;
d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = f 'or' t '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) by
A16,A18,XBOOLEAN:def 3
.= f 'or' t '&' t 'or' d2 '&' add_ovfl(t1,t2) by A20,
XBOOLEAN:def 3
.= t;
then C1=2 to_power (n+1) by A5,FUNCOP_1:def 8;
hence C2 + C1 = 2 to_power n * 2 to_power 1 by A21,POWER:27
.= 2 * 2 to_power n by POWER:25
.= C5 + C3 + C4 by A17,A19,A22;
end;
end;
hence thesis;
end;
suppose
A23: d2<>f;
then
A24: C4=2 to_power n by FUNCOP_1:def 8;
now
per cases;
suppose
A25: add_ovfl(t1,t2)=f;
d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor'
add_ovfl(t1,t2) by A16,XBOOLEAN:def 3
.= f by A23,A25,XBOOLEAN:def 3;
then
A26: C2=0 by FUNCOP_1:def 8;
A27: C5=0 by A25,FUNCOP_1:def 8;
d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = t '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,
t2) by A16,XBOOLEAN:def 3
.= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) by A23,XBOOLEAN:def 3
.= t;
then C1=2 to_power (n+1) by A5,FUNCOP_1:def 8;
hence C2 + C1 = 2 to_power n * 2 to_power 1 by A26,POWER:27
.= 2 * 2 to_power n by POWER:25
.= C5 + C3 + C4 by A17,A24,A27;
end;
suppose
A28: add_ovfl(t1,t2)<>f;
d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor'
add_ovfl(t1,t2) by A16,XBOOLEAN:def 3
.= f 'xor' add_ovfl(t1,t2) by A23,XBOOLEAN:def 3
.= t by A28,XBOOLEAN:def 3;
then
A29: C2=2 to_power n by FUNCOP_1:def 8;
d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = t '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,
t2) by A16,XBOOLEAN:def 3
.= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) by A23,XBOOLEAN:def 3
.= t;
then C1=2 to_power (n+1) by A5,FUNCOP_1:def 8;
hence
C2 + C1 = 2 to_power n + 2 to_power n * 2 to_power 1 by A29,
POWER:27
.= 2 to_power n + 2 * 2 to_power n by POWER:25
.= 2 to_power n + 2 to_power n + 2 to_power n
.= C5 + C3 + C4 by A17,A24,A28,FUNCOP_1:def 8;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
thus Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n+1)) =
Absval((t1+t2)^<*d1 'xor' d2 'xor' add_ovfl(t1,t2)*>) + IFEQ(add_ovfl(z1,z2),
FALSE,0,2 to_power (n+1)) by A3,A4,Th19
.=Absval(t1+t2) + C2 + C1 by Th20
.= Absval(t1+t2) + C5 + C3 + C4 by A6
.= Absval(t1) + Absval(t2) + C3 + C4 by A2
.= Absval(t1) + C3 + (Absval(t2) + C4 )
.= Absval(t1)+IFEQ(d1,FALSE,0,2 to_power n) + Absval(t2^<*d2*>) by Th20
.= Absval(z1) + Absval(z2) by A3,A4,Th20;
end;
A30: P[1]
proof
reconsider T= <*t*>,F= <*f*> as Tuple of 1,BOOLEAN;
let z1,z2 be Tuple of 1, BOOLEAN;
A31: carry(z1,z2)/.1 = f by Def2;
A32: Absval(T)=1 by Th16;
A33: Absval(F)=0 by Th15;
per cases by Th14;
suppose
A34: z1=<*f*> & z2=<*f*>;
A35: now
let i;
assume
A36: i in Seg 1;
then
A37: i=1 by FINSEQ_1:2,TARSKI:def 1;
thus F/.i = (z1/.1) 'xor' f 'xor' f by A34,A36,FINSEQ_1:2,TARSKI:def 1
.= (z1/.1) 'xor' (z2/.1) 'xor' f by A34,FINSEQ_4:16
.= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A37,Def2;
end;
add_ovfl(z1,z2) = f by A31,A34,FINSEQ_4:16;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
hence thesis by A33,A34,A35,Def5;
end;
suppose
A38: z1=<*t*> & z2=<*f*>;
A39: now
let i;
assume
A40: i in Seg 1;
then
A41: i=1 by FINSEQ_1:2,TARSKI:def 1;
thus T/.i = (z1/.1) 'xor' f 'xor' f by A38,A40,FINSEQ_1:2,TARSKI:def 1
.= (z1/.1) 'xor' (z2/.1) 'xor' f by A38,FINSEQ_4:16
.= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A41,Def2;
end;
add_ovfl(z1,z2) = f by A31,A38,FINSEQ_4:16;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
hence thesis by A33,A38,A39,Def5;
end;
suppose
A42: z1=<*f*> & z2=<*t*>;
A43: now
let i;
assume i in Seg 1;
then
A44: i=1 by FINSEQ_1:2,TARSKI:def 1;
hence T/.i = 'not' t 'xor' t 'xor' f by FINSEQ_4:16
.= (z1/.1) 'xor' t 'xor' f by A42,FINSEQ_4:16
.= (z1/.1) 'xor' (z2/.1) 'xor' f by A42,FINSEQ_4:16
.= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A44,Def2;
end;
add_ovfl(z1,z2) = f by A31,A42,FINSEQ_4:16;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
hence thesis by A33,A42,A43,Def5;
end;
suppose
A45: z1=<*t*> & z2=<*t*>;
now
let i;
assume i in Seg 1;
then
A46: i=1 by FINSEQ_1:2,TARSKI:def 1;
hence F/.i = t 'xor' t 'xor' 'not' t by FINSEQ_4:16
.= (z1/.1) 'xor' t 'xor' f by A45,FINSEQ_4:16
.= (z1/.1) 'xor' (z2/.1) 'xor' f by A45,FINSEQ_4:16
.= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A46,Def2;
end;
then
A47: z1+z2=<*f*> by Def5;
add_ovfl(z1,z2) = t by A31,A45,FINSEQ_4:16;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 2 to_power 1 by
FUNCOP_1:def 8
.= 2 by POWER:25;
hence thesis by A32,A33,A45,A47;
end;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A30,A1);
end;
theorem
for z1,z2 being Tuple of n,BOOLEAN st z1,z2 are_summable holds Absval(
z1+z2) = Absval(z1) + Absval(z2)
proof
let z1,z2 be Tuple of n,BOOLEAN;
assume z1,z2 are_summable;
then add_ovfl(z1,z2) = FALSE;
then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n))=0 by FUNCOP_1:def 8;
hence
Absval(z1+z2) = Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n))
.= Absval(z1) + Absval(z2) by Th21;
end;