:: A Representation of Integers by Binary Arithmetics
:: and Addition of Integers
:: by Hisayoshi Kunimune and Yatsuka Nakamura
::
:: Received January 30, 2003
:: Copyright (c) 2003-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, XBOOLE_0, NAT_1, INT_1, XXREAL_0, CARD_1, RELAT_1,
ARYTM_3, POWER, EUCLID, FINSEQ_1, BINOP_2, ZFMISC_1, TARSKI, FUNCT_1,
FINSEQ_2, MARGREL1, BINARITH, ARYTM_1, SUBSET_1, PARTFUN1, XBOOLEAN,
BINARI_2, BINARI_3, FUNCOP_1, ORDINAL4, COMPLEX1, NEWTON, BINARI_4,
XCMPLX_0;
notations INT_1, SUBSET_1, XBOOLEAN, MARGREL1, FUNCOP_1, XCMPLX_0, POWER,
BINARITH, BINARI_2, BINARI_3, SERIES_1, ORDINAL1, NUMBERS, XXREAL_0,
XBOOLE_0, NAT_D, BINOP_2, EUCLID, TARSKI, PARTFUN1, FUNCT_1, RELAT_1,
ZFMISC_1, INT_2, FINSEQOP, NEWTON, FINSEQ_1, FINSEQ_2;
constructors REAL_1, NAT_D, FINSEQOP, NEWTON, SERIES_1, BINARITH, BINARI_2,
EUCLID, BINARI_3, RVSUM_1, RELSET_1, BINOP_2, TREES_3;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, XBOOLEAN,
MARGREL1, VALUED_0, FINSEQ_1, FINSEQ_2, RELAT_1, FUNCT_1, CARD_1,
XCMPLX_0, ORDINAL1;
requirements REAL, SUBSET, NUMERALS, ARITHM;
equalities FINSEQ_2, XBOOLEAN, EUCLID;
theorems POWER, NAT_1, PRE_FF, ABSVALUE, BINARI_3, INT_1, BINARITH, NAT_2,
BINARI_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCOP_1, RVSUM_1, FUNCT_2,
ZFMISC_1, EULER_2, PEPIN, PREPOWER, XREAL_1, XXREAL_0, XBOOLEAN, NAT_D,
VALUED_1, XREAL_0, CARD_1;
schemes NAT_1;
begin :: Preliminaries
reserve n for non zero Nat,
j,k,l,m for Nat,
g,h,i for Integer;
theorem Th1:
for m being Nat st m > 0 holds m * 2 >= m + 1
proof
let m be Nat;
assume m > 0;
then
A1: m >= 0 + 1 by INT_1:7;
m * 2 = m + m;
hence thesis by A1,XREAL_1:6;
end;
theorem Th2:
for m being Nat holds 2 to_power m >= m
proof
defpred P[Nat] means 2 to_power $1 >= $1;
A1: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A2: 2 to_power m >= m;
per cases;
suppose
A3: m = 0;
then 2 to_power (m+1) = 2 by POWER:25;
hence thesis by A3;
end;
suppose
A4: m > 0;
reconsider m2 = 2 to_power m as Nat;
m2 * 2 >= m * 2 & 2 to_power 1 = 2 by A2,NAT_1:4,POWER:25;
then
A5: 2 to_power (m+1) >= m * 2 by POWER:27;
m * 2 >= m + 1 by A4,Th1;
hence thesis by A5,XXREAL_0:2;
end;
end;
A6: P[0];
thus for m being Nat holds P[m] from NAT_1:sch 2(A6,A1);
end;
theorem
for m be Nat holds 0*m + 0*m = 0*m
proof
let m be Nat;
A1: dom(0*m) = Seg m by FUNCOP_1:13;
dom addreal = [:REAL,REAL:] & rng 0*m c= REAL by FINSEQ_1:def 4,FUNCT_2:def 1
;
then
A2: [:rng 0*m, rng 0*m:] c= dom addreal by ZFMISC_1:96;
A3: dom(0*m + 0*m) = dom(addreal.:(0*m,0*m)) by RVSUM_1:def 4
.= dom 0*m /\ dom 0*m by A2,FUNCOP_1:69
.= Seg m by FUNCOP_1:13;
for k be Nat st k in dom(0*m) holds (0*m).k = (0*m+0*m).k
proof
let k be Nat such that
A4: k in dom(0*m);
(0*m).k = 0;
then (0*m+0*m).k = 0 + 0 by A3,A1,A4,VALUED_1:def 1;
hence thesis;
end;
hence thesis by A3,FINSEQ_1:13,FUNCOP_1:13;
end;
theorem Th4:
for k,m,l be Nat holds k <= l & l <= m implies k = l or k + 1 <= l & l <= m
proof
defpred P[Nat] means for m,l be Nat holds $1 <= l & l <= m implies $1 = l or
($1 + 1 <= l & l <= m);
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
P[k];
let m,l be Nat;
assume that
A2: k+1 <= l and
A3: l <= m;
k+1 = l or k+1 < l by A2,XXREAL_0:1;
hence thesis by A3,NAT_1:13;
end;
A4: P[0] by NAT_1:13;
thus for k being Nat holds P[k] from NAT_1:sch 2(A4,A1);
end;
theorem Th5:
for n be non zero Nat holds for x,y be Tuple of n,BOOLEAN st x =
0*n & y = 0*n holds carry(x,y) = 0*n
proof
let n be non zero Nat;
let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n and
A2: y = 0*n;
A3: for j be Nat st 1 < j & j <= n holds carry(x,y).j = 0
proof
let j be Nat such that
A4: 1 < j and
A5: j <= n;
reconsider k = j - 1 as Element of NAT by A4,INT_1:5;
k + 1 = j;
then
A6: 1 <= k & k < n by A4,A5,NAT_1:13;
len(0*n) = n by CARD_1:def 7;
then
A7: x/.k = (0*n).k by A1,A6,FINSEQ_4:15
.= FALSE;
A8: j = k + 1;
len carry(x,y) = n by CARD_1:def 7;
then carry(x,y).j = carry(x,y)/.j by A4,A5,FINSEQ_4:15
.= FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.k) 'or' FALSE '&' (
carry(x,y)/.k) by A1,A2,A6,A8,A7,BINARITH:def 2
.= FALSE;
hence thesis;
end;
1 <= len carry(x,y) by NAT_1:14;
then
A9: carry(x,y).1 = carry(x,y)/.1 by FINSEQ_4:15
.= 0 by BINARITH:def 2;
for l be Nat st l in Seg n holds carry(x,y).l = (0*n).l
proof
let l be Nat such that
A10: l in Seg n;
A11: 1 <= l by A10,FINSEQ_1:1;
A12: (0*n).l = 0;
per cases by A10,A11,Th4,FINSEQ_1:1;
suppose
l = 1;
hence thesis by A9;
end;
suppose
A13: 1 + 1 <= l & l <= n;
then 1 < l by NAT_1:13;
hence thesis by A3,A12,A13;
end;
end;
hence thesis by A1,FINSEQ_2:119;
end;
theorem
for n be non zero Nat holds for x,y be Tuple of n,BOOLEAN st x = 0*n
& y = 0*n holds x + y = 0*n
proof
let n be non zero Nat;
let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n and
A2: y = 0*n;
for k be Nat st k in Seg n holds (x+y).k = (0*n).k
proof
let k be Nat such that
A3: k in Seg n;
reconsider k as Nat;
A4: (0*n).k = FALSE;
A5: 1 <= k by A3,FINSEQ_1:1;
len x = n by CARD_1:def 7;
then k <= len x by A3,FINSEQ_1:1;
then
A6: y/.k = FALSE by A1,A2,A4,A5,FINSEQ_4:15;
len carry(x,y) = n by CARD_1:def 7;
then k <= len carry(x,y) by A3,FINSEQ_1:1;
then
A7: carry(x,y)/.k = carry(x,y).k by A5,FINSEQ_4:15
.= FALSE by A1,A2,A4,Th5;
len(x+y) = n by CARD_1:def 7;
then k <= len(x+y) by A3,FINSEQ_1:1;
then (x+y).k = (x+y)/.k by A5,FINSEQ_4:15
.= FALSE 'xor' FALSE by A1,A2,A3,A6,A7,BINARITH:def 5
.= FALSE;
hence thesis;
end;
hence thesis by A1,FINSEQ_2:119;
end;
theorem
for n be non zero Nat for F be Tuple of n,BOOLEAN st F = 0*n holds
Intval F = 0
proof
let n be non zero Nat;
let F be Tuple of n,BOOLEAN such that
A1: F = 0*n;
A2: 1 <= n by NAT_1:14;
n <= len F by CARD_1:def 7;
then F/.n = F.n by A2,FINSEQ_4:15
.= FALSE by A1;
then Intval F = Absval F by BINARI_2:def 3;
hence thesis by A1,BINARI_3:6;
end;
theorem Th8:
l + m <= k - 1 implies l < k & m < k
proof
assume
A1: l + m <= k - 1;
then
A2: l + m - m <= k - 1 - m by XREAL_1:9;
k <= k + m by NAT_1:11;
then
A3: k - m <= k + m - m by XREAL_1:9;
k - 1 - m = k - m - 1;
then k - 1 - m < k by A3,XREAL_1:146,XXREAL_0:2;
hence l < k by A2,XXREAL_0:2;
k <= k + l by NAT_1:11;
then
A4: k - l <= k + l - l by XREAL_1:9;
A5: m + l - l <= k - 1 - l by A1,XREAL_1:9;
k - 1 - l = k - l - 1;
then k - 1 - l < k by A4,XREAL_1:146,XXREAL_0:2;
hence thesis by A5,XXREAL_0:2;
end;
theorem Th9:
g <= h + i & h < 0 & i < 0 implies g < h & g < i
proof
assume that
A1: g <= h + i and
A2: h < 0 and
A3: i < 0;
g - i <= h + i - i by A1,XREAL_1:9;
then i + (g + -i) < 0 + h by A3,XREAL_1:8;
hence g < h;
g - h <= i + h - h by A1,XREAL_1:9;
then h + (g + -h) < 0 + i by A2,XREAL_1:8;
hence thesis;
end;
theorem Th10:
l + m <= 2 to_power n - 1 implies add_ovfl(n-BinarySequence(l),n
-BinarySequence(m)) = FALSE
proof
set L = n-BinarySequence(l), M = n-BinarySequence(m);
A1: Absval(L+M) + 2 to_power n >= 2 to_power n by NAT_1:11;
assume
A2: l + m <= 2 to_power n - 1;
then
A3: l < 2 to_power n by Th8;
assume add_ovfl(L,M) <> FALSE;
then
A4: IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n) = 2 to_power n by FUNCOP_1:def 8;
A5: m < 2 to_power n by A2,Th8;
Absval(L+M) + IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n) = Absval(L)+
Absval(M) by BINARITH:21
.= l + Absval(M) by A3,BINARI_3:35
.= l + m by A5,BINARI_3:35;
hence contradiction by A2,A4,A1,XREAL_1:146,XXREAL_0:2;
end;
theorem Th11:
for n be non zero Nat, l,m be Nat st l + m <= 2 to_power n - 1
holds Absval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m
proof
let n be non zero Nat, l,m be Nat such that
A1: l + m <= 2 to_power n - 1;
A2: l < 2 to_power n by A1,Th8;
set L = n-BinarySequence(l), M = n-BinarySequence(m);
add_ovfl(L,M) = FALSE by A1,Th10;
then L,M are_summable by BINARITH:def 7;
then
A3: Absval(L+M) = Absval(L) + Absval(M) by BINARITH:22
.= l + Absval(M) by A2,BINARI_3:35;
m < 2 to_power n by A1,Th8;
hence thesis by A3,BINARI_3:35;
end;
theorem Th12:
for n be non zero Nat holds for z be Tuple of n,BOOLEAN st z/.n
= TRUE holds Absval(z) >= 2 to_power (n-'1)
proof
defpred P[Nat] means (for z be Tuple of $1,BOOLEAN st z/.$1 = TRUE holds
Absval(z) >= 2 to_power ($1-'1));
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat such that
P[n];
let z be Tuple of (n+1),BOOLEAN such that
A2: z/.(n+1) = TRUE;
consider x be Element of n-tuples_on BOOLEAN, a be Element of BOOLEAN
such that
A3: z = x^<*a*> by FINSEQ_2:117;
A4: n + 1 >= 1 by NAT_1:11;
then n + 1 - 1 >= 1 - 1 by XREAL_1:9;
then
A5: n + 1 -' 1 = n by XREAL_0:def 2;
len z = n+1 by CARD_1:def 7;
then
A6: z/.(n+1) = (x^<*a*>).(n+1) by A3,A4,FINSEQ_4:15
.= a by FINSEQ_2:116;
Absval(z) = Absval(x) + IFEQ(a,FALSE,0,2 to_power n) by A3,BINARITH:20
.= Absval(x) + 2 to_power n by A2,A6,FUNCOP_1:def 8;
hence thesis by A5,NAT_1:11;
end;
A7: P[1]
proof
let z be Tuple of 1,BOOLEAN such that
A8: z/.1 = TRUE;
A9: len z = 1 by CARD_1:def 7;
then z.1 = z/.1 by FINSEQ_4:15;
then z = <*TRUE*> by A8,A9,FINSEQ_1:40;
then
A10: Absval(z) = 1 by BINARITH:16;
2 to_power (1-'1) = 2 to_power (1-1) by XREAL_0:def 2;
hence thesis by A10,POWER:24;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A7,A1);
end;
theorem Th13:
l + m <= 2 to_power (n-'1) - 1 implies carry(n-BinarySequence(l)
,n-BinarySequence(m))/.n = FALSE
proof
set L = n-BinarySequence(l), M = n-BinarySequence(m), F = FALSE, T = TRUE;
assume
A1: l + m <= 2 to_power (n-'1) - 1;
then
A2: l < 2 to_power (n-'1) by Th8;
n >= 1 by NAT_1:14;
then n-1 >= 1-1 by XREAL_1:9;
then n-'1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n-'1) < 2 to_power n by POWER:39,XREAL_1:146;
then
A3: 2 to_power (n-'1) - 1 < 2 to_power n - 1 by XREAL_1:14;
assume not carry(L,M)/.n = F;
then
A4: carry(L,M)/.n = T by XBOOLEAN:def 3;
A5: m < 2 to_power (n-'1) by A1,Th8;
1 <= n by NAT_1:14;
then
A6: n in Seg n by FINSEQ_1:1;
then
A7: M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A5,NAT_D:27
.= IFEQ(0,0,F,T) by NAT_D:26
.= F by FUNCOP_1:def 8;
L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by A6,BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A2,NAT_D:27
.= IFEQ(0,0,F,T) by NAT_D:26
.= F by FUNCOP_1:def 8;
then (L+M)/.n = F 'xor' F 'xor' T by A4,A6,A7,BINARITH:def 5
.= T;
then
A8: Absval(L+M) >= 2 to_power (n-'1) by Th12;
l + m < 2 to_power (n-'1) by A1,XREAL_1:146,XXREAL_0:2;
hence contradiction by A1,A3,A8,Th11,XXREAL_0:2;
end;
theorem Th14:
for n be non zero Nat st l + m <= 2 to_power (n-'1) - 1 holds
Intval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m
proof
let n be non zero Nat such that
A1: l + m <= 2 to_power (n-'1) - 1;
A2: l < 2 to_power (n-'1) by A1,Th8;
set L = n-BinarySequence(l), M = n-BinarySequence(m), F = FALSE, T = TRUE;
n >= 1 by NAT_1:14;
then n-1 >= 1-1 by XREAL_1:9;
then n-'1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n-'1) < 2 to_power n by POWER:39,XREAL_1:146;
then
A3: 2 to_power (n-'1) - 1 < 2 to_power n - 1 by XREAL_1:14;
A4: m < 2 to_power (n-'1) by A1,Th8;
1 <= n by NAT_1:14;
then
A5: n in Seg n by FINSEQ_1:1;
then
A6: M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A4,NAT_D:27
.= IFEQ(0,0,F,T) by NAT_D:26
.= F by FUNCOP_1:def 8;
L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by A5,BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A2,NAT_D:27
.= IFEQ(0,0,F,T) by NAT_D:26
.= F by FUNCOP_1:def 8;
then (L+M)/.n = F 'xor' F 'xor' (carry(L,M)/.n) by A5,A6,BINARITH:def 5
.= F by A1,Th13;
then Intval(L+M) = Absval(L+M) by BINARI_2:def 3;
hence thesis by A1,A3,Th11,XXREAL_0:2;
end;
theorem Th15:
for z be Tuple of 1,BOOLEAN st z=<*TRUE*> holds Intval(z) = -1
proof
let z be Tuple of 1,BOOLEAN such that
A1: z = <*TRUE*>;
len z = 1 by CARD_1:def 7;
then z/.1 = z.1 by FINSEQ_4:15
.= TRUE by A1;
then Intval(z) = Absval(z) - 2 to_power 1 by BINARI_2:def 3
.= 1 - 2 to_power 1 by A1,BINARITH:16
.= 1 - (1 + 1) by POWER:25
.= 0 - 1;
hence thesis;
end;
theorem
for z be Tuple of 1,BOOLEAN st z=<*FALSE*> holds Intval(z) = 0
proof
let z be Tuple of 1,BOOLEAN such that
A1: z = <*FALSE*>;
len z = 1 by CARD_1:def 7;
then z/.1 = z.1 by FINSEQ_4:15
.= FALSE by A1;
then Intval(z) = Absval(z) by BINARI_2:def 3;
hence thesis by A1,BINARITH:15;
end;
theorem
for x be boolean object holds TRUE 'or' x = TRUE;
theorem
for n be non zero Nat holds 0 <= 2 to_power (n-'1) - 1 & -(2 to_power
(n-'1)) <= 0
proof
defpred P[Nat] means 0 <= 2 to_power ($1-'1) - 1 & -(2 to_power ($1-'1)) <=
0;
A1: for k be non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat such that
A2: 0 <= 2 to_power (k-'1) - 1 and
-(2 to_power (k-'1)) <= 0;
(k+1)-'1 = k by NAT_D:34;
then 2 to_power (k-'1) < 2 to_power ((k+1)-'1) by NAT_2:9,POWER:39;
hence thesis by A2,XREAL_1:9;
end;
1 - 1 = 0;
then 2 to_power (1-'1) = 2 to_power 0 by XREAL_0:def 2
.= 1 by POWER:24;
then
A3: P[1];
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A3,A1);
end;
theorem
for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds x,y are_summable
proof
let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n and
A2: y = 0*n;
A3: 1 <= n by NAT_1:14;
len x = n by CARD_1:def 7;
then x/.n = (0*n).n by A1,A3,FINSEQ_4:15
.= FALSE;
then add_ovfl(x,y) = FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.n) 'or'
FALSE '&' (carry(x,y)/.n) by A1,A2,BINARITH:def 6
.= FALSE;
hence thesis by BINARITH:def 7;
end;
theorem Th20:
(i*n) mod n = 0;
begin :: Majorant Power
definition
let m, j be Nat;
func MajP(m, j) -> Nat means
:Def1:
2 to_power it >= j & it >= m & for k be
Nat st 2 to_power k >= j & k >= m holds k >= it;
existence
proof
per cases;
suppose
A1: 2 to_power m >= j;
for k be Nat st 2 to_power k >= j & k >= m holds k >= m;
hence thesis by A1;
end;
suppose
A2: 2 to_power m < j;
defpred P[Nat] means 2 to_power $1 >= j & $1 >= m;
2 to_power m >= m by Th2;
then
A3: j >= m by A2,XXREAL_0:2;
2 to_power j >= j by Th2;
then
A4: ex k be Nat st P[k] by A3;
ex k be Nat st P[k] & for l be Nat st P[l] holds l >= k from NAT_1:
sch 5(A4);
hence thesis;
end;
end;
uniqueness
proof
let p, q be Nat;
assume 2 to_power p >= j & p >= m & ( for k be Nat st 2 to_power k >= j &
k >= m holds k >= p)& 2 to_power q >= j &( q >= m & for k be Nat st 2 to_power
k >= j & k >= m holds k >= q );
then p >= q & q >= p;
hence thesis by XXREAL_0:1;
end;
end;
theorem
j >= k implies MajP(m, j) >= MajP(m, k)
proof
assume
A1: j >= k;
A2: MajP(m, j) >= m by Def1;
2 to_power MajP(m, j) >= j by Def1;
then 2 to_power MajP(m, j) >= k by A1,XXREAL_0:2;
hence thesis by A2,Def1;
end;
theorem Th22:
l >= m implies MajP(l,j) >= MajP(m,j)
proof
assume
A1: l >= m;
A2: 2 to_power MajP(l,j) >= j by Def1;
MajP(l,j) >= l by Def1;
then MajP(l,j) >= m by A1,XXREAL_0:2;
hence thesis by A2,Def1;
end;
theorem
m >= 1 implies MajP(m, 1) = m
proof
assume m >= 1;
then
A1: 2 to_power m >= 1 by POWER:35;
for k be Nat st 2 to_power k >= 1 & k >= m holds k >= m;
hence thesis by A1,Def1;
end;
theorem Th24:
j <= 2 to_power m implies MajP(m, j) = m
proof
A1: for k be Nat st 2 to_power k >= j & k >= m holds k >= m;
assume j <= 2 to_power m;
hence thesis by A1,Def1;
end;
theorem
j > 2 to_power m implies MajP(m, j) > m
proof
assume
A1: j > 2 to_power m;
2 to_power MajP(m, j) >= j by Def1;
then 2 to_power MajP(m, j) > 2 to_power m by A1,XXREAL_0:2;
hence thesis by PRE_FF:8;
end;
begin :: 2's Complement
definition
let m be Nat;
let i be Integer;
func 2sComplement( m, i ) -> Tuple of m, BOOLEAN equals
:Def2:
m
-BinarySequence( |.(2 to_power MajP(m,|.i.|)) + i .| ) if i < 0 otherwise m
-BinarySequence( |.i.| );
correctness;
end;
theorem
for m be Nat holds 2sComplement(m,0) = 0*m
proof
let m be Nat;
2sComplement(m,0) = m-BinarySequence |.0.| by Def2
.= m-BinarySequence(0) by ABSVALUE:2;
hence thesis by BINARI_3:25;
end;
theorem
for i be Integer st i <= 2 to_power (n-'1) - 1 & -(2 to_power (n-'1))
<= i holds Intval( 2sComplement( n, i ) ) = i
proof
let i such that
A1: i <= 2 to_power (n-'1) - 1 and
A2: -(2 to_power (n-'1)) <= i;
A3: n >= 1 by NAT_1:14;
now
per cases;
suppose
i >= 0;
then reconsider i as Element of NAT by INT_1:3;
A4: 2sComplement(n,i) = n-BinarySequence(|.i.|) by Def2
.= n-BinarySequence(i) by ABSVALUE:def 1;
i + 1 <= 2 to_power (n-'1) - 1 + 1 by A1,XREAL_1:6;
then
A5: i < 2 to_power (n-'1) by NAT_1:13;
n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n-'1 = n - 1 by XREAL_0:def 2;
then 2 to_power (n-'1) < 2 to_power n by POWER:39,XREAL_1:146;
then i < 2 to_power n by A5,XXREAL_0:2;
then
A6: Absval(n-BinarySequence i) = i by BINARI_3:35;
1 <= n by NAT_1:14;
then n in Seg n by FINSEQ_1:1;
then (n-BinarySequence i)/.n = IFEQ((i div 2 to_power (n-'1)) mod 2,0,
FALSE,TRUE) by BINARI_3:def 1
.= IFEQ(0 mod 2,0,FALSE,TRUE) by A5,NAT_D:27
.= IFEQ(0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def 8;
hence thesis by A4,A6,BINARI_2:def 3;
end;
suppose
A7: i < 0;
A8: 2 to_power n >= 2 to_power (n-'1) by NAT_2:9,POWER:39;
then -(2 to_power n) <= -(2 to_power (n-'1)) by XREAL_1:24;
then -(2 to_power n) <= i by A2,XXREAL_0:2;
then -(2 to_power n) - i <= i-i by XREAL_1:9;
then -(2 to_power n + i) <= 0;
then 2 to_power n + i >= -0;
then reconsider k = 2 to_power n + i as Element of NAT by INT_1:3;
|.i.| = -i by A7,ABSVALUE:def 1;
then |.i.| <= --2 to_power (n-'1) by A2,XREAL_1:24;
then MajP(n,|.i.|) = n by A8,Th24,XXREAL_0:2;
then
A9: 2sComplement(n,i) = n-BinarySequence(|.k.|) by A7,Def2
.= n-BinarySequence(k) by ABSVALUE:def 1;
k < 2 to_power n + 0 by A7,XREAL_1:8;
then k < (2 to_power 1) * (2 to_power (n-'1)) by NAT_1:14,NAT_2:10;
then k < 2*(2 to_power (n-'1)) by POWER:25;
then
A10: k < 2 to_power (n-'1) + (2 to_power (n-'1));
A11: 2 to_power n + i < 2 to_power n + 0 by A7,XREAL_1:6;
2 to_power n + -(2 to_power (n-'1)) = 2 to_power n - (2 to_power (n -'1))
.= (2 to_power 1) * (2 to_power (n-'1)) - (2 to_power (n-'1)) by
NAT_1:14,NAT_2:10
.= 2*(2 to_power (n-'1)) - (2 to_power (n-'1)) by POWER:25
.= 2 to_power (n-'1);
then
A12: k >= 2 to_power (n-'1) by A2,XREAL_1:6;
n in Seg n by A3,FINSEQ_1:1;
then (n-BinarySequence(k))/.n = IFEQ((k div 2 to_power (n-'1)) mod 2,0,
FALSE,TRUE) by BINARI_3:def 1
.= IFEQ(1 mod 2,0,FALSE,TRUE) by A12,A10,NAT_2:20
.= IFEQ(1,0,FALSE,TRUE) by NAT_D:14
.= TRUE by FUNCOP_1:def 8;
then Intval(2sComplement(n,i)) = Absval(n-BinarySequence(k)) - 2
to_power n by A9,BINARI_2:def 3
.= k - 2 to_power n by A11,BINARI_3:35
.= 0 + i;
hence thesis;
end;
end;
hence thesis;
end;
Lm1: k mod n = l mod n & k > l implies ex s be Integer st k = l + s*n
proof
assume that
A1: k mod n = l mod n and
A2: k > l;
consider m be Nat such that
A3: k = l + m by A2,NAT_1:10;
take m div n;
l = (l div n)*n + (l mod n) & k = (k div n)*n + (l mod n) by A1,NAT_D:2;
then m mod n = (((k div n) - (l div n))*n) mod n by A3
.= 0;
then (l+m) div n = (l div n) + (m div n) by NAT_D:19;
then k = ((l div n) + (m div n))*n + (l mod n) by A1,A3,NAT_D:2
.= (m div n)*n + ((l div n)*n + (l mod n))
.= (m div n)*n + l by NAT_D:2;
hence thesis;
end;
Lm2: k mod n = l mod n implies ex s be Integer st k = l + s*n
proof
assume
A1: k mod n = l mod n;
now
per cases by XXREAL_0:1;
suppose
A2: k = l;
set s = 0;
k = l + s*n by A2;
hence thesis;
end;
suppose
A3: k > l or l > k;
now
per cases by A3;
suppose
k > l;
hence thesis by A1,Lm1;
end;
suppose
k < l;
then consider t be Integer such that
A4: l = k + t*n by A1,Lm1;
k = l + (-t)*n by A4;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
Lm3: for k,l,m be Nat st m < n & k mod 2 to_power n = l mod 2 to_power n holds
(k div 2 to_power m) mod 2 = (l div 2 to_power m) mod 2
proof
let k,l,m be Nat such that
A1: m < n and
A2: k mod 2 to_power n = l mod 2 to_power n;
consider j be Nat such that
A3: n = m + j by A1,NAT_1:10;
2 to_power n = 2 |^ n by POWER:41;
then 2 to_power n is non zero by PREPOWER:5;
then consider s be Integer such that
A4: k = l + s*(2 to_power n) by A2,Lm2;
reconsider j as Nat;
set M = 2 to_power m, J = 2 to_power j;
m + -m < n + -m by A1,XREAL_1:8;
then 0 + 1 < j + 1 by A3,XREAL_1:8;
then 1 <= j by NAT_1:13;
then 2 to_power 1 divides 2 to_power j by NAT_2:11;
then 2 divides 2 to_power j by POWER:25;
then J mod 2 = 0 by PEPIN:6;
then
A5: (s*J) mod 2 = ((s mod 2) * 0) mod 2 by NAT_D:67
.= 0 by NAT_D:26;
reconsider L = l as Integer;
A6: M > 0 by POWER:34;
k div M = (l + s*(J*M)) div M by A4,A3,POWER:27
.= (l + s*J*M) div M
.= (l div M) + s*J by A6,NAT_D:61;
then (k div M) mod 2 = ((L div M) mod 2 + 0) mod 2 by A5,NAT_D:66
.= (L div M) mod 2 by NAT_D:65;
hence thesis;
end;
Lm4: for h,i be Integer st h mod 2 to_power n = i mod 2 to_power n holds ((2
to_power MajP(n,|.h.|))+h) mod 2 to_power n = ((2 to_power MajP(n,|.i.|))+i)
mod 2 to_power n
proof
let h,i be Integer such that
A1: h mod 2 to_power n = i mod 2 to_power n;
n <= MajP(n,|.i.|) by Def1;
then consider y be Nat such that
A2: MajP(n,|.i.|) = n + y by NAT_1:10;
reconsider L = 2 to_power MajP(n,|.i.|) as Integer;
reconsider M = 2 to_power MajP(n,|.h.|) as Integer;
n <= MajP(n,|.h.|) by Def1;
then consider x be Nat such that
A3: MajP(n,|.h.|) = n + x by NAT_1:10;
reconsider x as Nat;
M = (2 to_power n)*(2 to_power x) by A3,POWER:27;
then
A4: M mod 2 to_power n = (((2 to_power n) mod (2 to_power n)) * (2 to_power
x)) mod 2 to_power n by EULER_2:8
.= (0 * (2 to_power x)) mod 2 to_power n by NAT_D:25
.= 0 by NAT_D:26;
reconsider y as Nat;
L = (2 to_power n)*(2 to_power y) by A2,POWER:27;
then
A5: L mod 2 to_power n = (((2 to_power n) mod (2 to_power n)) * (2 to_power
y)) mod 2 to_power n by EULER_2:8
.= (0 * (2 to_power y)) mod 2 to_power n by NAT_D:25
.= 0 by NAT_D:26;
A6: (L + i) mod 2 to_power n = ((L mod 2 to_power n)+(i mod 2 to_power n))
mod 2 to_power n by NAT_D:66
.= (i mod 2 to_power n) mod 2 to_power n by A5;
(M + h) mod 2 to_power n = ((M mod 2 to_power n)+(h mod 2 to_power n))
mod 2 to_power n by NAT_D:66
.= (h mod 2 to_power n) mod 2 to_power n by A4;
hence thesis by A1,A6;
end;
Lm5: for h,i be Integer st h >= 0 & i >= 0 & h mod 2 to_power n = i mod 2
to_power n holds 2sComplement(n,h) = 2sComplement(n,i)
proof
let h,i be Integer such that
A1: h >= 0 & i >= 0 and
A2: h mod 2 to_power n = i mod 2 to_power n;
A3: for j be Nat st j in Seg n holds (n-BinarySequence(|.h.|)).j = (n
-BinarySequence(|.i.|)).j
proof
A4: |.h.| = h & |.i.| = i by A1,ABSVALUE:def 1;
let j be Nat such that
A5: j in Seg n;
reconsider j as Nat;
A6: j <= n by A5,FINSEQ_1:1;
A7: 1 <= j by A5,FINSEQ_1:1;
then j - 1 >= 1 - 1 by XREAL_1:9;
then j-'1 = j - 1 by XREAL_0:def 2;
then
A8: j-'1 < n by A6,XREAL_1:146,XXREAL_0:2;
len(n-BinarySequence(|.i.|)) = n by CARD_1:def 7;
then
A9: (n-BinarySequence(|.i.|)).j = (n-BinarySequence(|.i.|))/.j by A7,A6,
FINSEQ_4:15
.= IFEQ((|.i.| div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A5,
BINARI_3:def 1;
len(n-BinarySequence(|.h.|)) = n by CARD_1:def 7;
then
(n-BinarySequence(|.h.|)).j = (n-BinarySequence(|.h.|))/.j by A7,A6,
FINSEQ_4:15
.= IFEQ((|.h.| div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A5,
BINARI_3:def 1
.= IFEQ((|.i.| div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,A8,A4
,Lm3;
hence thesis by A9;
end;
2sComplement(n,h) = n-BinarySequence(|.h.|) & 2sComplement(n,i) = n
-BinarySequence(|.i.|) by A1,Def2;
hence thesis by A3,FINSEQ_2:119;
end;
Lm6: for h,i be Integer st h < 0 & i < 0 & h mod 2 to_power n = i mod 2
to_power n holds 2sComplement(n,h) = 2sComplement(n,i)
proof
let h,i be Integer such that
A1: h < 0 and
A2: i < 0 and
A3: h mod 2 to_power n = i mod 2 to_power n;
|.i.| = -i by A2,ABSVALUE:def 1;
then 2 to_power MajP(n,|.i.|) >= -i by Def1;
then 2 to_power MajP(n,|.i.|) + i >= -i+i by XREAL_1:6;
then reconsider I = 2 to_power MajP(n,|.i.|) + i as Element of NAT by INT_1:3
;
|.h.| = -h by A1,ABSVALUE:def 1;
then 2 to_power MajP(n,|.h.|) >= -h by Def1;
then 2 to_power MajP(n,|.h.|) + h >= -h+h by XREAL_1:6;
then reconsider H = 2 to_power MajP(n,|.h.|) + h as Element of NAT by INT_1:3
;
A4: (H qua Nat) mod (2 to_power n) = (I qua Nat) mod (2 to_power n) by A3,Lm4;
A5: for j be Nat st j in Seg n holds (n-BinarySequence(|.H.|)).j = (n
-BinarySequence(|.I.|)).j
proof
A6: len(n-BinarySequence(I)) = n by CARD_1:def 7;
let j be Nat such that
A7: j in Seg n;
A8: 1 <= j by A7,FINSEQ_1:1;
A9: j <= n by A7,FINSEQ_1:1;
reconsider j as Nat;
j - 1 >= 1 - 1 by A8,XREAL_1:9;
then j-'1 = j - 1 by XREAL_0:def 2;
then
A10: j-'1 < n by A9,XREAL_1:146,XXREAL_0:2;
len(n-BinarySequence(H)) = n & |.H.| = H by ABSVALUE:def 1,CARD_1:def 7;
then
(n-BinarySequence(|.H.|)).j = (n-BinarySequence(H))/.j by A8,A9,FINSEQ_4:15
.= IFEQ((H div (2 to_power (j-'1))) mod 2,0,FALSE,TRUE) by A7,
BINARI_3:def 1
.= IFEQ((I div (2 to_power (j-'1))) mod 2,0,FALSE,TRUE) by A4,A10,Lm3
.= (n-BinarySequence(I))/.j by A7,BINARI_3:def 1
.= (n-BinarySequence(I)).j by A8,A9,A6,FINSEQ_4:15;
hence thesis by ABSVALUE:def 1;
end;
2sComplement(n,h) = n-BinarySequence(|.(2 to_power MajP(n,|.h.|))+h.|)
& 2sComplement(n,i) = n-BinarySequence(|.(2 to_power MajP(n,|.i.|))+i.|)
by A1,A2,Def2;
hence thesis by A5,FINSEQ_2:119;
end;
theorem
for h,i be Integer st ( h >= 0 & i >= 0 or h < 0 & i < 0 ) & h mod 2
to_power n = i mod 2 to_power n holds 2sComplement(n,h) = 2sComplement(n,i) by
Lm5,Lm6;
theorem
for h,i be Integer st ( h >= 0 & i >= 0 or h < 0 & i < 0 ) & h,i
are_congruent_mod 2 to_power n holds 2sComplement(n,h) = 2sComplement(n,i)
proof
let h,i be Integer such that
A1: h >= 0 & i >= 0 or h < 0 & i < 0 and
A2: h,i are_congruent_mod 2 to_power n;
h mod 2 to_power n = i mod 2 to_power n by A2,NAT_D:64;
hence thesis by A1,Lm5,Lm6;
end;
theorem Th30:
for l,m be Nat st l mod 2 to_power n = m mod 2 to_power n holds
n-BinarySequence(l) = n-BinarySequence(m)
proof
let l,m be Nat such that
A1: l mod 2 to_power n = m mod 2 to_power n;
|.m.| = m by ABSVALUE:def 1;
then
A2: 2sComplement(n,m) = n-BinarySequence(m) by Def2;
|.l.| = l by ABSVALUE:def 1;
then 2sComplement(n,l) = n-BinarySequence(l) by Def2;
hence thesis by A1,A2,Lm5;
end;
theorem
for l,m be Nat st l,m are_congruent_mod 2 to_power n holds n
-BinarySequence(l) = n-BinarySequence(m)
proof
let l,m be Nat;
assume l,m are_congruent_mod 2 to_power n;
then (l qua Integer) mod 2 to_power n = (m qua Integer) mod 2 to_power n by
NAT_D:64;
hence thesis by Th30;
end;
theorem Th32:
for j be Nat st 1 <= j & j <= n holds 2sComplement(n+1,i)/.j =
2sComplement(n,i)/.j
proof
let j be Nat such that
A1: 1 <= j and
A2: j <= n;
A3: j in Seg n by A1,A2,FINSEQ_1:1;
n <= n+1 by NAT_1:11;
then j <= n+1 by A2,XXREAL_0:2;
then
A4: j in Seg (n+1) by A1,FINSEQ_1:1;
set N = |. (2 to_power MajP(n,|.i.|)) + i .|;
set M = |. (2 to_power MajP(n+1,|.i.|)) + i .|;
A5: i < 0 implies (M div 2 to_power (j-'1)) mod 2 = (N div 2 to_power (j-'1)
) mod 2
proof
MajP(n+1,|.i.|) >= MajP(n,|.i.|) by Th22,NAT_1:11;
then consider m be Nat such that
A6: MajP(n+1,|.i.|) = MajP(n,|.i.|) + m by NAT_1:10;
reconsider m as Nat;
set P = MajP(n,|.i.|);
assume
A7: i < 0;
set Q = 2 to_power P;
A8: (Q * 2 to_power m qua Integer) mod Q = 0;
2 to_power (MajP(n+1,|.i.|)) >= |.i.| by Def1;
then 2 to_power (MajP(n+1,|.i.|)) >= -i by A7,ABSVALUE:def 1;
then 2 to_power (MajP(n+1,|.i.|)) + i >= -i + i by XREAL_1:6;
then M = 2 to_power (P+m) + i by A6,ABSVALUE:def 1
.= (Q * 2 to_power m)+i by POWER:27;
then
A9: M mod Q = (((Q * 2 to_power m qua Integer) mod Q) + (i mod Q)) mod Q
by NAT_D:66
.= (i mod Q) mod Q;
A10: (Q qua Integer) mod Q = 0 by NAT_D:25;
j + -1 >= 1 + -1 by A1,XREAL_1:6;
then j -' 1 = j - 1 by XREAL_0:def 2;
then
A11: j -' 1 < n by A2,XREAL_1:146,XXREAL_0:2;
P >= n by Def1;
then
A12: j -' 1 < P by A11,XXREAL_0:2;
Q >= |.i.| by Def1;
then Q >= -i by A7,ABSVALUE:def 1;
then Q + i >= -i + i by XREAL_1:6;
then N = Q + i by ABSVALUE:def 1;
then N mod Q = (((Q qua Integer) mod Q) + (i mod Q)) mod Q by NAT_D:66
.= (i mod Q) mod Q by A10;
hence thesis by A9,A12,Lm3;
end;
per cases;
suppose
i >= 0;
then reconsider i as Element of NAT by INT_1:3;
A13: 2sComplement(n,i)/.j = (n-BinarySequence(|.i.|))/.j by Def2
.= (n-BinarySequence(i))/.j by ABSVALUE:def 1
.= IFEQ((i div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A3,
BINARI_3:def 1;
2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(|.i.|))/.j by Def2
.= ((n+1)-BinarySequence(i))/.j by ABSVALUE:def 1
.= IFEQ((i div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A4,
BINARI_3:def 1;
hence thesis by A13;
end;
suppose
A14: i < 0;
then
A15: 2sComplement(n,i)/.j = (n-BinarySequence(N))/.j by Def2
.= IFEQ((N div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A3,
BINARI_3:def 1;
2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(M))/.j by A14,Def2
.= IFEQ((M div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A4,
BINARI_3:def 1;
hence thesis by A5,A14,A15;
end;
end;
theorem Th33:
ex x be Element of BOOLEAN st 2sComplement(m+1,i) = 2sComplement (m,i)^<*x*>
proof
consider a be Element of m-tuples_on BOOLEAN,
b be Element of BOOLEAN such that
A1: 2sComplement(m+1,i) = a^<*b*> by FINSEQ_2:117;
now
per cases;
suppose
m > 0;
then reconsider m as non zero Nat;
for j be Nat st j in Seg m holds 2sComplement(m,i).j = a.j
proof
A2: len 2sComplement(m,i) = m by CARD_1:def 7;
let j be Nat such that
A3: j in Seg m;
reconsider j as Nat;
A4: 1 <= j by A3,FINSEQ_1:1;
len a = m by CARD_1:def 7;
then
A5: j in dom a by A3,FINSEQ_1:def 3;
A6: j <= m by A3,FINSEQ_1:1;
m <= m + 1 by NAT_1:11;
then len 2sComplement(m+1,i) = m+1 & j <= m + 1 by A6,CARD_1:def 7
,XXREAL_0:2;
then 2sComplement(m+1,i).j = 2sComplement(m+1,i)/.j by A4,FINSEQ_4:15
.= 2sComplement(m,i)/.j by A4,A6,Th32
.= 2sComplement(m,i).j by A2,A4,A6,FINSEQ_4:15;
hence thesis by A1,A5,FINSEQ_1:def 7;
end;
then a = 2sComplement(m,i) by FINSEQ_2:119;
hence thesis by A1;
end;
suppose
A7: m = 0;
then consider c be Element of BOOLEAN such that
A8: 2sComplement(m+1,i) = <*c*> by FINSEQ_2:97;
A9: 2sComplement(m+1,i) = {}^<*c*> by A8,FINSEQ_1:34;
2sComplement(m,i) = {} by A7;
hence thesis by A9;
end;
end;
hence thesis;
end;
theorem
ex x be Element of BOOLEAN st (m+1)-BinarySequence(l) = (m
-BinarySequence(l))^<*x*>
proof
consider x be Element of BOOLEAN such that
A1: 2sComplement(m+1,l) = 2sComplement(m,l)^<*x*> by Th33;
A2: |.l.| = l by ABSVALUE:def 1;
then (m+1)-BinarySequence(l) = 2sComplement(m,l)^<*x*> by A1,Def2
.= (m-BinarySequence(l))^<*x*> by A2,Def2;
hence thesis;
end;
theorem Th35:
for n be non zero Nat holds -2 to_power n <= h+i & h < 0 & i <
0 & -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i implies carry(
2sComplement(n+1,h),2sComplement(n+1,i))/.(n+1) = TRUE
proof
defpred P[Nat] means -2 to_power $1 <= h+i & h < 0 & i < 0 & -2 to_power ($1
-'1) <= h & -2 to_power ($1-'1) <= i implies carry(2sComplement($1+1,h),
2sComplement($1+1,i))/.($1+1) = TRUE;
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat such that
P[n];
assume that
-2 to_power (n+1) <= h+i and
A2: h < 0 and
A3: i < 0 and
A4: -2 to_power (n+1-'1) <= h and
A5: -2 to_power (n+1-'1) <= i;
set H1 = 2sComplement(n+1+1,h), I1 = 2sComplement(n+1+1,i), H =
2sComplement(n+1,h), I = 2sComplement(n+1,i), T = TRUE, N = n+1;
A6: N-'1 = N-1 by XREAL_0:def 2;
then
A7: 2 to_power (N-'1) < 2 to_power N by POWER:39,XREAL_1:146;
2 to_power (N-'1) + 2 to_power (N-'1) = 2*(2 to_power (N-'1))
.= (2 to_power 1)*(2 to_power (N-'1)) by POWER:25
.= 2 to_power (0+N) by A6,POWER:27;
then
A8: -2 to_power (N-'1) + 2 to_power N = 2 to_power (N-'1);
then
A9: 2 to_power (N-'1) <= 2 to_power N + h by A4,XREAL_1:6;
A10: 2 to_power (N-'1) <= 2 to_power N + i by A5,A8,XREAL_1:6;
A11: 2 to_power N + i < 0 + 2 to_power N by A3,XREAL_1:8;
N-1 = n;
then
A12: N-'1 = n by XREAL_0:def 2;
0 <= 2 to_power N + h & 0 <= 2 to_power N + i by A4,A5,A8,XREAL_1:6;
then reconsider
NH = 2 to_power N + h, NI = 2 to_power N + i as Element of NAT
by INT_1:3;
A13: len(N-BinarySequence(NI)) = N by CARD_1:def 7;
A14: 1 <= N by NAT_1:11;
then
A15: H1/.N = H/.N & I1/.N = I/.N by Th32;
A16: 2 to_power N + h < 0 + 2 to_power N by A2,XREAL_1:8;
A17: N < N+1 by NAT_1:13;
|.i.| = -i by A3,ABSVALUE:def 1;
then --2 to_power (N-'1) >= |.i.| by A5,XREAL_1:24;
then MajP(N,|.i.|) = N by A7,Th24,XXREAL_0:2;
then
A18: I/.N = (N-BinarySequence |.NI.|)/.N by A3,Def2
.= (N-BinarySequence(NI))/.N by ABSVALUE:def 1
.= (N-BinarySequence(NI)).N by A14,A13,FINSEQ_4:15
.= T by A12,A10,A11,BINARI_3:29;
A19: len (N-BinarySequence(NH)) = N by CARD_1:def 7;
|.h.| = -h by A2,ABSVALUE:def 1;
then --2 to_power (N-'1) >= |.h.| by A4,XREAL_1:24;
then MajP(N,|.h.|) = N by A7,Th24,XXREAL_0:2;
then H/.N = (N-BinarySequence|.NH.|)/.N by A2,Def2
.= (N-BinarySequence(NH))/.N by ABSVALUE:def 1
.= (N-BinarySequence(NH)).N by A14,A19,FINSEQ_4:15
.= T by A12,A9,A16,BINARI_3:29;
then
carry(H1,I1)/.(N+1) = T '&' T 'or' T '&' (carry(H1,I1)/.N) 'or' T '&'
(carry(H1,I1)/.N) by A14,A18,A15,A17,BINARITH:def 2
.= T 'or' (carry(H1,I1)/.N);
hence thesis;
end;
A20: P[1]
proof
1-'1 = 1-1 by XREAL_0:def 2;
then 3 div 2 to_power (1-'1) = (1+2) div 1 by POWER:24
.= 3;
then
A21: (3 div 2 to_power (1-'1)) mod 2 = (2+1) mod 2
.= ((2 mod 2) + 1) mod 2 by NAT_D:22
.= (0 + 1) mod 2 by NAT_D:25
.= 1 by PEPIN:5;
A22: -2+1 = -1;
set H = 2sComplement(2,h), I = 2sComplement(2,i), T = TRUE;
assume that
A23: -2 to_power 1 <= h+i and
A24: h < 0 and
A25: i < 0 and
-2 to_power (1-'1) <= h and
-2 to_power (1-'1) <= i;
A26: i <= -1 by A25,INT_1:8;
-2 to_power 1 < h by A23,A24,A25,Th9;
then -2 < h by POWER:25;
then
A27: -1 <= h by A22,INT_1:7;
-2 to_power 1 < i by A23,A24,A25,Th9;
then -2 < i by POWER:25;
then -1 <= i by A22,INT_1:7;
then
A28: i = -1 by A26,XXREAL_0:1;
A29: 1 in Seg 2 by FINSEQ_1:1;
A30: 2 to_power 2 = 2 |^ (1+1) by POWER:41
.= 2 |^ 1 + 2 |^ 1 by PEPIN:29
.= 2 to_power 1 + 2 |^ 1 by POWER:41
.= 2 to_power 1 + 2 to_power 1 by POWER:41
.= 2 + 2 to_power 1 by POWER:25
.= 2 + 2 by POWER:25;
A31: 2 to_power 2 > 2 to_power 0 by POWER:39;
A32: h <= -1 by A24,INT_1:8;
then
A33: h = -1 by A27,XXREAL_0:1;
then |.h.| = --1 by ABSVALUE:def 1;
then 2 to_power 0 = |.h.| by POWER:24;
then MajP(2,|.h.|) = 2 by A31,Th24;
then |.2 to_power MajP(2,|.h.|) + h.| = |.4 + -1.| by A27,A32,A30,
XXREAL_0:1
.= 3 by ABSVALUE:def 1;
then (2sComplement(2,h))/.1 = (2-BinarySequence(3))/.1 by A24,Def2
.= IFEQ(1,0,FALSE,TRUE) by A21,A29,BINARI_3:def 1
.= TRUE by FUNCOP_1:def 8;
then carry(H,I)/.(1+1) = T '&' T 'or' T '&' (carry(H,I)/.1) 'or' T '&' (
carry(H,I)/.1) by A33,A28,BINARITH:def 2
.= T 'or' (carry(H,I)/.1);
hence thesis;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A20,A1);
end;
theorem
for n be non zero Nat st h + i <= 2 to_power (n-'1) - 1 & h >= 0 & i
>= 0 holds Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i
proof
let n be non zero Nat such that
A1: h + i <= 2 to_power (n-'1) - 1 and
A2: h >= 0 & i >= 0;
reconsider h,i as Element of NAT by A2,INT_1:3;
A3: 2sComplement(n,i) = n-BinarySequence(|.i.|) by Def2
.= n-BinarySequence(i) by ABSVALUE:def 1;
2sComplement(n,h) = n-BinarySequence(|.h.|) by Def2
.= n-BinarySequence(h) by ABSVALUE:def 1;
hence thesis by A1,A3,Th14;
end;
theorem
for n be non zero Nat st -2 to_power ((n+1)-'1) <= h + i & h < 0 & i
< 0 & -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i holds Intval(
2sComplement(n+1,h) + 2sComplement(n+1,i)) = h+i
proof
let n be non zero Nat such that
A1: -2 to_power ((n+1)-'1) <= h + i and
A2: h < 0 and
A3: i < 0 and
A4: -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i;
A5: 2 to_power (n+1) + -(2 to_power n) = -(2 to_power n) + ((2 to_power 1)*
(2 to_power n)) by POWER:27
.= -(2 to_power n) + 2*(2 to_power n) by POWER:25
.= 2 to_power n;
(n+1)-1 = n;
then
A6: -2 to_power n <= h+i by A1,XREAL_0:def 2;
then
A7: -2 to_power n < h by A2,A3,Th9;
then
A8: 2 to_power n <= 2 to_power (n+1) + h by A5,XREAL_1:6;
A9: -2 to_power n < i by A2,A3,A6,Th9;
then
A10: 0 <= 2 to_power (n+1) + i by A5,XREAL_1:6;
0 <= 2 to_power (n+1) + h by A7,A5,XREAL_1:6;
then reconsider
NH = 2 to_power (n+1) + h, NI = 2 to_power (n+1) + i as Element
of NAT by A10,INT_1:3;
A11: 1 <= n + 1 by NAT_1:11;
set H = 2sComplement(n,h), I = 2sComplement(n,i), H1 = 2sComplement(n+1,h),
I1 = 2sComplement(n+1,i), F = FALSE, T = TRUE;
n < n+1 by XREAL_1:29;
then
A12: 2 to_power n < 2 to_power (n+1) by POWER:39;
A13: (ex a be Element of BOOLEAN st H1 = H^<*a*> )& ex a be Element of
BOOLEAN st I1 = I^<*a*> by Th33;
A14: 2 to_power (n+1) + h < 2 to_power (n+1) + 0 by A2,XREAL_1:8;
-h < --2 to_power n by A7,XREAL_1:24;
then |.h.| < 2 to_power n by A2,ABSVALUE:def 1;
then
A15: MajP(n+1,|.h.|) = n+1 by A12,Th24,XXREAL_0:2;
then
A16: H1 = (n+1)-BinarySequence(|.2 to_power (n+1)+h.|) by A2,Def2
.= (n+1)-BinarySequence(NH) by ABSVALUE:def 1;
len H1 = n + 1 by CARD_1:def 7;
then
A17: H1/.(n+1) = H1.(n+1) by A11,FINSEQ_4:15
.= ((n+1)-BinarySequence(|.2 to_power (n+1)+h.|)).(n+1) by A2,A15,Def2
.= ((n+1)-BinarySequence(NH)).(n+1) by ABSVALUE:def 1
.= T by A14,A8,BINARI_3:29;
A18: 2 to_power n <= 2 to_power (n+1) + i by A9,A5,XREAL_1:6;
A19: 2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A3,XREAL_1:8;
-i < --2 to_power n by A9,XREAL_1:24;
then |.i.| < 2 to_power n by A3,ABSVALUE:def 1;
then
A20: MajP(n+1,|.i.|) = n+1 by A12,Th24,XXREAL_0:2;
then
A21: I1 = (n+1)-BinarySequence(|.2 to_power (n+1)+i.|) by A3,Def2
.= (n+1)-BinarySequence(NI) by ABSVALUE:def 1;
len I1 = n + 1 by CARD_1:def 7;
then
A22: I1/.(n+1) = I1.(n+1) by A11,FINSEQ_4:15
.= ((n+1)-BinarySequence(|.2 to_power (n+1)+i.|)).(n+1) by A3,A20,Def2
.= ((n+1)-BinarySequence(NI)).(n+1) by ABSVALUE:def 1
.= T by A19,A18,BINARI_3:29;
then
A23: Intval(I1) = Absval(I1) - 2 to_power (n+1) by BINARI_2:def 3
.= NI - 2 to_power (n+1) by A19,A21,BINARI_3:35
.= i;
A24: carry(H1,I1)/.(n+1) = T by A2,A3,A4,A6,Th35;
then
A25: Int_add_ovfl(H1,I1) = F '&' 'not' T '&' T by A17,A22,BINARI_2:def 4
.= F;
A26: Int_add_udfl(H1,I1) = T '&' T '&' 'not' T by A17,A22,A24,BINARI_2:def 5
.= F;
Intval(H1) = Absval(H1) - 2 to_power (n+1) by A17,BINARI_2:def 3
.= NH - 2 to_power (n+1) by A14,A16,BINARI_3:35
.= h;
then Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1)) + IFEQ(F,F,0,2
to_power(n+1)) by A13,A23,A25,A26,BINARI_2:12
.= h + i - 0 + 0;
hence thesis;
end;
theorem
for n be non zero Nat holds -(2 to_power (n-'1)) <= h & h <= 2
to_power (n-'1) - 1 & -(2 to_power (n-'1)) <= i & i <= 2 to_power (n-'1) - 1 &
-(2 to_power (n-'1)) <= h+i & h+i <= 2 to_power (n-'1) - 1 & ( h >= 0 & i < 0
or h < 0 & i >= 0 ) implies Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i
proof
defpred P[non zero Nat] means -(2 to_power ($1-'1)) <= h & h <= 2 to_power
($1-'1) - 1 & -(2 to_power ($1-'1)) <= i & i <= 2 to_power ($1-'1) - 1 & -(2
to_power ($1-'1)) <= h+i & h+i <= 2 to_power ($1-'1) - 1 & ((h >= 0 & i < 0) or
(h < 0 & i >= 0)) implies Intval(2sComplement($1,h) + 2sComplement($1,i)) = h+i
;
A1: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat such that
-(2 to_power (n-'1)) <= h & h <= 2 to_power (n-'1) - 1 & -(2 to_power
(n-'1)) <= i & i <= 2 to_power (n-'1) - 1 & -(2 to_power (n-'1)) <= h+i & h+i
<= 2 to_power (n-'1) - 1 & ( h >= 0 & i < 0 or h < 0 & i >= 0 ) implies Intval(
2sComplement(n,h) + 2sComplement(n,i)) = h+i;
assume that
A2: -(2 to_power ((n+1)-'1)) <= h and
A3: h <= 2 to_power ((n+1)-'1) - 1 and
A4: -(2 to_power ((n+1)-'1)) <= i and
A5: i <= 2 to_power ((n+1)-'1) - 1 and
-(2 to_power ((n+1)-'1)) <= h+i and
h+i <= 2 to_power ((n+1)-'1) - 1 and
A6: h >= 0 & i < 0 or h < 0 & i >= 0;
set H = 2sComplement(n,h), I = 2sComplement(n,i), H1 = 2sComplement(n+1,h)
, I1 = 2sComplement(n+1,i), n2 = 2 to_power n, F = FALSE, T = TRUE;
A7: (n+1)-1 = n;
then
A8: -n2 <= h by A2,XREAL_0:def 2;
A9: i <= n2 - 1 by A5,A7,XREAL_0:def 2;
A10: (ex a be Element of BOOLEAN st H1 = H^<*a*> )& ex b be Element of
BOOLEAN st I1 = I^<*b*> by Th33;
A11: -n2 <= i by A4,A7,XREAL_0:def 2;
A12: h <= n2 - 1 by A3,A7,XREAL_0:def 2;
now
per cases by A6;
suppose
A13: h >= 0 & i < 0;
2 to_power (n+1) + -(2 to_power n) = -(2 to_power n) + ((2
to_power 1)*(2 to_power n)) by POWER:27
.= -(2 to_power n) + 2*(2 to_power n) by POWER:25
.= 2 to_power n;
then
A14: 2 to_power n <= 2 to_power (n+1) + i by A11,XREAL_1:6;
then reconsider NI = 2 to_power (n+1) + i as Element of NAT by INT_1:3;
n < n+1 by XREAL_1:29;
then
A15: 2 to_power n < 2 to_power (n+1) by POWER:39;
|.i.| = -i by A13,ABSVALUE:def 1;
then |.i.| <= --2 to_power n by A11,XREAL_1:24;
then
A16: MajP(n+1,|.i.|) = n+1 by A15,Th24,XXREAL_0:2;
then
A17: I1 = (n+1)-BinarySequence(|.2 to_power (n+1)+i.|) by A13,Def2
.= (n+1)-BinarySequence(NI) by ABSVALUE:def 1;
A18: 2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A13,XREAL_1:8;
reconsider h as Element of NAT by A13,INT_1:3;
A19: h < 2 to_power n by A12,XREAL_1:146,XXREAL_0:2;
A20: H1 = (n+1)-BinarySequence(|.h.|) by Def2
.= (n+1)-BinarySequence(h) by ABSVALUE:def 1;
then
A21: H1.(n+1) = F by A19,BINARI_3:26;
n + 0 < n+1 by XREAL_1:8;
then 2 to_power n < 2 to_power (n+1) by POWER:39;
then
A22: h < 2 to_power (n+1) by A19,XXREAL_0:2;
A23: 1 <= n + 1 by NAT_1:11;
len I1 = n+1 by CARD_1:def 7;
then
A24: I1/.(n+1) = I1.(n+1) by A23,FINSEQ_4:15;
A25: I1.(n+1) = ((n+1)-BinarySequence(|.2 to_power (n+1)+i.|)).(n+1)
by A13,A16,Def2
.= ((n+1)-BinarySequence(NI)).(n+1) by ABSVALUE:def 1
.= T by A18,A14,BINARI_3:29;
then
A26: Intval(I1) = Absval(I1) - 2 to_power (n+1) by A24,BINARI_2:def 3
.= NI - 2 to_power (n+1) by A18,A17,BINARI_3:35
.= i;
len H1 = n+1 by CARD_1:def 7;
then
A27: H1/.(n+1) = H1.(n+1) by A23,FINSEQ_4:15;
then
A28: Int_add_ovfl(H1,I1) = 'not' F '&' 'not' T '&' (carry(H1,I1)/.(n+1
)) by A21,A25,A24,BINARI_2:def 4
.= F;
A29: Int_add_udfl(H1,I1) = F '&' T '&' 'not' (carry(H1,I1)/.(n+1)) by A21
,A25,A27,A24,BINARI_2:def 5
.= F;
Intval(H1) = Absval(H1) by A21,A27,BINARI_2:def 3
.= h by A20,A22,BINARI_3:35;
then
Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1)) + IFEQ(F,F,0,
2 to_power(n+1)) by A10,A26,A28,A29,BINARI_2:12
.= h + i - 0 + 0;
hence thesis;
end;
suppose
A30: h < 0 & i >= 0;
2 to_power (n+1) + -(2 to_power n) = -(2 to_power n) + ((2
to_power 1)*(2 to_power n)) by POWER:27
.= -(2 to_power n) + 2*(2 to_power n) by POWER:25
.= 2 to_power n;
then
A31: 2 to_power n <= 2 to_power (n+1) + h by A8,XREAL_1:6;
then reconsider NH = 2 to_power (n+1) + h as Element of NAT by INT_1:3;
n < n+1 by XREAL_1:29;
then
A32: 2 to_power n < 2 to_power (n+1) by POWER:39;
|.h.| = -h by A30,ABSVALUE:def 1;
then |.h.| <= --2 to_power n by A8,XREAL_1:24;
then
A33: MajP(n+1,|.h.|) = n+1 by A32,Th24,XXREAL_0:2;
then
A34: H1 = (n+1)-BinarySequence(|.2 to_power (n+1)+h.|) by A30,Def2
.= (n+1)-BinarySequence(NH) by ABSVALUE:def 1;
A35: 2 to_power (n+1) + h < 2 to_power (n+1) + 0 by A30,XREAL_1:8;
reconsider i as Element of NAT by A30,INT_1:3;
A36: i < 2 to_power n by A9,XREAL_1:146,XXREAL_0:2;
A37: I1 = (n+1)-BinarySequence(|.i.|) by Def2
.= (n+1)-BinarySequence(i) by ABSVALUE:def 1;
then
A38: I1.(n+1) = F by A36,BINARI_3:26;
n + 0 < n+1 by XREAL_1:8;
then 2 to_power n < 2 to_power (n+1) by POWER:39;
then
A39: i < 2 to_power (n+1) by A36,XXREAL_0:2;
A40: 1 <= n + 1 by NAT_1:11;
len H1 = n+1 by CARD_1:def 7;
then
A41: H1/.(n+1) = H1.(n+1) by A40,FINSEQ_4:15;
A42: H1.(n+1) = ((n+1)-BinarySequence(|.2 to_power (n+1)+h.|)).(n+1)
by A30,A33,Def2
.= ((n+1)-BinarySequence(NH)).(n+1) by ABSVALUE:def 1
.= T by A35,A31,BINARI_3:29;
then
A43: Intval(H1) = Absval(H1) - 2 to_power (n+1) by A41,BINARI_2:def 3
.= NH - 2 to_power (n+1) by A35,A34,BINARI_3:35
.= h;
len I1 = n+1 by CARD_1:def 7;
then
A44: I1/.(n+1) = I1.(n+1) by A40,FINSEQ_4:15;
then
A45: Int_add_ovfl(H1,I1) = 'not' T '&' 'not' F '&' (carry(H1,I1)/.(n+1
)) by A38,A42,A41,BINARI_2:def 4
.= F;
A46: Int_add_udfl(H1,I1) = T '&' F '&' 'not' (carry(H1,I1)/.(n+1)) by A38
,A42,A44,A41,BINARI_2:def 5
.= F;
Intval(I1) = Absval(I1) by A38,A44,BINARI_2:def 3
.= i by A37,A39,BINARI_3:35;
then
Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1)) + IFEQ(F,F,0,
2 to_power(n+1)) by A10,A43,A45,A46,BINARI_2:12
.= h + i - 0 + 0;
hence thesis;
end;
end;
hence thesis;
end;
A47: P[1]
proof
A48: |.-1.| = --1 by ABSVALUE:def 1
.= 1;
2 to_power 1 = 2 & for k be Nat st 2 to_power k >= 1 & k >= 1 holds k
>= 1 by POWER:25;
then MajP(1,|.-1.|) = 1 by A48,Def1;
then
A49: 2sComplement(1,-1) = 1-BinarySequence(|.(2 to_power 1)+-1.|) by Def2
.= 1-BinarySequence(|.2+-1.|) by POWER:25
.= 1-BinarySequence(1) by ABSVALUE:def 1
.= (0+1)-BinarySequence(2 to_power 0) by POWER:24
.= (0*0)^<*1*> by BINARI_3:28
.= <*TRUE*> by FINSEQ_1:34;
assume that
A50: -(2 to_power (1-'1)) <= h and
A51: h <= 2 to_power (1-'1) - 1 and
A52: -(2 to_power (1-'1)) <= i and
A53: i <= 2 to_power (1-'1) - 1 and
-(2 to_power (1-'1)) <= h+i and
h+i <= 2 to_power (1-'1) - 1 and
A54: h >= 0 & i < 0 or h < 0 & i >= 0;
A55: 1 -' 1 = 1 - 1 by XREAL_0:def 2
.= 0;
then
A56: h <= 1-1 by A51,POWER:24;
A57: i <= 1-1 by A53,A55,POWER:24;
A58: -1 <= i by A52,A55,POWER:24;
A59: 2sComplement(1,0) = 1-BinarySequence |.0.| by Def2
.= 1-BinarySequence(0) by ABSVALUE:def 1
.= 0*1 by BINARI_3:25
.= <* FALSE *> by FINSEQ_2:59;
A60: -1 <= h by A50,A55,POWER:24;
now
per cases by A54;
suppose
A61: h >= 0 & i < 0;
then i <= -1 by INT_1:8;
then
A62: i = -1 by A58,XXREAL_0:1;
h = 0 by A56,A61;
hence thesis by A59,A49,A62,Th15,BINARI_3:17;
end;
suppose
A63: h < 0 & i >= 0;
then h <= -1 by INT_1:8;
then
A64: h = -1 by A60,XXREAL_0:1;
i = 0 by A57,A63;
hence thesis by A59,A49,A64,Th15,BINARI_3:17;
end;
end;
hence thesis;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A47,A1);
end;