Copyright (c) 2003 Association of Mizar Users
environ
vocabulary INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, ABSVALUE,
BINARITH, BINARI_2, BINARI_3, ARYTM_1, NAT_1, BINARI_4, EUCLID, ARYTM_3,
FINSEQ_2, FINSEQ_4, FUNCT_1, BOOLE, RELAT_1, VECTSP_1, ZF_LANG, GROUP_1;
notation INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, BINARITH,
BINARI_2, BINARI_3, GROUP_1, SERIES_1, NUMBERS, XCMPLX_0, XREAL_0,
XBOOLE_0, EUCLID, REAL_1, NAT_1, TARSKI, FINSEQ_4, FUNCT_1, RELAT_1,
VECTSP_1, ZFMISC_1, FINSEQOP, PREPOWER, SUBSET_1;
constructors BINARITH, BINARI_2, BINARI_3, GROUP_1, SERIES_1, REAL_1, EUCLID,
FINSEQ_4, FINSEQOP, SEQ_1, PREPOWER, EULER_2, MEMBERED;
clusters INT_1, BINARITH, MARGREL1, RELSET_1, NAT_1, XREAL_0, MEMBERED;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
theorems AXIOMS, POWER, NAT_1, PRE_FF, ABSVALUE, REAL_1, BINARI_3, INT_1,
BINARITH, NAT_2, BINARI_2, JORDAN2B, FINSEQ_1, FINSEQ_2, FINSEQ_4,
MARGREL1, EUCLID, FUNCOP_1, RVSUM_1, FUNCT_2, ZFMISC_1, JORDAN4, GR_CY_1,
CQC_LANG, GROUP_4, INT_3, SCMFSA9A, EULER_2, PEPIN, PREPOWER, ARMSTRNG,
XCMPLX_0, XCMPLX_1, RLVECT_1;
schemes NAT_1, BINARITH;
begin :: Preliminaries
reserve n for non empty Nat,
j,k,l,m for Nat,
g,h,i for Integer;
theorem Th1:
m > 0 implies m * 2 >= m + 1
proof
assume m > 0;
then m >= 0 + 1 by INT_1:20;
then m >= 1 & m * 2 = m + m by XCMPLX_1:11;
hence thesis by AXIOMS:24;
end;
theorem Th2:
for m being Nat holds 2 to_power m >= m
proof
defpred _P[Nat] means 2 to_power $1 >= $1;
2 to_power 0 = 1 by POWER:29;
then A1:_P[0];
A2:for m being Nat st _P[m] holds _P[m+1] proof
let m be Nat such that
A3: 2 to_power m >= m;
now per cases by NAT_1:19;
suppose
A4: m = 0;
then 2 to_power (m+1) = 2 by POWER:30;
hence thesis by A4;
suppose
A5: m > 0;
A6: (2 to_power m) * 2 >= m * 2 by A3,NAT_1:20;
2 to_power 1 = 2 by POWER:30;
then A7: 2 to_power (m+1) >= m * 2 by A6,POWER:32;
m * 2 >= m + 1 by A5,Th1;
hence thesis by A7,AXIOMS:22;
end;
hence thesis;
end;
thus for m being Nat holds _P[m] from Ind(A1,A2);
end;
theorem
for m be Nat holds 0*m + 0*m = 0*m
proof
let m be Nat;
A1:dom addreal = [:REAL,REAL:] by FUNCT_2:def 1;
rng 0*m c= REAL by FINSEQ_1:def 4;
then A2:[:rng 0*m, rng 0*m:] c= dom addreal by A1,ZFMISC_1:119;
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:84
.= dom (m |-> (0 qua Real)) by EUCLID:def 4
.= Seg m by FINSEQ_2:68;
A4:dom(0*m) = dom(m |-> (0 qua Real)) by EUCLID:def 4
.= Seg m by FINSEQ_2:68;
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
A5: k in dom(0*m);
A6: (0*m).k = (m |-> (0 qua Real)).k by EUCLID:def 4
.= 0 qua Real by A4,A5,FINSEQ_2:70;
then (0*m+0*m).k = 0 + 0 by A3,A4,A5,RVSUM_1:26;
hence thesis by A6;
end;
hence thesis by A3,A4,FINSEQ_1:17;
end;
theorem Th4:
for k be Nat holds
k <= l & l <= m implies k = l or (k + 1 <= l & l <= m)
proof
defpred _P[Nat] means
$1 <= l & l <= m implies $1 = l or ($1 + 1 <= l & l <= m);
A1: _P[0] by NAT_1:38;
A2:for k be Nat st _P[k] holds _P[k+1] proof
let k be Nat such that
k <= l & l <= m implies k = l or (k + 1 <= l & l <= m);
assume that
A3: k+1 <= l and
A4: l <= m;
k+1 = l or k+1 < l by A3,AXIOMS:21;
hence thesis by A4,NAT_1:38;
end;
thus for k being Nat holds _P[k] from Ind(A1,A2);
end;
theorem Th5:
for n be non empty 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 empty Nat;
let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n & y = 0*n;
len carry(x,y) = n by FINSEQ_2:109;
then 1 <= len carry(x,y) by RLVECT_1:99;
then A2:carry(x,y).1 = carry(x,y)/.1 by FINSEQ_4:24
.= 0 by BINARITH:def 5,MARGREL1:36;
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 & j <= n;
reconsider k = j - 1 as Nat by A4,INT_1:18;
k + 1 = j + 1 - 1 by XCMPLX_1:29
.= j by XCMPLX_1:26;
then A5: 1 <= k & k < n & j = k + 1 by A4,NAT_1:38;
then A6: k in Seg n & k <= len x & k <= len y by FINSEQ_1:3,FINSEQ_2:109;
len(0*n) = len(n |-> (0 qua Real)) by EUCLID:def 4
.= n by FINSEQ_2:69;
then A7: x/.k = (0*n).k by A1,A5,FINSEQ_4:24
.= (n |-> (0 qua Real)).k by EUCLID:def 4
.= FALSE by A6,FINSEQ_2:70,MARGREL1:36;
len carry(x,y) = n by FINSEQ_2:109;
then carry(x,y).j = carry(x,y)/.j by A4,FINSEQ_4:24
.= FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.k) 'or'
FALSE '&' (carry(x,y)/.k) by A1,A5,A7,BINARITH:def 5
.= FALSE 'or' FALSE '&' (carry(x,y)/.k) 'or'
FALSE '&' (carry(x,y)/.k) by MARGREL1:49
.= FALSE 'or' FALSE 'or' FALSE '&' (carry(x,y)/.k) by MARGREL1:49
.= FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7;
hence thesis by MARGREL1:36;
end;
for l be Nat st l in Seg n holds carry(x,y).l = (0*n).l
proof
let l be Nat such that
A8: l in Seg n;
A9: 1 <= l & l <= n by A8,FINSEQ_1:3;
A10: (0*n).l = (n |-> (0 qua Real)).l by EUCLID:def 4
.= 0 by A8,FINSEQ_2:70;
now per cases by A9,Th4;
suppose l = 1;
hence thesis by A2,A10;
suppose 1 + 1 <= l & l <= n;
then 1 < l & l <= n by NAT_1:38;
hence thesis by A3,A10;
end;
hence thesis;
end;
hence thesis by A1,FINSEQ_2:139;
end;
theorem
for n be non empty 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 empty Nat;
let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n & 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
A2: k in Seg n;
A3: (0*n).k = (n |-> (0 qua Real)).k by EUCLID:def 4
.= FALSE by A2,FINSEQ_2:70,MARGREL1:36;
len x = n & len y = n & len carry(x,y) = n & len(x+y) = n
by FINSEQ_2:109;
then A4: 1 <= k & k <= len x & k <= len carry(x,y) & k <= len(x+y)
by A2,FINSEQ_1:3;
then A5: y/.k = FALSE by A1,A3,FINSEQ_4:24;
A6: carry(x,y)/.k = carry(x,y).k by A4,FINSEQ_4:24
.= FALSE by A1,A3,Th5;
(x+y).k = (x+y)/.k by A4,FINSEQ_4:24
.= FALSE 'xor' FALSE 'xor' FALSE by A1,A2,A5,A6,BINARITH:def 8
.= FALSE 'xor' FALSE by BINARITH:14
.= FALSE by BINARITH:14;
hence thesis by A3;
end;
hence thesis by A1,FINSEQ_2:139;
end;
theorem
for n be non empty Nat
for F be Tuple of n,BOOLEAN st F = 0*n holds
Intval F = 0
proof
let n be non empty Nat;
let F be Tuple of n,BOOLEAN such that
A1:F = 0*n;
A2:1 <= n & n <= len F by FINSEQ_2:109,RLVECT_1:99;
then A3:n in Seg n by FINSEQ_1:3;
F/.n = F.n by A2,FINSEQ_4:24
.= FALSE by A1,A3,JORDAN2B:2,MARGREL1:def 13;
then Intval F = Absval F by BINARI_2:def 3;
hence thesis by A1,BINARI_3:7;
end;
theorem Th8:
l + m <= k - 1 implies l < k & m < k
proof
assume
A1: l + m <= k - 1;
k <= k + m by NAT_1:29;
then k - m <= k + m - m by REAL_1:49;
then k - m <= k + m + -m by XCMPLX_0:def 8;
then A2:k - m <= k by XCMPLX_1:137;
l + m - m <= k - 1 - m by A1,REAL_1:49;
then l + m + -m <= k - 1 - m by XCMPLX_0:def 8;
then A3:l <= k - 1 - m by XCMPLX_1:137;
k - 1 - m = k - m - 1 by XCMPLX_1:21;
then k - 1 - m < k - m by INT_1:26;
then k - 1 - m < k by A2,AXIOMS:22;
hence l < k by A3,AXIOMS:22;
k <= k + l by NAT_1:29;
then k - l <= k + l - l by REAL_1:49;
then k - l <= k + l + -l by XCMPLX_0:def 8;
then A4:k - l <= k by XCMPLX_1:137;
m + l - l <= k - 1 - l by A1,REAL_1:49;
then m + l + -l <= k - 1 - l by XCMPLX_0:def 8;
then A5:m <= k - 1 - l by XCMPLX_1:137;
k - 1 - l = k - l - 1 by XCMPLX_1:21;
then k - 1 - l < k - l by INT_1:26;
then k - 1 - l < k by A4,AXIOMS:22;
hence thesis by A5,AXIOMS:22;
end;
theorem Th9:
g <= h + i & h < 0 & i < 0 implies g < h & g < i
proof
assume
A1: g <= h + i & h < 0 & i < 0;
then g - i <= h + i - i by REAL_1:49;
then g - i <= h by XCMPLX_1:26;
then i + (g - i) < 0 + h by A1,REAL_1:67;
then i + (g + -i) < 0 + h by XCMPLX_0:def 8;
then i + -i + g < h by XCMPLX_1:1;
then i - i + g < h by XCMPLX_0:def 8;
then 0 + g < h by XCMPLX_1:14;
hence g < h;
g - h <= i + h - h by A1,REAL_1:49;
then g - h <= i by XCMPLX_1:26;
then h + (g - h) < 0 + i by A1,REAL_1:67;
then h + (g + -h) < 0 + i by XCMPLX_0:def 8;
then h + -h + g < i by XCMPLX_1:1;
then h - h + g < i by XCMPLX_0:def 8;
then 0 + g < i by XCMPLX_1:14;
hence thesis;
end;
theorem Th10:
l + m <= 2 to_power n - 1 implies
add_ovfl(n-BinarySequence(l),n-BinarySequence(m)) = FALSE
proof
assume
A1: l + m <= 2 to_power n - 1;
set L = n-BinarySequence(l), M = n-BinarySequence(m);
assume
A2:add_ovfl(L,M) <> FALSE;
A3:l < 2 to_power n & m < 2 to_power n by A1,Th8;
A4:IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n) = 2 to_power n
by A2,CQC_LANG:def 1;
A5:Absval(L+M) + IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n)
= Absval(L)+Absval(M) by BINARITH:47
.= l + Absval(M) by A3,BINARI_3:36
.= l + m by A3,BINARI_3:36;
A6:2 to_power n > 2 to_power n - 1 by INT_1:26;
Absval(L+M) + 2 to_power n >= 2 to_power n by NAT_1:29;
hence contradiction by A1,A4,A5,A6,AXIOMS:22;
end;
theorem Th11:
for n be non empty 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 empty Nat, l,m be Nat such that
A1: l + m <= 2 to_power n - 1;
set L = n-BinarySequence(l), M = n-BinarySequence(m);
A2:l < 2 to_power n & m < 2 to_power n by A1,Th8;
add_ovfl(L,M) = FALSE by A1,Th10;
then L,M are_summable by BINARITH:def 10;
then Absval(L+M) = Absval(L) + Absval(M) by BINARITH:48
.= l + Absval(M) by A2,BINARI_3:36;
hence thesis by A2,BINARI_3:36;
end;
theorem Th12:
for n be non empty 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: _P[1] proof
let z be Tuple of 1,BOOLEAN such that
A2: z/.1 = TRUE;
A3: len z = 1 by FINSEQ_2:109;
then z.1 = z/.1 by FINSEQ_4:24;
then z = <*TRUE*> by A2,A3,FINSEQ_1:57;
then A4: Absval(z) = 1 by BINARITH:42;
2 to_power (1-'1) = 2 to_power (1-1) by BINARITH:def 3;
hence thesis by A4,POWER:29;
end;
A5:for n be non empty Nat st _P[n] holds _P[n+1] proof
let n be non empty Nat such that _P[n];
let z be Tuple of (n+1),BOOLEAN such that
A6: z/.(n+1) = TRUE;
consider x be (Tuple of n,BOOLEAN), a be Element of BOOLEAN such that
A7: z = x^<*a*> by FINSEQ_2:137;
A8: n + 1 >= 1 by NAT_1:29;
then n + 1 - 1 >= 1 - 1 by REAL_1:49;
then A9: n + 1 -' 1 = n + 1 - 1 by BINARITH:def 3
.= n by XCMPLX_1:26;
len z = n+1 by FINSEQ_2:109;
then A10: z/.(n+1) = (x^<*a*>).(n+1) by A7,A8,FINSEQ_4:24
.= a by FINSEQ_2:136;
Absval(z) = Absval(x) + IFEQ(a,FALSE,0,2 to_power n) by A7,BINARITH:46
.= Absval(x) + 2 to_power n by A6,A10,CQC_LANG:def 1,MARGREL1:38;
hence thesis by A9,NAT_1:29;
end;
thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A5);
end;
theorem Th13:
l + m <= 2 to_power (n-'1) - 1 implies
carry(n-BinarySequence(l),n-BinarySequence(m))/.n = FALSE
proof
assume
A1: l + m <= 2 to_power (n-'1) - 1;
set L = n-BinarySequence(l), M = n-BinarySequence(m),
F = FALSE, T = TRUE;
assume
not(carry(L,M)/.n = F);
then A2:carry(L,M)/.n = T by MARGREL1:39;
A3:l < 2 to_power (n-'1) & m < 2 to_power (n-'1) by A1,Th8;
1 <= n by RLVECT_1:99;
then A4:n in Seg n by FINSEQ_1:3;
then A5:L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A3,JORDAN4:5
.= IFEQ(0,0,F,T) by GR_CY_1:6
.= F by CQC_LANG:def 1;
A6:M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by A4,BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A3,JORDAN4:5
.= IFEQ(0,0,F,T) by GR_CY_1:6
.= F by CQC_LANG:def 1;
n >= 1 by RLVECT_1:99;
then n-1 >= 1-1 by REAL_1:49;
then n-'1 = n - 1 by BINARITH:def 3;
then n-'1 < n by INT_1:26;
then 2 to_power (n-'1) < 2 to_power n by POWER:44;
then 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
then A7:l + m <= 2 to_power n - 1 by A1,AXIOMS:22;
(L+M)/.n = F 'xor' F 'xor' T by A2,A4,A5,A6,BINARITH:def 8
.= F 'xor' T by BINARITH:14
.= T by BINARITH:14;
then A8:Absval(L+M) >= 2 to_power (n-'1) by Th12;
2 to_power (n-'1) - 1 < 2 to_power (n-'1) by INT_1:26;
then l + m < 2 to_power (n-'1) by A1,AXIOMS:22;
hence contradiction by A7,A8,Th11;
end;
theorem Th14:
for n be non empty 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 empty Nat such that
A1: l + m <= 2 to_power (n-'1) - 1;
set L = n-BinarySequence(l), M = n-BinarySequence(m),
F = FALSE, T = TRUE;
A2:l < 2 to_power (n-'1) & m < 2 to_power (n-'1) by A1,Th8;
1 <= n by RLVECT_1:99;
then A3:n in Seg n by FINSEQ_1:3;
then A4:L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A2,JORDAN4:5
.= IFEQ(0,0,F,T) by GR_CY_1:6
.= F by CQC_LANG:def 1;
M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by A3,BINARI_3:def 1
.= IFEQ(0 mod 2,0,F,T) by A2,JORDAN4:5
.= IFEQ(0,0,F,T) by GR_CY_1:6
.= F by CQC_LANG:def 1;
then (L+M)/.n = F 'xor' F 'xor' (carry(L,M)/.n) by A3,A4,BINARITH:def 8
.= F 'xor' (carry(L,M)/.n) by BINARITH:14
.= carry(L,M)/.n by BINARITH:14
.= F by A1,Th13;
then A5:Intval(L+M) = Absval(L+M) by BINARI_2:def 3;
n >= 1 by RLVECT_1:99;
then n-1 >= 1-1 by REAL_1:49;
then n-'1 = n - 1 by BINARITH:def 3;
then n-'1 < n by INT_1:26;
then 2 to_power (n-'1) < 2 to_power n by POWER:44;
then 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
then l + m <= 2 to_power n - 1 by A1,AXIOMS:22;
hence thesis by A5,Th11;
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 FINSEQ_2:109;
then z/.1 = z.1 by FINSEQ_4:24
.= TRUE by A1,FINSEQ_1:57;
then Intval(z) = Absval(z) - 2 to_power 1 by BINARI_2:def 3,MARGREL1:38
.= 1 - 2 to_power 1 by A1,BINARITH:42
.= 1 - (1 + 1) by POWER:30
.= 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 FINSEQ_2:109;
then z/.1 = z.1 by FINSEQ_4:24
.= FALSE by A1,FINSEQ_1:57;
then Intval(z) = Absval(z) by BINARI_2:def 3;
hence thesis by A1,BINARITH:41;
end;
theorem Th17:
for x be boolean set holds
TRUE 'or' x = TRUE
proof
let x be boolean set;
TRUE 'or' x = 'not'('not' TRUE '&' 'not' x) by BINARITH:def 1
.= 'not'(FALSE '&' 'not' x) by MARGREL1:41
.= 'not' FALSE by MARGREL1:49;
hence thesis by MARGREL1:41;
end;
theorem
for n be non empty 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;
1 - 1 = 0;
then 2 to_power (1-'1) = 2 to_power 0 by BINARITH:def 3
.= 1 by POWER:29;
then A1: _P[1];
A2:for k be non empty Nat st _P[k] holds _P[k+1] proof
let k be non empty Nat such that
A3: 0 <= 2 to_power (k-'1) - 1 & -(2 to_power (k-'1)) <= 0;
(k+1)-'1
= k by BINARITH:39;
then 2 > 1 & k-'1 < (k+1)-'1 by NAT_2:11;
then 2 to_power (k-'1) < 2 to_power ((k+1)-'1) by POWER:44;
hence thesis by A3,REAL_1:49,50;
end;
thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A2);
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 & y = 0*n;
A2:1 <= n & len x = n by FINSEQ_2:109,RLVECT_1:99;
then A3:n in Seg n by FINSEQ_1:3;
x/.n = (0*n).n by A1,A2,FINSEQ_4:24
.= (n |-> (0 qua Real)).n by EUCLID:def 4
.= FALSE by A3,FINSEQ_2:70,MARGREL1:36;
then add_ovfl(x,y) = FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.n) 'or'
FALSE '&' (carry(x,y)/.n) by A1,BINARITH:def 9
.= FALSE 'or' FALSE '&' (carry(x,y)/.n) 'or' FALSE '&' (carry(x,y)/.n)
by MARGREL1:49
.= FALSE 'or' FALSE 'or' FALSE '&' (carry(x,y)/.n) by MARGREL1:49
.= FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
.= FALSE 'or' FALSE by BINARITH:7
.= FALSE by BINARITH:7;
hence thesis by BINARITH:def 10;
end;
theorem Th20:
(i*n) mod n = 0
proof
n >= 0 + 1 by RLVECT_1:99;
then n > 0 by NAT_1:38;
then (i*n) mod n = ((i mod n) * ((n qua Integer) mod n)) mod n by INT_3:15
.= ((i mod n) * (n mod n)) mod n by SCMFSA9A:5
.= ((i mod n) * 0) mod n by GR_CY_1:5
.= 0 mod n by SCMFSA9A:5;
hence thesis by GR_CY_1:6;
end;
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;
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 2 to_power j >= j & j >= m by A2,Th2,AXIOMS:22;
then A3: ex k be Nat st _P[k];
ex k be Nat st _P[k] & for l be Nat st _P[l] holds l >= k from Min(A3);
hence thesis;
end;
uniqueness
proof
let p, q be Nat such that
A4: 2 to_power p >= j & p >= m &
for k be Nat st 2 to_power k >= j & k >= m holds k >= p and
A5: 2 to_power q >= j & q >= m &
for k be Nat st 2 to_power k >= j & k >= m holds k >= q;
p >= q & q >= p by A4,A5;
hence thesis by AXIOMS:21;
end;
end;
theorem
j >= k implies MajP(m, j) >= MajP(m, k)
proof
assume
A1: j >= k;
2 to_power MajP(m, j) >= j & MajP(m, j) >= m by Def1;
then 2 to_power MajP(m, j) >= k & MajP(m, j) >= m by A1,AXIOMS:22;
hence thesis by 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 & MajP(l,j) >= l by Def1;
then MajP(l,j) >= m by A1,AXIOMS:22;
hence thesis by A2,Def1;
end;
theorem
m >= 1 implies MajP(m, 1) = m
proof
assume m >= 1;
then m >= 0 + 1;
then 2 > 1 & m > 0 by NAT_1:38;
then A1:2 to_power m >= 1 & m >= m by POWER:40;
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
assume
A1: j <= 2 to_power m;
for k be Nat st 2 to_power k >= j & k >= m holds k >= 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,AXIOMS:22;
hence thesis by PRE_FF:10;
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( abs( (2 to_power MajP(m,abs(i))) + i ) ) if i < 0
otherwise
m-BinarySequence( abs(i) );
correctness;
end;
theorem
for m be Nat holds 2sComplement(m,0) = 0*m
proof
let m be Nat;
2sComplement(m,0) = m-BinarySequence( abs(0) ) by Def2
.= m-BinarySequence(0) by ABSVALUE:7;
hence thesis by BINARI_3:26;
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 & -(2 to_power (n-'1)) <= i;
A2:n >= 1 by RLVECT_1:99;
now per cases;
suppose
A3: i >= 0;
then reconsider i as Nat by INT_1:16;
A4: 2sComplement(n,i) = n-BinarySequence(abs(i)) by A3,Def2
.= n-BinarySequence(i) by A3,ABSVALUE:def 1;
i + 1 <= 2 to_power (n-'1) - 1 + 1 by A1,AXIOMS:24;
then i + 1 <= 2 to_power (n-'1) + 1 - 1 by XCMPLX_1:29;
then i + 1 <= 2 to_power (n-'1) by XCMPLX_1:26;
then A5: i < 2 to_power (n-'1) by NAT_1:38;
n >= 1 by RLVECT_1:99;
then n - 1 >= 1 - 1 by REAL_1:49;
then n-'1 = n - 1 by BINARITH:def 3;
then n-'1 < n by INT_1:26;
then 2 to_power (n-'1) < 2 to_power n by POWER:44;
then i < 2 to_power n by A5,AXIOMS:22;
then A6: Absval(n-BinarySequence i) = i by BINARI_3:36;
1 <= n by RLVECT_1:99;
then n in Seg n by FINSEQ_1:3;
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,JORDAN4:5
.= IFEQ(0,0,FALSE,TRUE) by GR_CY_1:6
.= FALSE by CQC_LANG:def 1;
hence thesis by A4,A6,BINARI_2:def 3;
suppose
A7: i < 0;
then abs(i) = -i by ABSVALUE:def 1;
then A8: abs(i) <= --2 to_power (n-'1) by A1,REAL_1:50;
n > n-'1 by NAT_2:11;
then A9: 2 to_power n >= 2 to_power (n-'1) by POWER:44;
then -(2 to_power n) <= -(2 to_power (n-'1)) by REAL_1:50;
then -(2 to_power n) <= i by A1,AXIOMS:22;
then -(2 to_power n) - i <= i-i by REAL_1:49;
then -(2 to_power n) - i <= 0 by XCMPLX_1:14;
then -(2 to_power n + i) <= 0 by XCMPLX_1:161;
then A10: 2 to_power n + i >= 0 by REAL_1:26,50;
then reconsider k = 2 to_power n + i as Nat by INT_1:16;
abs(i) <= 2 to_power n by A8,A9,AXIOMS:22;
then MajP(n,abs(i)) = n by Th24;
then A11: 2sComplement(n,i) = n-BinarySequence(abs(k)) by A7,Def2
.= n-BinarySequence(k) by A10,ABSVALUE:def 1;
A12: 2 to_power n + i < 2 to_power n + 0 by A7,REAL_1:53;
2 to_power n + -(2 to_power (n-'1)) =
2 to_power n - (2 to_power (n-'1)) by XCMPLX_0:def 8
.= (2 to_power 1) * (2 to_power (n-'1)) - (2 to_power (n-'1))
by A2,NAT_2:12
.= 2*(2 to_power (n-'1)) - (2 to_power (n-'1)) by POWER:30
.= 2 to_power (n-'1)+(2 to_power (n-'1))-(2 to_power (n-'1))
by XCMPLX_1:11
.= 2 to_power (n-'1) by XCMPLX_1:26;
then A13: k >= 2 to_power (n-'1) by A1,AXIOMS:24;
k < 2 to_power n + 0 by A7,REAL_1:67;
then k < (2 to_power 1) * (2 to_power (n-'1)) by A2,NAT_2:12;
then k < 2*(2 to_power (n-'1)) by POWER:30;
then A14: k < 2 to_power (n-'1) + (2 to_power (n-'1)) by XCMPLX_1:11;
n in Seg n by A2,FINSEQ_1:3;
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 A13,A14,NAT_2:22
.= IFEQ(1,0,FALSE,TRUE) by GROUP_4:102
.= TRUE by CQC_LANG:def 1;
then Intval(2sComplement(n,i)) = Absval(n-BinarySequence(k)) - 2 to_power
n
by A11,BINARI_2:def 3,MARGREL1:38
.= k - 2 to_power n by A12,BINARI_3:36
.= 2 to_power n - 2 to_power n + i by XCMPLX_1:29
.= 0 + i by XCMPLX_1:14;
hence thesis;
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
A1: k mod n = l mod n & k > l;
n >= 0 + 1 by RLVECT_1:99;
then A2:n > 0 & n <> 0 by NAT_1:38;
then A3: l = (l div n)*n + (l mod n) by NAT_1:47;
A4: k = (k div n)*n + (l mod n) by A1,A2,NAT_1:47;
consider m be Nat such that
A5: k = l + m by A1,NAT_1:28;
l + m - l = k + -l by A5,XCMPLX_0:def 8;
then l - l + m = k + -l by XCMPLX_1:29;
then 0 + m = k + -l by XCMPLX_1:14;
then m = (k div n)*n + (l mod n) - ((l div n)*n + (l mod n))
by A3,A4,XCMPLX_0:def 8
.= (k div n)*n - (l div n)*n by XCMPLX_1:32
.= ((k div n) - (l div n))*n by XCMPLX_1:40;
then m mod n = (((k div n) - (l div n))*n) mod n by SCMFSA9A:5
.= 0 by Th20;
then (l+m) div n = (l div n) + (m div n) by GROUP_4:106;
then A6: k = ((l div n) + (m div n))*n + (l mod n) by A1,A2,A5,NAT_1:47
.= (m div n)*n + (l div n)*n + (l mod n) by XCMPLX_1:8
.= (m div n)*n + ((l div n)*n + (l mod n)) by XCMPLX_1:1
.= (m div n)*n + l by A2,NAT_1:47;
take m div n;
thus thesis by A6;
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 AXIOMS:21;
suppose
A2: k = l;
set s = 0;
k = l + s*n by A2;
hence thesis;
suppose
A3: k > l or l > k;
now per cases by A3;
suppose
k > l;
hence thesis by A1,Lm1;
suppose
k < l;
then consider t be Integer such that
A4: l = k + t*n by A1,Lm1;
k = l + -(t*n) by A4,XCMPLX_1:137;
then k = l + (-t)*n by XCMPLX_1:175;
hence thesis;
end;
hence thesis;
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 & k mod 2 to_power n = l mod 2 to_power n;
2 to_power n = 2 |^ n by POWER:46;
then 2 to_power n is non empty by PREPOWER:12;
then consider s be Integer such that
A2: k = l + s*(2 to_power n) by A1,Lm2;
consider j be Nat such that
A3: n = m + j by A1,NAT_1:28;
set M = 2 to_power m, J = 2 to_power j;
reconsider L = l as Integer;
A4:M > 0 by POWER:39;
A5:L div M = l div M by SCMFSA9A:5;
A6:n - m = m - m + j by A3,XCMPLX_1:29
.= 0 + j by XCMPLX_1:14;
m + -m < n + -m by A1,REAL_1:67;
then m - m < n + -m by XCMPLX_0:def 8;
then m - m < n - m by XCMPLX_0:def 8;
then 0 < j by A6,XCMPLX_1:14;
then 0 + 1 < j + 1 by REAL_1:67;
then 1 <= j by NAT_1:38;
then 2 to_power 1 divides 2 to_power j by NAT_2:13;
then 2 divides 2 to_power j by POWER:30;
then A7:J mod 2 = 0 by PEPIN:6;
A8:(s*J) mod 2 = ((s mod 2) * ((J qua Integer) mod 2)) mod 2 by INT_3:15
.= ((s mod 2) * 0) mod 2 by A7,SCMFSA9A:5
.= 0 mod 2 by SCMFSA9A:5
.= 0 by GR_CY_1:6;
k div M
= (l + s*(2 to_power (j+m))) div M by A2,A3,SCMFSA9A:5
.= (l + s*(J*M)) div M by POWER:32
.= (l + s*J*M) div M by XCMPLX_1:4
.= (L div M) + s*J by A4,INT_3:8
.= (l div M) + s*J by SCMFSA9A:5;
then (k div M) mod 2 = ((l div M) + s*J) mod 2 by SCMFSA9A:5
.= ((L div M) + s*J) mod 2 by SCMFSA9A:5
.= ((L div M) mod 2 + 0) mod 2 by A8,INT_3:14
.= (L div M) mod 2 by INT_3:13;
hence thesis by A5,SCMFSA9A:5;
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,abs h))+h) mod 2 to_power n =
((2 to_power MajP(n,abs 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;
A2:2 to_power n > 0 & 2 to_power n is Nat by POWER:39;
reconsider M = 2 to_power MajP(n,abs h) as Integer;
n <= MajP(n,abs h) by Def1;
then consider x be Nat such that
A3: MajP(n,abs h) = n + x by NAT_1:28;
M = (2 to_power n)*(2 to_power x) by A3,POWER:32;
then A4:M mod 2 to_power n =
((2 to_power n)*(2 to_power x)) mod 2 to_power n by SCMFSA9A:5
.= (((2 to_power n) mod (2 to_power n)) * (2 to_power x)) mod 2 to_power n
by EULER_2:10
.= (0 * (2 to_power x)) mod 2 to_power n by GR_CY_1:5
.= 0 by GR_CY_1:6;
reconsider L = 2 to_power MajP(n,abs i) as Integer;
n <= MajP(n,abs i) by Def1;
then consider y be Nat such that
A5: MajP(n,abs i) = n + y by NAT_1:28;
L = (2 to_power n)*(2 to_power y) by A5,POWER:32;
then A6:L mod 2 to_power n =
((2 to_power n)*(2 to_power y)) mod 2 to_power n by SCMFSA9A:5
.= (((2 to_power n) mod (2 to_power n)) * (2 to_power y)) mod 2 to_power n
by EULER_2:10
.= (0 * (2 to_power y)) mod 2 to_power n by GR_CY_1:5
.= 0 by GR_CY_1:6;
A7:(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 A2,INT_3:14
.= (h mod 2 to_power n) mod 2 to_power n by A4;
(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 A2,INT_3:14
.= (i mod 2 to_power n) mod 2 to_power n by A6;
hence thesis by A1,A7;
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 & h mod 2 to_power n = i mod 2 to_power n;
A2:2sComplement(n,h) = n-BinarySequence(abs(h)) by A1,Def2;
A3:2sComplement(n,i) = n-BinarySequence(abs(i)) by A1,Def2;
for j be Nat st j in Seg n holds
(n-BinarySequence(abs(h))).j = (n-BinarySequence(abs(i))).j
proof
let j be Nat such that
A4: j in Seg n;
A5: 1 <= j & j <= n by A4,FINSEQ_1:3;
then j - 1 >= 1 - 1 by REAL_1:49;
then j-'1 = j - 1 by BINARITH:def 3;
then j-'1 < j by INT_1:26;
then A6: j-'1 < n by A5,AXIOMS:22;
abs h = h & abs i = i &
2 to_power n > 0 by A1,ABSVALUE:def 1,POWER:39;
then A7: abs(h) mod 2 to_power n = h mod 2 to_power n &
abs(i) mod 2 to_power n = i mod 2 to_power n &
h mod 2 to_power n >= 0 & i mod 2 to_power n >= 0
by INT_3:9,SCMFSA9A:5;
A8: len(n-BinarySequence(abs(h))) = n &
len(n-BinarySequence(abs(i))) = n by FINSEQ_2:109;
then A9: (n-BinarySequence(abs(h))).j =
(n-BinarySequence(abs(h)))/.j by A5,FINSEQ_4:24
.= IFEQ((abs(h) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
by A4,BINARI_3:def 1
.= IFEQ((abs(i) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
by A1,A6,A7,Lm3;
(n-BinarySequence(abs(i))).j =
(n-BinarySequence(abs(i)))/.j by A5,A8,FINSEQ_4:24
.= IFEQ((abs(i) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
by A4,BINARI_3:def 1;
hence thesis by A9;
end;
hence thesis by A2,A3,FINSEQ_2:139;
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 & i < 0 & h mod 2 to_power n = i mod 2 to_power n;
A2:2sComplement(n,h) =
n-BinarySequence(abs((2 to_power MajP(n,abs(h)))+h)) by A1,Def2;
A3:2sComplement(n,i) =
n-BinarySequence(abs((2 to_power MajP(n,abs(i)))+i)) by A1,Def2;
abs h = -h by A1,ABSVALUE:def 1;
then 2 to_power MajP(n,abs h) >= -h by Def1;
then 2 to_power MajP(n,abs h) + h >= -h+h by AXIOMS:24;
then A4:2 to_power MajP(n,abs h) + h >= 0 by XCMPLX_0:def 6;
then reconsider H = 2 to_power MajP(n,abs h) + h as Nat by INT_1:16;
abs i = -i by A1,ABSVALUE:def 1;
then 2 to_power MajP(n,abs i) >= -i by Def1;
then 2 to_power MajP(n,abs i) + i >= -i+i by AXIOMS:24;
then A5:2 to_power MajP(n,abs i) + i >= 0 by XCMPLX_0:def 6;
then reconsider I = 2 to_power MajP(n,abs i) + i as Nat by INT_1:16;
H mod (2 to_power n) = (H qua Integer) mod (2 to_power n) &
I mod (2 to_power n) = (I qua Integer) mod (2 to_power n) by SCMFSA9A:5;
then A6:(H qua Nat) mod (2 to_power n) = (I qua Nat) mod (2 to_power n) by A1,
Lm4;
for j be Nat st j in Seg n holds
(n-BinarySequence(abs H)).j = (n-BinarySequence(abs I)).j
proof
let j be Nat such that
A7: j in Seg n;
A8: 1 <= j & j <= n by A7,FINSEQ_1:3;
A9: len(n-BinarySequence(H)) = n &
len(n-BinarySequence(I)) = n by FINSEQ_2:109;
j - 1 >= 1 - 1 by A8,REAL_1:49;
then j-'1 = j - 1 by BINARITH:def 3;
then j-'1 < j by INT_1:26;
then A10: j-'1 < n by A8,AXIOMS:22;
abs H = H & abs I = I by A4,A5,ABSVALUE:def 1;
then (n-BinarySequence(abs H)).j
= (n-BinarySequence(H))/.j by A8,A9,FINSEQ_4:24
.= 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 A6,A10,Lm3
.= (n-BinarySequence(I))/.j by A7,BINARI_3:def 1
.= (n-BinarySequence(I)).j by A8,A9,FINSEQ_4:24;
hence thesis by A5,ABSVALUE:def 1;
end;
hence thesis by A2,A3,FINSEQ_2:139;
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)) & h,i are_congruent_mod 2 to_power n
;
2 to_power n > 0 by POWER:39;
then h mod 2 to_power n = i mod 2 to_power n by A1,INT_3:12;
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;
A2:(l qua Integer) mod 2 to_power n
= l mod 2 to_power n by SCMFSA9A:5
.= (m qua Integer) mod 2 to_power n by A1,SCMFSA9A:5;
A3:l >= 0 & m >= 0 by NAT_1:18;
then abs l = l & abs m = m by ABSVALUE:def 1;
then 2sComplement(n,l) = n-BinarySequence(l) &
2sComplement(n,m) = n-BinarySequence(m) by A3,Def2;
hence thesis by A2,A3,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 such that
A1:l,m are_congruent_mod 2 to_power n;
2 to_power n > 0 by POWER:39;
then (l qua Integer) mod 2 to_power n
= (m qua Integer) mod 2 to_power n by A1,INT_3:12;
then l mod 2 to_power n
= (m qua Integer) mod 2 to_power n by SCMFSA9A:5
.= m mod 2 to_power n by SCMFSA9A:5;
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 & j <= n;
A2:j in Seg n by A1,FINSEQ_1:3;
n <= n+1 by NAT_1:29;
then j <= n+1 by A1,AXIOMS:22;
then A3:j in Seg (n+1) by A1,FINSEQ_1:3;
set M = abs( (2 to_power MajP(n+1,abs(i))) + i );
set N = abs( (2 to_power MajP(n,abs(i))) + i );
A4:i < 0 implies
(M div 2 to_power (j-'1)) mod 2 = (N div 2 to_power (j-'1)) mod 2
proof
assume
A5: i < 0;
n + 1 >= n by NAT_1:29;
then MajP(n+1,abs(i)) >= MajP(n,abs(i)) by Th22;
then consider m be Nat such that
A6: MajP(n+1,abs(i)) = MajP(n,abs(i)) + m by NAT_1:28;
set P = MajP(n,abs(i));
set Q = 2 to_power P;
2 to_power (MajP(n+1,abs(i))) >= abs i by Def1;
then 2 to_power (MajP(n+1,abs(i))) >= -i by A5,ABSVALUE:def 1;
then 2 to_power (MajP(n+1,abs(i))) + i >= -i + i by AXIOMS:24;
then 2 to_power (MajP(n+1,abs(i))) + i >= i - i by XCMPLX_0:def 8;
then 2 to_power (MajP(n+1,abs(i))) + i >= 0 by XCMPLX_1:14;
then A7: M = 2 to_power (P+m) + i by A6,ABSVALUE:def 1
.= (Q * 2 to_power m)+i by POWER:32;
A8: Q > 0 by POWER:39;
A9: (Q * 2 to_power m qua Integer) mod Q
= (Q * 2 to_power m) mod Q by SCMFSA9A:5
.= 0 by GROUP_4:101;
A10: M mod Q = ((Q * 2 to_power m)+i) mod Q by A7,SCMFSA9A:5
.= (((Q * 2 to_power m qua Integer) mod Q) +
(i mod Q)) mod Q by A8,INT_3:14
.= (i mod Q) mod Q by A9;
A11: (Q qua Integer) mod Q = Q mod Q by SCMFSA9A:5
.= 0 by GR_CY_1:5;
Q >= abs i by Def1;
then Q >= -i by A5,ABSVALUE:def 1;
then Q + i >= -i + i by AXIOMS:24;
then Q + i >= i - i by XCMPLX_0:def 8;
then Q + i >= 0 by XCMPLX_1:14;
then N = Q + i by ABSVALUE:def 1;
then A12: N mod Q =(Q + i) mod Q by SCMFSA9A:5
.= (((Q qua Integer) mod Q) + (i mod Q)) mod Q by A8,INT_3:14
.= (i mod Q) mod Q by A11;
A13:P >= n by Def1;
j + -1 >= 1 + -1 by A1,AXIOMS:24;
then A14:j - 1 >= 0 by XCMPLX_0:def 8;
then A15:j -' 1 = j - 1 by BINARITH:def 3;
then j -' 1 < j by INT_1:26;
then j -' 1 < n by A1,AXIOMS:22;
then j -' 1 < P by A13,AXIOMS:22;
hence thesis by A10,A12,A14,A15,Lm3;
end;
per cases;
suppose
A16: i >= 0;
then reconsider i as Nat by INT_1:16;
A17: 2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(abs i))/.j by A16,Def2
.= ((n+1)-BinarySequence(i))/.j by A16,ABSVALUE:def 1
.= IFEQ((i div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A3,BINARI_3:def 1
;
2sComplement(n,i)/.j = (n-BinarySequence(abs i))/.j by A16,Def2
.= (n-BinarySequence(i))/.j by A16,ABSVALUE:def 1
.= IFEQ((i div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,BINARI_3:def 1
;
hence thesis by A17;
suppose
A18: i < 0;
then A19: 2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(M))/.j by Def2
.= IFEQ((M div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A3,BINARI_3:def 1
;
2sComplement(n,i)/.j = (n-BinarySequence(N))/.j by A18,Def2
.= IFEQ((N div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,BINARI_3:def 1
;
hence thesis by A4,A18,A19;
end;
theorem Th33:
ex x be Element of BOOLEAN st
2sComplement(m+1,i) = 2sComplement(m,i)^<*x*>
proof
consider a be (Tuple of m,BOOLEAN), b be Element of BOOLEAN such that
A1: 2sComplement(m+1,i) = a^<*b*> by FINSEQ_2:137;
now per cases by NAT_1:19;
suppose m > 0;
then reconsider m as non empty Nat;
for j be Nat st j in Seg m holds
2sComplement(m,i).j = a.j
proof
let j be Nat such that
A2: j in Seg m;
A3: len 2sComplement(m+1,i) = m+1 & len 2sComplement(m,i) = m &
len a = m by FINSEQ_2:109;
A4: 1 <= j & j <= m by A2,FINSEQ_1:3;
m <= m + 1 by NAT_1:29;
then j <= m + 1 by A4,AXIOMS:22;
then A5: 2sComplement(m+1,i).j = 2sComplement(m+1,i)/.j by A3,A4,FINSEQ_4:24
.= 2sComplement(m,i)/.j by A4,Th32
.= 2sComplement(m,i).j by A3,A4,FINSEQ_4:24;
j in dom a by A2,A3,FINSEQ_1:def 3;
hence thesis by A1,A5,FINSEQ_1:def 7;
end;
then a = 2sComplement(m,i) by FINSEQ_2:139;
hence thesis by A1;
suppose
A6: m = 0;
then A7: 2sComplement(m,i) = <*>BOOLEAN by FINSEQ_2:113
.= {};
reconsider E = {} as FinSequence by FINSEQ_1:14;
consider c be Element of BOOLEAN such that
A8: 2sComplement(m+1,i) = <*c*> by A6,FINSEQ_2:117;
2sComplement(m+1,i) = E^<*c*> by A8,FINSEQ_1:47;
hence thesis by A7;
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 >= 0 by NAT_1:18;
then A3:abs l = l by ABSVALUE:def 1;
then (m+1)-BinarySequence(l)
= 2sComplement(m,l)^<*x*> by A1,A2,Def2
.= (m-BinarySequence(l))^<*x*> by A2,A3,Def2;
hence thesis;
end;
theorem Th35:
for n be non empty 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: _P[1] proof
assume
A2: -2 to_power 1 <= h+i & h < 0 & i < 0 &
-2 to_power (1-'1) <= h & -2 to_power (1-'1) <= i;
then -2 to_power 1 < h & -2 to_power 1 < i by Th9;
then A3: -2 < h & -2 < i by POWER:30;
-2+1 = -1;
then A4: -1 <= h & -1 <= i by A3,INT_1:20;
h <= -1 & i <= -1 by A2,INT_1:21;
then A5: h = -1 & i = -1 by A4,AXIOMS:21;
then abs h = --1 & abs i = --1 by ABSVALUE:def 1;
then 2 to_power 0 = abs h & 2 to_power 2 > 2 to_power 0 by POWER:29,44;
then A6: MajP(2,abs h) = 2 by Th24;
2 to_power 2 = 2 |^ (1+1) by POWER:46
.= 2 |^ 1 + 2 |^ 1 by PEPIN:30
.= 2 to_power 1 + 2 |^ 1 by POWER:46
.= 2 to_power 1 + 2 to_power 1 by POWER:46
.= 2 + 2 to_power 1 by POWER:30
.= 2 + 2 by POWER:30;
then A7: abs(2 to_power MajP(2,abs h) + h)
= 3 by A5,A6,ABSVALUE:def 1;
1-'1 = 1-1 by BINARITH:def 3;
then 3 div 2 to_power (1-'1)
= (1+2) div 1 by POWER:29
.= 3 by NAT_2:6;
then A8:(3 div 2 to_power (1-'1)) mod 2 = (2+1) mod 2
.= ((2 mod 2) + 1) mod 2 by GR_CY_1:2
.= (0 + 1) mod 2 by GR_CY_1:5
.= (1 qua Integer) mod 2 by SCMFSA9A:5
.= 1 by PEPIN:5;
A9:1 in Seg 2 by FINSEQ_1:3;
A10:(2sComplement(2,h))/.1 = (2-BinarySequence(3))/.1 by A2,A7,Def2
.= IFEQ(1,0,FALSE,TRUE) by A8,A9,BINARI_3:def 1
.= TRUE by CQC_LANG:def 1;
set H = 2sComplement(2,h), I = 2sComplement(2,i), T = TRUE;
carry(H,I)/.(1+1)
= T '&' T 'or' T '&' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1)
by A5,A10,BINARITH:def 5
.= T 'or' T '&' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1) by MARGREL1:45
.= T 'or' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1) by MARGREL1:50
.= T 'or' (carry(H,I)/.1) 'or' (carry(H,I)/.1) by MARGREL1:50
.= T 'or' (carry(H,I)/.1) by Th17;
hence thesis by Th17;
end;
A11:for n be non empty Nat st _P[n] holds _P[n+1]
proof
let n be non empty Nat such that _P[n];
assume
A12: -2 to_power (n+1) <= h+i & h < 0 & i < 0 &
-2 to_power (n+1-'1) <= h & -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;
A13: N-1 = n by XCMPLX_1:26;
A14:0 <= n by NAT_1:18;
then A15: N-'1 = N-1 by A13,BINARITH:def 3;
A16:N-'1 = n by A13,A14,BINARITH:def 3;
N-1 < N by INT_1:26;
then A17: 2 to_power (N-'1) < 2 to_power N by A15,POWER:44;
2 to_power (N-'1) + 2 to_power (N-'1) = 2*(2 to_power (N-'1)) by XCMPLX_1
:11
.= (2 to_power 1)*(2 to_power (N-'1)) by POWER:30
.= 2 to_power (1+(N-1)) by A15,POWER:32
.= 2 to_power (1+(N+-1)) by XCMPLX_0:def 8
.= 2 to_power (1+N+-1) by XCMPLX_1:1
.= 2 to_power (1+N-1) by XCMPLX_0:def 8
.= 2 to_power (1-1+N) by XCMPLX_1:29
.= 2 to_power (0+N);
then A18: -2 to_power (N-'1) + 2 to_power N
= (-2 to_power (N-'1) + 2 to_power (N-'1)) + 2 to_power (N-'1)
by XCMPLX_1:1
.= -(2 to_power (N-'1) - 2 to_power (N-'1)) + 2 to_power (N-'1)
by XCMPLX_1:162
.= -0 + 2 to_power (N-'1) by XCMPLX_1:14
.= 2 to_power (N-'1);
abs h = -h & abs i = -i by A12,ABSVALUE:def 1;
then --2 to_power (N-'1) >= abs h & --2 to_power (N-'1) >= abs i
by A12,REAL_1:50;
then abs h < 2 to_power N & abs i < 2 to_power N by A17,AXIOMS:22;
then A19: MajP(N,abs h) = N & MajP(N,abs i) = N by Th24;
A20: 2 to_power (N-'1) <= 2 to_power N + h &
2 to_power (N-'1) <= 2 to_power N + i
by A12,A18,AXIOMS:24;
2 to_power n > 0 by POWER:39;
then A21: 0 <= 2 to_power N + h & 0 <= 2 to_power N + i by A16,A20,AXIOMS:22;
then reconsider NH = 2 to_power N + h,
NI = 2 to_power N + i as Nat by INT_1:16;
A22: 1 <= N & len (N-BinarySequence(NH)) = N & len(N-BinarySequence(NI)) = N
by FINSEQ_2:109,NAT_1:29;
A23: 2 to_power N + h < 0 + 2 to_power N &
2 to_power N + i < 0 + 2 to_power N by A12,REAL_1:67;
A24: H/.N = (N-BinarySequence(abs NH))/.N by A12,A19,Def2
.= (N-BinarySequence(NH))/.N by A21,ABSVALUE:def 1
.= (N-BinarySequence(NH)).N by A22,FINSEQ_4:24
.= T by A16,A20,A23,BINARI_3:30;
A25: I/.N = (N-BinarySequence(abs NI))/.N by A12,A19,Def2
.= (N-BinarySequence(NI))/.N by A21,ABSVALUE:def 1
.= (N-BinarySequence(NI)).N by A22,FINSEQ_4:24
.= T by A16,A20,A23,BINARI_3:30;
A26: H1/.N = H/.N & I1/.N = I/.N by A22,Th32;
N < N+1 by NAT_1:38;
then carry(H1,I1)/.(N+1) = T '&' T 'or' T '&' (carry(H1,I1)/.N) 'or'
T '&' (carry(H1,I1)/.N) by A22,A24,A25,A26,BINARITH:def 5
.= T 'or' T '&' (carry(H1,I1)/.N) 'or' T '&' (carry(H1,I1)/.N)
by MARGREL1:45
.= T 'or' (carry(H1,I1)/.N) 'or' T '&' (carry(H1,I1)/.N) by MARGREL1:50
.= T 'or' (carry(H1,I1)/.N) 'or' (carry(H1,I1)/.N) by MARGREL1:50
.= T 'or' (carry(H1,I1)/.N) by Th17;
hence thesis by Th17;
end;
thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A11);
end;
theorem
for n be non empty Nat st
-(2 to_power (n-'1)) <= h + i & 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 empty Nat such that
A1: -(2 to_power (n-'1)) <= h + i & h + i <= 2 to_power (n-'1) - 1 &
h >= 0 & i >= 0;
reconsider h,i as Nat by A1,INT_1:16;
A2: 2sComplement(n,h) = n-BinarySequence(abs h) by A1,Def2
.= n-BinarySequence(h) by A1,ABSVALUE:def 1;
2sComplement(n,i) = n-BinarySequence(abs i) by A1,Def2
.= n-BinarySequence(i) by A1,ABSVALUE:def 1;
hence thesis by A1,A2,Th14;
end;
theorem
for n be non empty Nat st
-2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
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 empty Nat such that
A1: -2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
h < 0 & i < 0 & -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i;
set H = 2sComplement(n,h), I = 2sComplement(n,i),
H1 = 2sComplement(n+1,h), I1 = 2sComplement(n+1,i),
F = FALSE, T = TRUE;
(n+1)-1 = n & n >= 0 by NAT_1:18,XCMPLX_1:26;
then A2:-2 to_power n <= h+i & h+i <= 2 to_power n - 1 by A1,BINARITH:def 3;
then A3:-2 to_power n < h & -2 to_power n < i by A1,Th9;
then -h < --2 to_power n & -i < --2 to_power n by REAL_1:50;
then A4:abs h < 2 to_power n & abs i < 2 to_power n by A1,ABSVALUE:def 1;
n < n+1 by REAL_1:69;
then 2 to_power n < 2 to_power (n+1) by POWER:44;
then abs h < 2 to_power (n+1) & abs i < 2 to_power (n+1) by A4,AXIOMS:22;
then A5:MajP(n+1,abs h) = n+1 & MajP(n+1,abs i) = n+1 by Th24;
A6:2 to_power (n+1) + h < 2 to_power (n+1) + 0 &
2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A1,REAL_1:67;
2 to_power (n+1) + -(2 to_power n)
= -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
.= -(2 to_power n) + 2*(2 to_power n) by POWER:30
.= 2 to_power n by XCMPLX_1:184;
then A7:2 to_power n <= 2 to_power (n+1) + h &
2 to_power n <= 2 to_power (n+1) + i by A3,AXIOMS:24;
2 to_power n > 0 by POWER:39;
then A8:0 <= 2 to_power (n+1) + h &
0 <= 2 to_power (n+1) + i by A7,AXIOMS:22;
then reconsider NH = 2 to_power (n+1) + h,
NI = 2 to_power (n+1) + i as Nat by INT_1:16;
consider a be Element of BOOLEAN such that
A9: H1 = H^<*a*> by Th33;
consider a be Element of BOOLEAN such that
A10: I1 = I^<*a*> by Th33;
A11: len H1 = n + 1 & len I1 = n + 1 by FINSEQ_2:109;
A12: 1 <= n + 1 by NAT_1:29;
then A13: H1/.(n+1) = H1.(n+1) by A11,FINSEQ_4:24
.= ((n+1)-BinarySequence(abs(2 to_power (n+1)+h))).(n+1) by A1,A5,Def2
.= ((n+1)-BinarySequence(NH)).(n+1) by A8,ABSVALUE:def 1
.= T by A6,A7,BINARI_3:30;
A14: I1/.(n+1) = I1.(n+1) by A11,A12,FINSEQ_4:24
.= ((n+1)-BinarySequence(abs(2 to_power (n+1)+i))).(n+1) by A1,A5,Def2
.= ((n+1)-BinarySequence(NI)).(n+1) by A8,ABSVALUE:def 1
.= T by A6,A7,BINARI_3:30;
A15: H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A1,A5,Def2
.= (n+1)-BinarySequence(NH) by A8,ABSVALUE:def 1;
A16: I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A1,A5,Def2
.= (n+1)-BinarySequence(NI) by A8,ABSVALUE:def 1;
A17: Intval(H1) = Absval(H1) - 2 to_power (n+1)
by A13,BINARI_2:def 3,MARGREL1:38
.= NH - 2 to_power (n+1) by A6,A15,BINARI_3:36
.= h by XCMPLX_1:26;
A18: Intval(I1) = Absval(I1) - 2 to_power (n+1)
by A14,BINARI_2:def 3,MARGREL1:38
.= NI - 2 to_power (n+1) by A6,A16,BINARI_3:36
.= i by XCMPLX_1:26;
A19: carry(H1,I1)/.(n+1) = T by A1,A2,Th35;
then A20: Int_add_ovfl(H1,I1)
= 'not' T '&' 'not' T '&' T by A13,A14,BINARI_2:def 4
.= F '&' 'not' T '&' T by MARGREL1:41
.= F '&' T by MARGREL1:45
.= F by MARGREL1:45;
Int_add_udfl(H1,I1)
= T '&' T '&' 'not' T by A13,A14,A19,BINARI_2:def 5
.= T '&' 'not' T by MARGREL1:45
.= F by MARGREL1:46;
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 A9,A10,A17,A18,A20,BINARI_2:14
.= h + i - 0 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
.= h + i - 0 + 0 by CQC_LANG:def 1;
hence thesis;
end;
theorem
for n be non empty 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 empty 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: _P[1] proof
assume
A2: -(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));
1 -' 1 = 1 - 1 by BINARITH:def 3
.= 0;
then A3:-1 <= h & h <= 1-1 & -1 <= i & i <= 1-1 &
-1 <= h+i & h+i <= 1-1 by A2,POWER:29;
A4: 2sComplement(1,0) = 1-BinarySequence(abs 0) by Def2
.= 1-BinarySequence(0) by ABSVALUE:def 1
.= 0*1 by BINARI_3:26
.= 1 |-> (0 qua Real) by EUCLID:def 4
.= <* FALSE *> by FINSEQ_2:73,MARGREL1:36;
A5:2 to_power 1 = 2 & (for k be Nat st 2 to_power k >= 1 & k >= 1 holds
k >= 1) by POWER:30;
abs(-1) = --1 by ABSVALUE:def 1
.= 1;
then A6: MajP(1,abs(-1)) = 1 by A5,Def1;
A7: 0*0 = 0 |-> (0 qua Real) by EUCLID:def 4
.= {} by FINSEQ_2:72;
A8: 2sComplement(1,-1)
= 1-BinarySequence(abs((2 to_power 1)+-1)) by A6,Def2
.= 1-BinarySequence(abs(2+-1)) by POWER:30
.= 1-BinarySequence(1) by ABSVALUE:def 1
.= (0+1)-BinarySequence(2 to_power 0) by POWER:29
.= (0*0)^<*1*> by ARMSTRNG:7
.= <*TRUE*> by A7,FINSEQ_1:47,MARGREL1:36;
now per cases by A2;
suppose
h >= 0 & i < 0;
then A9: h = 0 & i <= -1 by A3,INT_1:21;
then i = -1 by A3,AXIOMS:21;
hence thesis by A4,A8,A9,Th15,BINARI_3:18;
suppose
A10: h < 0 & i >= 0;
then h <= -1 by INT_1:21;
then A11: h = -1 by A3,AXIOMS:21;
i = 0 by A3,A10;
hence thesis by A4,A8,A11,Th15,BINARI_3:18;
end;
hence thesis;
end;
A12:for n be non empty Nat st _P[n] holds _P[n+1] proof
let n be non empty 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
A13: -(2 to_power ((n+1)-'1)) <= h & h <= 2 to_power ((n+1)-'1) - 1 &
-(2 to_power ((n+1)-'1)) <= i & i <= 2 to_power ((n+1)-'1) - 1 &
-(2 to_power ((n+1)-'1)) <= h+i & h+i <= 2 to_power ((n+1)-'1) - 1 &
((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;
(n+1)-1 = n & n >= 0 by NAT_1:18,XCMPLX_1:26;
then A14: -n2 <= h & h <= n2 - 1 & -n2 <= i & i <= n2 - 1 &
-n2 <= h+i & h+i <= n2 - 1 by A13,BINARITH:def 3;
consider a be Element of BOOLEAN such that
A15: H1 = H^<*a*> by Th33;
consider b be Element of BOOLEAN such that
A16: I1 = I^<*b*> by Th33;
now per cases by A13;
suppose
A17: h >= 0 & i < 0;
then reconsider h as Nat by INT_1:16;
A18: H1 = (n+1)-BinarySequence(abs h) by A17,Def2
.= (n+1)-BinarySequence(h) by A17,ABSVALUE:def 1;
A19: len H1 = n+1 & len I1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:29;
2 to_power n - 1 < 2 to_power n by INT_1:26;
then A20: h < 2 to_power n by A14,AXIOMS:22;
then A21: H1.(n+1) = F by A18,BINARI_3:27;
abs i = -i by A17,ABSVALUE:def 1;
then A22: abs i <= --2 to_power n by A14,REAL_1:50;
n < n+1 by REAL_1:69;
then 2 to_power n < 2 to_power (n+1) by POWER:44;
then abs i < 2 to_power (n+1) by A22,AXIOMS:22;
then A23: MajP(n+1,abs i) = n+1 by Th24;
A24: 2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A17,REAL_1:67;
2 to_power (n+1) + -(2 to_power n)
= -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
.= -(2 to_power n) + 2*(2 to_power n) by POWER:30
.= 2 to_power n by XCMPLX_1:184;
then A25: 2 to_power n <= 2 to_power (n+1) + i by A14,AXIOMS:24;
then A26: 0 < 2 to_power (n+1) + i by POWER:39;
then reconsider NI = 2 to_power (n+1) + i as Nat by INT_1:16;
A27: I1.(n+1) = ((n+1)-BinarySequence(abs(2 to_power (n+1)+i))).(n+1)
by A17,A23,Def2
.= ((n+1)-BinarySequence(NI)).(n+1) by A26,ABSVALUE:def 1
.= T by A24,A25,BINARI_3:30;
n + 0 < n+1 by REAL_1:67;
then 2 to_power n < 2 to_power (n+1) by POWER:44;
then A28: h < 2 to_power (n+1) by A20,AXIOMS:22;
A29: H1/.(n+1) = H1.(n+1) by A19,FINSEQ_4:24;
then A30: Intval(H1) = Absval(H1) by A21,BINARI_2:def 3
.= h by A18,A28,BINARI_3:36;
A31: I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A17,A23,Def2
.= (n+1)-BinarySequence(NI) by A26,ABSVALUE:def 1;
A32: I1/.(n+1) = I1.(n+1) by A19,FINSEQ_4:24;
then A33: Intval(I1) = Absval(I1) - 2 to_power (n+1)
by A27,BINARI_2:def 3,MARGREL1:38
.= NI - 2 to_power (n+1) by A24,A31,BINARI_3:36
.= i by XCMPLX_1:26;
A34: Int_add_ovfl(H1,I1) = 'not' F '&' 'not' T '&' (carry(H1,I1)/.(n+1))
by A21,A27,A29,A32,BINARI_2:def 4
.= T '&' 'not' T '&' (carry(H1,I1)/.(n+1)) by MARGREL1:41
.= F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:46
.= F by MARGREL1:45;
Int_add_udfl(H1,I1)
= F '&' T '&' 'not' (carry(H1,I1)/.(n+1))
by A21,A27,A29,A32,BINARI_2:def 5
.= F '&' 'not' (carry(H1,I1)/.(n+1)) by MARGREL1:45
.= F by MARGREL1:45;
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 A15,A16,A30,A33,A34,BINARI_2:14
.= h + i - 0 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
.= h + i - 0 + 0 by CQC_LANG:def 1;
hence thesis;
suppose
A35: h < 0 & i >= 0;
then reconsider i as Nat by INT_1:16;
A36: I1 = (n+1)-BinarySequence(abs i) by A35,Def2
.= (n+1)-BinarySequence(i) by A35,ABSVALUE:def 1;
A37: len I1 = n+1 & len H1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:29;
2 to_power n - 1 < 2 to_power n by INT_1:26;
then A38: i < 2 to_power n by A14,AXIOMS:22;
then A39: I1.(n+1) = F by A36,BINARI_3:27;
abs h = -h by A35,ABSVALUE:def 1;
then A40: abs h <= --2 to_power n by A14,REAL_1:50;
n < n+1 by REAL_1:69;
then 2 to_power n < 2 to_power (n+1) by POWER:44;
then abs h < 2 to_power (n+1) by A40,AXIOMS:22;
then A41: MajP(n+1,abs h) = n+1 by Th24;
A42: 2 to_power (n+1) + h < 2 to_power (n+1) + 0 by A35,REAL_1:67;
2 to_power (n+1) + -(2 to_power n)
= -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
.= -(2 to_power n) + 2*(2 to_power n) by POWER:30
.= 2 to_power n by XCMPLX_1:184;
then A43: 2 to_power n <= 2 to_power (n+1) + h by A14,AXIOMS:24;
then A44: 0 < 2 to_power (n+1) + h by POWER:39;
then reconsider NH = 2 to_power (n+1) + h as Nat by INT_1:16;
A45: H1.(n+1) = ((n+1)-BinarySequence(abs(2 to_power (n+1)+h))).(n+1)
by A35,A41,Def2
.= ((n+1)-BinarySequence(NH)).(n+1) by A44,ABSVALUE:def 1
.= T by A42,A43,BINARI_3:30;
n + 0 < n+1 by REAL_1:67;
then 2 to_power n < 2 to_power (n+1) by POWER:44;
then A46: i < 2 to_power (n+1) by A38,AXIOMS:22;
A47: I1/.(n+1) = I1.(n+1) by A37,FINSEQ_4:24;
then A48: Intval(I1) = Absval(I1) by A39,BINARI_2:def 3
.= i by A36,A46,BINARI_3:36;
A49: H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A35,A41,Def2
.= (n+1)-BinarySequence(NH) by A44,ABSVALUE:def 1;
A50: H1/.(n+1) = H1.(n+1) by A37,FINSEQ_4:24;
then A51: Intval(H1) = Absval(H1) - 2 to_power (n+1)
by A45,BINARI_2:def 3,MARGREL1:38
.= NH - 2 to_power (n+1) by A42,A49,BINARI_3:36
.= h by XCMPLX_1:26;
A52: Int_add_ovfl(H1,I1) = 'not' T '&' 'not' F '&' (carry(H1,I1)/.(n+1))
by A39,A45,A47,A50,BINARI_2:def 4
.= F '&' 'not' F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:41
.= F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:46
.= F by MARGREL1:45;
Int_add_udfl(H1,I1) = T '&' F '&' 'not' (carry(H1,I1)/.(n+1))
by A39,A45,A47,A50,BINARI_2:def 5
.= F '&' 'not' (carry(H1,I1)/.(n+1)) by MARGREL1:45
.= F by MARGREL1:45;
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 A15,A16,A48,A51,A52,BINARI_2:14
.= h + i - 0 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
.= h + i - 0 + 0 by CQC_LANG:def 1;
hence thesis;
end;
hence thesis;
end;
thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A12);
end;