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;