:: Binary Arithmetics. Binary Sequences :: by Robert Milewski :: :: Received February 24, 1998 :: Copyright (c) 1998-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, NAT_1, FINSEQ_2, MARGREL1, BINARITH, ARYTM_3, POWER, SUBSET_1, ORDINAL4, FINSEQ_1, FUNCOP_1, XBOOLEAN, CARD_1, RELAT_1, REAL_1, FINSEQ_5, EUCLID, XXREAL_0, FUNCT_1, PARTFUN1, ARYTM_1, BINARI_2, ZFMISC_1, INT_1, ABIAN, BINARI_3, XCMPLX_0; notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_D, POWER, ABIAN, SERIES_1, MARGREL1, FUNCT_1, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_5, ZFMISC_1, FINSEQ_2, BINARITH, BINARI_2, EUCLID; constructors NAT_D, FINSEQOP, SERIES_1, BINARITH, FINSEQ_5, BINARI_2, ABIAN, EUCLID, TREES_3; registrations RELSET_1, XREAL_0, NAT_1, XBOOLEAN, MARGREL1, NAT_2, ORDINAL1, XBOOLE_0, FINSEQ_2, INT_1, FINSEQ_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; equalities FINSEQ_2, EUCLID, XBOOLEAN, ORDINAL1; theorems TARSKI, NAT_1, NAT_2, MARGREL1, POWER, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, BINARITH, BINARI_2, XREAL_1, XCMPLX_1, XBOOLEAN, NAT_D, PARTFUN1, XXREAL_0, CARD_1; schemes NAT_1, NAT_2, FINSEQ_2; begin :: Binary Arithmetics theorem Th1: for n be non zero Nat for F be Tuple of n,BOOLEAN holds Absval F < 2 to_power n proof defpred P[non zero Nat] means for F be Tuple of $1,BOOLEAN holds Absval F < 2 to_power $1; A1: for n be non zero Nat st P[n] holds P[n+1] proof let n be non zero Nat; assume A2: P[n]; n < n+1 by NAT_1:13; then A3: 2 to_power n < 2 to_power (n+1) by POWER:39; let F be Tuple of n+1,BOOLEAN; consider T be Element of n-tuples_on BOOLEAN, d be Element of BOOLEAN such that A4: F = T^<*d*> by FINSEQ_2:117; A5: Absval F = Absval T + IFEQ(d,FALSE,0,2 to_power n) by A4,BINARITH:20; A6: Absval T < 2 to_power n by A2; per cases by XBOOLEAN:def 3; suppose d = FALSE; then Absval F = Absval T + 0 by A5,FUNCOP_1:def 8; then Absval F + 2 to_power n < 2 to_power n + 2 to_power (n+1) by A2,A3, XREAL_1:8; hence thesis by XREAL_1:6; end; suppose d = TRUE; then Absval F = Absval T + 2 to_power n by A5,FUNCOP_1:def 8; then Absval F < 2 to_power n + 2 to_power n by A6,XREAL_1:6; then Absval F < 2 to_power n * 2; then Absval F < 2 to_power n * 2 to_power 1 by POWER:25; hence thesis by POWER:27; end; end; A7: P[1] proof let F be Tuple of 1,BOOLEAN; consider d be Element of BOOLEAN such that A8: F = <*d*> by FINSEQ_2:97; d = TRUE or d = FALSE by XBOOLEAN:def 3; then Absval F = 1 or Absval F = 0 by A8,BINARITH:15,16; then Absval F < 2; hence thesis by POWER:25; end; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A7,A1); end; theorem Th2: for n be non zero Nat for F1,F2 be Tuple of n,BOOLEAN st Absval F1 = Absval F2 holds F1 = F2 proof defpred P[non zero Nat] means for F1,F2 be Tuple of $1,BOOLEAN st Absval F1 = Absval F2 holds F1 = F2; A1: for k be non zero Nat st P[k] holds P[k+1] proof let k be non zero Nat; assume A2: for F1,F2 be Tuple of k,BOOLEAN st Absval F1 = Absval F2 holds F1 = F2; let F1,F2 be Tuple of k+1,BOOLEAN; consider T1 be Element of k-tuples_on BOOLEAN, d1 be Element of BOOLEAN such that A3: F1 = T1^<*d1*> by FINSEQ_2:117; assume A4: Absval F1 = Absval F2; consider T2 be Element of k-tuples_on BOOLEAN, d2 be Element of BOOLEAN such that A5: F2 = T2^<*d2*> by FINSEQ_2:117; A6: Absval T1 + IFEQ(d1,FALSE,0,2 to_power k) = Absval F1 by A3,BINARITH:20 .= Absval T2 + IFEQ(d2,FALSE,0,2 to_power k) by A5,A4,BINARITH:20; d1 = d2 proof assume A7: d1 <> d2; per cases by XBOOLEAN:def 3; suppose A8: d1 = FALSE; then A9: IFEQ(d1,FALSE,0 qua Real,2 to_power k) = 0 by FUNCOP_1:def 8; IFEQ(d2,FALSE,0 qua Real,2 to_power k) = 2 to_power k by A7,A8, FUNCOP_1:def 8; hence contradiction by A6,A9,Th1,NAT_1:11; end; suppose A10: d1 = TRUE; then d2 = FALSE by A7,XBOOLEAN:def 3; then A11: IFEQ(d2,FALSE,0 qua Real,2 to_power k) = 0 by FUNCOP_1:def 8; IFEQ(d1,FALSE,0 qua Real,2 to_power k) = 2 to_power k by A10, FUNCOP_1:def 8; hence contradiction by A6,A11,Th1,NAT_1:11; end; end; hence thesis by A2,A3,A5,A6,XCMPLX_1:2; end; A12: P[1] proof let F1,F2 be Tuple of 1,BOOLEAN; consider d1 be Element of BOOLEAN such that A13: F1 = <*d1*> by FINSEQ_2:97; assume A14: Absval F1 = Absval F2; assume A15: F1 <> F2; consider d2 be Element of BOOLEAN such that A16: F2 = <*d2*> by FINSEQ_2:97; per cases by XBOOLEAN:def 3; suppose A17: d1 = FALSE; then A18: Absval F1 = 0 by A13,BINARITH:15; d2 = TRUE by A13,A16,A15,A17,XBOOLEAN:def 3; hence contradiction by A16,A14,A18,BINARITH:16; end; suppose A19: d1 = TRUE; then A20: Absval F1 = 1 by A13,BINARITH:16; d2 = FALSE by A13,A16,A15,A19,XBOOLEAN:def 3; hence contradiction by A16,A14,A20,BINARITH:15; end; end; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A12,A1); end; theorem for t1,t2 be FinSequence st Rev t1 = Rev t2 holds t1 = t2 proof let t1,t2 be FinSequence; assume A1: Rev t1 = Rev t2; thus t1 = Rev Rev t1 .= t2 by A1; end; theorem Th4: for n be Nat holds 0*n in BOOLEAN* proof let n be Nat; n |-> FALSE is FinSequence of BOOLEAN; hence thesis by FINSEQ_1:def 11; end; theorem Th5: for n be Nat for y be Tuple of n,BOOLEAN st y = 0*n holds 'not' y = n |-> 1 proof let n be Nat; let y be Tuple of n,BOOLEAN; assume A1: y = 0*n; A2: now A3: len y = n by CARD_1:def 7; let i be Nat; assume that A4: 1 <= i and A5: i <= len 'not' y; A6: len 'not' y = n by CARD_1:def 7; then A7: i in Seg n by A4,A5,FINSEQ_1:1; then A8: y.i = FALSE by A1,FUNCOP_1:7; thus ('not' y).i = ('not' y)/.i by A4,A5,FINSEQ_4:15 .= 'not' (y/.i) by A7,BINARITH:def 1 .= 'not' FALSE by A4,A5,A6,A3,A8,FINSEQ_4:15 .= (n |-> 1).i by A7,FUNCOP_1:7; end; len 'not' y = n by CARD_1:def 7 .= len (n |-> 1) by CARD_1:def 7; hence thesis by A2,FINSEQ_1:14; end; theorem Th6: for n be non zero Nat for F be Tuple of n,BOOLEAN st F = 0*n holds Absval F = 0 proof defpred P[Nat] means for F be Tuple of $1,BOOLEAN st F = 0*$1 holds Absval F = 0; A1: for n be non zero Nat st P[n] holds P[n+1] proof let n be non zero Nat; assume A2: for F be Tuple of n,BOOLEAN st F = 0*n holds Absval F = 0; let F be Tuple of n+1,BOOLEAN; 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider F1 = 0*n as Tuple of n,BOOLEAN; assume F = 0*(n+1); hence Absval F = Absval(F1 ^ <*FALSE*>) by FINSEQ_2:60 .= Absval(F1) + IFEQ(FALSE,FALSE,0,2 to_power n) by BINARITH:20 .= 0 + IFEQ(FALSE,FALSE,0,2 to_power n) by A2 .= 0 by FUNCOP_1:def 8; end; A3: P[1] by BINARITH:15,FINSEQ_2:59; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A3,A1); end; theorem for n be non zero Nat for F be Tuple of n,BOOLEAN st F = 0*n holds Absval 'not' F = 2 to_power n - 1 proof let n be non zero Nat; let F be Tuple of n,BOOLEAN; assume A1: F = 0*n; thus Absval 'not' F = - Absval F + 2 to_power n - 1 by BINARI_2:13 .= - 0 + 2 to_power n - 1 by A1,Th6 .= 2 to_power n - 1; end; theorem for n be Nat holds Rev (0*n) = 0*n proof let n be Nat; A1: now let k be Nat; assume A2: k in dom 0*n; then k in Seg len 0*n by FINSEQ_1:def 3; then A3: k in Seg n by CARD_1:def 7; then n - k + 1 in Seg n by FINSEQ_5:2; then A4: len 0*n - k + 1 in Seg n by CARD_1:def 7; thus (Rev 0*n).k = (0*n).(len 0*n - k + 1) by A2,FINSEQ_5:58 .= 0 by A4,FUNCOP_1:7 .= (0*n).k by A3,FUNCOP_1:7; end; dom Rev (0*n) = Seg len Rev (0*n) by FINSEQ_1:def 3 .= Seg len 0*n by FINSEQ_5:def 3 .= dom 0*n by FINSEQ_1:def 3; hence thesis by A1,FINSEQ_1:13; end; theorem for n be Nat for y be Tuple of n,BOOLEAN st y = 0*n holds Rev 'not' y = 'not' y proof let n be Nat; let y be Tuple of n,BOOLEAN; assume A1: y = 0*n; A2: now let k be Nat; assume A3: k in dom 'not' y; then k in Seg len 'not' y by FINSEQ_1:def 3; then A4: k in Seg n by CARD_1:def 7; then n - k + 1 in Seg n by FINSEQ_5:2; then A5: len 'not' y - k + 1 in Seg n by CARD_1:def 7; thus (Rev 'not' y).k = ('not' y).(len 'not' y - k + 1) by A3,FINSEQ_5:58 .= (n |-> 1).(len 'not' y - k + 1) by A1,Th5 .= 1 by A5,FUNCOP_1:7 .= (n |-> 1).k by A4,FUNCOP_1:7 .= ('not' y).k by A1,Th5; end; dom Rev 'not' y = Seg len Rev 'not' y by FINSEQ_1:def 3 .= Seg len 'not' y by FINSEQ_5:def 3 .= dom 'not' y by FINSEQ_1:def 3; hence thesis by A2,FINSEQ_1:13; end; theorem Th10: Bin1 1 = <*TRUE*> proof 1 in Seg 1 by FINSEQ_1:3; then A1: (Bin1 1)/.1 = TRUE by BINARI_2:5; ex d be Element of BOOLEAN st Bin1 1 = <*d*> by FINSEQ_2:97; hence thesis by A1,FINSEQ_4:16; end; theorem Th11: for n be non zero Nat holds Absval (Bin1 n) = 1 proof defpred P[Nat] means Absval (Bin1 $1) = 1; A1: for n be non zero Nat st P[n] holds P[n+1] proof let n be non zero Nat; assume A2: Absval (Bin1 n) = 1; thus Absval (Bin1 (n+1)) = Absval (Bin1 n ^ <*FALSE*>) by BINARI_2:7 .= Absval Bin1 n + IFEQ(FALSE,FALSE,0,2 to_power n) by BINARITH:20 .= Absval Bin1 n + 0 by FUNCOP_1:def 8 .= 1 by A2; end; A3: P[1] by Th10,BINARITH:16; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A3,A1); end; theorem Th12: for x,y be Element of BOOLEAN holds (x 'or' y = TRUE iff x = TRUE or y = TRUE) & (x 'or' y = FALSE iff x = FALSE & y = FALSE) proof let x,y be Element of BOOLEAN; thus x 'or' y = TRUE implies x = TRUE or y = TRUE proof assume x 'or' y = TRUE; then 'not' x = FALSE or 'not' y = FALSE by MARGREL1:12; hence thesis; end; thus x = TRUE or y = TRUE implies x 'or' y = TRUE; thus x 'or' y = FALSE implies x = FALSE & y = FALSE proof assume A1: x 'or' y = FALSE; then 'not' x = TRUE by MARGREL1:12; hence thesis by A1; end; thus thesis; end; theorem Th13: for x,y be Element of BOOLEAN holds add_ovfl(<*x*>,<*y*>) = TRUE iff x = TRUE & y = TRUE proof let x,y be Element of BOOLEAN; A1: (<*TRUE*>/.1) '&' (<*TRUE*>/.1) = TRUE by FINSEQ_4:16; thus add_ovfl(<*x*>,<*y*>) = TRUE implies x = TRUE & y = TRUE proof assume add_ovfl(<*x*>,<*y*>) = TRUE; then (<*x*>/.1) '&' (<*y*>/.1) 'or' (<*x*>/.1) '&' ((carry(<*x*>,<*y*>))/.1 ) 'or' (<*y*>/.1) '&' ((carry(<*x*>,<*y*>))/.1) = TRUE by BINARITH:def 6; then A2: (<*x*>/.1) '&' (<*y*>/.1) 'or' (<*x*>/.1) '&' ((carry(<*x*>,<*y*>))/.1 ) = TRUE or (<*y*>/.1) '&' ((carry(<*x*>,<*y*>))/.1) = TRUE by Th12; now per cases by A2,Th12; suppose A3: (<*x*>/.1) '&' (<*y*>/.1) = TRUE; then (<*x*>/.1) = TRUE by MARGREL1:12; hence thesis by A3,FINSEQ_4:16; end; suppose (<*x*>/.1) '&' ((carry(<*x*>,<*y*>))/.1) = TRUE; then (carry(<*x*>,<*y*>))/.1 = TRUE by MARGREL1:12; hence thesis by BINARITH:def 2; end; suppose (<*y*>/.1) '&' ((carry(<*x*>,<*y*>))/.1) = TRUE; then (carry(<*x*>,<*y*>))/.1 = TRUE by MARGREL1:12; hence thesis by BINARITH:def 2; end; end; hence thesis; end; assume that A4: x = TRUE and A5: y = TRUE; thus add_ovfl(<*x*>,<*y*>) = (<*TRUE*>/.1) '&' (<*TRUE*>/.1) 'or' (<*TRUE*> /.1) '&' ((carry(<*TRUE*>,<*TRUE*>))/.1) 'or' (<*TRUE*>/.1) '&' (((carry(<*TRUE *>,<*TRUE*>))/.1)) by A4,A5,BINARITH:def 6 .= TRUE by A1; end; theorem Th14: 'not' <*FALSE*> = <*TRUE*> proof now let i be Nat; assume A1: i in Seg 1; then A2: i = 1 by FINSEQ_1:2,TARSKI:def 1; len <*FALSE*> = 1 by CARD_1:def 7; then A3: (<*FALSE*>/.i) = <*FALSE*>.1 by A2,FINSEQ_4:15; len 'not' <*FALSE*> = 1 by CARD_1:def 7; hence ('not' <*FALSE*>).i = ('not' <*FALSE*>)/.i by A2,FINSEQ_4:15 .= 'not' (<*FALSE*>/.i) by A1,BINARITH:def 1 .= 'not' FALSE by A3,FINSEQ_1:40 .= <*TRUE*>.i by A2,FINSEQ_1:40; end; hence thesis by FINSEQ_2:119; end; theorem 'not' <*TRUE*> = <*FALSE*> proof now let i be Nat; assume A1: i in Seg 1; then A2: i = 1 by FINSEQ_1:2,TARSKI:def 1; len <*TRUE*> = 1 by CARD_1:def 7; then A3: (<*TRUE*>/.i) = <*TRUE*>.1 by A2,FINSEQ_4:15; len 'not' <*TRUE*> = 1 by CARD_1:def 7; hence ('not' <*TRUE*>).i = ('not' <*TRUE*>)/.i by A2,FINSEQ_4:15 .= 'not' (<*TRUE*>/.i) by A1,BINARITH:def 1 .= 'not' TRUE by A3,FINSEQ_1:40 .= <*FALSE*>.i by A2,FINSEQ_1:40; end; hence thesis by FINSEQ_2:119; end; theorem <*FALSE*> + <*FALSE*> = <*FALSE*> proof add_ovfl(<*FALSE*>,<*FALSE*>) <> TRUE by Th13; then add_ovfl(<*FALSE*>,<*FALSE*>) = FALSE by XBOOLEAN:def 3; then <*FALSE*>,<*FALSE*> are_summable by BINARITH:def 7; then Absval(<*FALSE*> + <*FALSE*>) = Absval <*FALSE*> + Absval <*FALSE*> by BINARITH:22 .= Absval <*FALSE*> + 0 by BINARITH:15 .= Absval <*FALSE*>; hence thesis by Th2; end; theorem Th17: <*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE *> proof add_ovfl(<*FALSE*>,<*TRUE*>) <> TRUE by Th13; then add_ovfl(<*FALSE*>,<*TRUE*>) = FALSE by XBOOLEAN:def 3; then <*FALSE*>,<*TRUE*> are_summable by BINARITH:def 7; then Absval(<*FALSE*> + <*TRUE*>) = Absval <*FALSE*> + Absval <*TRUE*> by BINARITH:22 .= Absval <*FALSE*> + 1 by BINARITH:16 .= 0 + 1 by BINARITH:15 .= Absval <*TRUE*> by BINARITH:16; hence <*FALSE*> + <*TRUE*> = <*TRUE*> by Th2; add_ovfl(<*TRUE*>,<*FALSE*>) <> TRUE by Th13; then add_ovfl(<*TRUE*>,<*FALSE*>) = FALSE by XBOOLEAN:def 3; then <*TRUE*>,<*FALSE*> are_summable by BINARITH:def 7; then Absval(<*TRUE*> + <*FALSE*>) = Absval <*TRUE*> + Absval <*FALSE*> by BINARITH:22 .= Absval <*TRUE*> + 0 by BINARITH:15 .= Absval <*TRUE*>; hence thesis by Th2; end; theorem <*TRUE*> + <*TRUE*> = <*FALSE*> proof A1: add_ovfl(<*TRUE*>,<*TRUE*>) = TRUE by Th13; Absval(<*TRUE*> + <*TRUE*>) = Absval(<*TRUE*> + <*TRUE*>) + 2 - 2 .= Absval(<*TRUE*> + <*TRUE*>) + 2 to_power 1 - 2 by POWER:25 .= Absval(<*TRUE*> + <*TRUE*>) + IFEQ(add_ovfl(<*TRUE*>,<*TRUE*>), FALSE ,0,2 to_power (1)) - 2 by A1,FUNCOP_1:def 8 .= Absval <*TRUE*> + Absval <*TRUE*> - 2 by BINARITH:21 .= Absval <*TRUE*> + 1 - 2 by BINARITH:16 .= 1 + 1 - 2 by BINARITH:16 .= Absval <*FALSE*> by BINARITH:15; hence thesis by Th2; end; theorem Th19: for n be non zero Nat for x,y be Tuple of n,BOOLEAN st x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds for k be non zero Nat st k <> 1 & k <= n holds x/.k = TRUE & (carry(x,Bin1 n))/.k = TRUE proof let n be non zero Nat; let x,y be Tuple of n,BOOLEAN; assume that A1: x/.n = TRUE and A2: (carry(x,Bin1 n))/.n = TRUE; defpred P[Nat] means ($1 in Seg (n -' 1) implies x/.(n -' $1 + 1) = TRUE & ( carry(x,Bin1 n))/.(n -' $1 + 1) = TRUE); let k be non zero Nat; assume that A3: k <> 1 and A4: k <= n; set i = n -' k + 1; 1 < k by A3,NAT_2:19; then 1 + 1 <= k by NAT_1:13; then A5: 1 <= k - 1 by XREAL_1:19; A6: for j be non zero Nat st P[j] holds P[j+1] proof let j be non zero Nat; assume that A7: P[j] and A8: j + 1 in Seg (n -' 1); A9: j + 1 <= n -' 1 by A8,FINSEQ_1:1; then A10: j < n -' 1 by NAT_1:13; then j < n - 1 by NAT_1:14,XREAL_1:233; then j + 1 < n by XREAL_1:20; then A11: j < n by NAT_1:13; j + 1 <= n - 1 by A9,NAT_1:14,XREAL_1:233; then 1 <= n - 1 - j by XREAL_1:19; then 1 <= n - j - 1; then 1 + 1 <= n - j by XREAL_1:19; then 1 + 1 <= n -' j by A11,XREAL_1:233; then A12: n -' j > 1 by NAT_1:13; A13: 1 <= j by NAT_1:14; A14: n -' j < n by NAT_2:9; then n -' j in Seg n by A12,FINSEQ_1:1; then A15: (Bin1 n)/.(n -' j) = FALSE by A12,BINARI_2:6; then ((Bin1 n)/.(n -' j)) '&' ((carry(x,Bin1 n))/.(n -' j)) = FALSE; then A16: TRUE = (x/.(n -' j)) '&' ((Bin1 n)/.(n -' j)) 'or' (x/.(n -' j)) '&' ((carry(x,Bin1 n))/.(n -' j)) by A7,A13,A10,A14,A12,A15,BINARITH:def 2 ,FINSEQ_1:1 .= (x/.(n -' j)) '&' ((carry(x,Bin1 n))/.(n -' j)) by A15; then x/.(n -' j) = TRUE by MARGREL1:12; hence x/.(n -' (j+1) + 1) = TRUE by A11,NAT_2:7; (carry(x,Bin1 n))/.(n -' j) = TRUE by A16,MARGREL1:12; hence thesis by A11,NAT_2:7; end; A17: 1 <= i by NAT_1:11; i = n - k + 1 by A4,XREAL_1:233 .= n - (k - 1); then A18: i <= n - 1 by A5,XREAL_1:13; then i + 1 <= n by XREAL_1:19; then i < n by NAT_1:13; then A19: k = n -' i + 1 by A4,NAT_2:5; i <= n -' 1 by A18,NAT_1:14,XREAL_1:233; then A20: i in Seg (n -' 1) by A17,FINSEQ_1:1; A21: P[1] by A1,A2,NAT_1:14,XREAL_1:235; for j be non zero Nat holds P[j] from NAT_1:sch 10(A21,A6); hence thesis by A19,A20; end; registration cluster zero -> non positive for Nat; coherence; end; theorem Th20: for n be non zero Nat for x be Tuple of n,BOOLEAN st x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds carry(x,Bin1 n) = 'not' Bin1 n proof let n be non zero Nat; let x be Tuple of n,BOOLEAN; assume that A1: x/.n = TRUE and A2: (carry(x,Bin1 n))/.n = TRUE; now A3: len 'not' Bin1 n = n by CARD_1:def 7; let i be Nat; reconsider z = i as Nat; A4: len carry(x,Bin1 n) = n by CARD_1:def 7; assume A5: i in Seg n; then A6: 1 <= i by FINSEQ_1:1; A7: i <= n by A5,FINSEQ_1:1; per cases; suppose A8: i = 1; thus carry(x,Bin1 n).i = (carry(x,Bin1 n))/.z by A6,A7,A4,FINSEQ_4:15 .= 'not' TRUE by A8,BINARITH:def 2 .= 'not' ((Bin1 n)/.i) by A5,A8,BINARI_2:5 .= ('not' Bin1 n)/.z by A5,BINARITH:def 1 .= ('not' Bin1 n).i by A6,A7,A3,FINSEQ_4:15; end; suppose A9: i <> 1; 1 <= i by A5,FINSEQ_1:1; then 0 < i; then A10: i is non zero; thus carry(x,Bin1 n).i = (carry(x,Bin1 n))/.z by A6,A7,A4,FINSEQ_4:15 .= 'not' FALSE by A1,A2,A7,A9,A10,Th19 .= 'not' ((Bin1 n)/.i) by A5,A9,BINARI_2:6 .= ('not' Bin1 n)/.z by A5,BINARITH:def 1 .= ('not' Bin1 n).i by A6,A7,A3,FINSEQ_4:15; end; end; hence thesis by FINSEQ_2:119; end; theorem Th21: for n be non zero Nat for x,y be Tuple of n,BOOLEAN st y = 0*n & x/.n = TRUE & (carry(x,Bin1 n))/.n = TRUE holds x = 'not' y proof let n be non zero Nat; let x,y be Tuple of n,BOOLEAN; assume that A1: y = 0*n and A2: x/.n = TRUE and A3: (carry(x,Bin1 n))/.n = TRUE; A4: len x = n by CARD_1:def 7; A5: len 'not' y = n by CARD_1:def 7; A6: len y = n by CARD_1:def 7; A7: len carry(x,Bin1 n) = n by CARD_1:def 7; now let i be Nat; reconsider z = i as Nat; assume A8: i in Seg n; then A9: 1 <= i by FINSEQ_1:1; A10: i <= n by A8,FINSEQ_1:1; A11: y.i = FALSE by A1,A8,FUNCOP_1:7; now per cases; suppose A12: i = 1; A13: n >= 1 by NAT_1:14; now per cases by A13,XXREAL_0:1; suppose n = 1; hence x .i = ('not' y).i by A3,BINARITH:def 2; end; suppose A14: n > 1; A15: len 'not' Bin1 n = n by CARD_1:def 7; A16: (carry(x,Bin1 n))/.i = FALSE by A12,BINARITH:def 2; then A17: ((Bin1 n)/.i) '&' ((carry(x,Bin1 n))/.i) = FALSE; A18: (1+1) <= n by A14,NAT_1:13; then A19: 2 in Seg n by FINSEQ_1:1; carry(x,Bin1 n).(i+1) = ('not' Bin1 n).2 by A2,A3,A12,Th20 .= ('not' Bin1 n)/.2 by A18,A15,FINSEQ_4:15 .= 'not' ((Bin1 n)/.2) by A19,BINARITH:def 1 .= 'not' FALSE by A19,BINARI_2:6 .= TRUE; then A20: TRUE = (carry(x,Bin1 n))/.(i+1) by A7,A12,A18,FINSEQ_4:15 .= (x/.i) '&' ((Bin1 n)/.i) 'or' (x/.i) '&' ((carry(x,Bin1 n)) /.i) by A12,A14,A16,A17,BINARITH:def 2 .= (x/.i) '&' ((Bin1 n)/.i) by A16; thus x .i = x/.z by A4,A9,A10,FINSEQ_4:15 .= 'not' FALSE by A20,MARGREL1:12 .= 'not' (y/.z) by A6,A9,A10,A11,FINSEQ_4:15 .= ('not' y)/.z by A8,BINARITH:def 1 .= ('not' y).i by A5,A9,A10,FINSEQ_4:15; end; end; hence x .i = ('not' y).i; end; suppose A21: i <> 1; 1 <= i by A8,FINSEQ_1:1; then 0 < i; then A22: i is non empty; thus x .i = x/.z by A4,A9,A10,FINSEQ_4:15 .= 'not' FALSE by A2,A3,A10,A21,A22,Th19 .= 'not' (y/.z) by A6,A9,A10,A11,FINSEQ_4:15 .= ('not' y)/.z by A8,BINARITH:def 1 .= ('not' y).i by A5,A9,A10,FINSEQ_4:15; end; end; hence x .i = ('not' y).i; end; hence thesis by FINSEQ_2:119; end; theorem Th22: for n be non zero Nat for y be Tuple of n,BOOLEAN st y = 0*n holds carry('not' y,Bin1 n) = 'not' Bin1 n proof let n be non zero Nat; let y be Tuple of n,BOOLEAN; A1: n >= 1 by NAT_1:14; A2: len y = n by CARD_1:def 7; assume A3: y = 0*n; then A4: y.n = 0 by FINSEQ_1:3,FUNCOP_1:7; n in Seg n by FINSEQ_1:3; then A5: ('not' y)/.n = 'not' (y/.n) by BINARITH:def 1 .= 'not' FALSE by A1,A4,A2,FINSEQ_4:15 .= TRUE; per cases; suppose A6: n = 1; now let i be Nat; A7: len 'not' Bin1 n = n by CARD_1:def 7; assume A8: i in Seg n; then A9: i = 1 by A6,FINSEQ_1:2,TARSKI:def 1; len carry('not' y,Bin1 n) = n by CARD_1:def 7; hence carry('not' y,Bin1 n).i = (carry('not' y,Bin1 n))/.i by A6,A9, FINSEQ_4:15 .= 'not' TRUE by A9,BINARITH:def 2 .= 'not' ((Bin1 n)/.i) by A8,A9,BINARI_2:5 .= ('not' Bin1 n)/.i by A8,BINARITH:def 1 .= ('not' Bin1 n).i by A6,A9,A7,FINSEQ_4:15; end; hence thesis by FINSEQ_2:119; end; suppose n <> 1; then A10: n is non trivial by NAT_2:def 1; defpred P[Nat] means $1 <= n implies (carry('not' y,Bin1 n))/.$1 = TRUE; A11: for i be non trivial Nat st P[i] holds P[i+1] proof let i be non trivial Nat; assume that A12: i <= n implies (carry('not' y,Bin1 n))/.i = TRUE and A13: i + 1 <= n; A14: 1 <= i by NAT_1:14; A15: i < n by A13,NAT_1:13; then A16: i in Seg n by A14,FINSEQ_1:1; then A17: y.i = FALSE by A3,FUNCOP_1:7; A18: ('not' y)/.i = 'not' (y/.i) by A16,BINARITH:def 1 .= 'not' FALSE by A2,A14,A15,A17,FINSEQ_4:15 .= TRUE; i <> 1 by NAT_2:def 1; then A19: ((Bin1 n)/.i) = FALSE by A16,BINARI_2:6; then ((Bin1 n)/.i) '&' ((carry('not' y,Bin1 n))/.i) = FALSE; hence (carry('not' y,Bin1 n))/.(i + 1) = (('not' y)/.i) '&' ((Bin1 n)/.i) 'or' (('not' y)/.i) '&' ((carry('not' y,Bin1 n))/.i) by A14,A15,A19, BINARITH:def 2 .= TRUE by A12,A13,A18,NAT_1:13; end; A20: P[2] proof assume 2 <= n; then 1 + 1 <= n; then A21: 1 < n by NAT_1:13; then A22: 1 in Seg n by FINSEQ_1:1; then A23: y.1 = FALSE by A3,FUNCOP_1:7; ('not' y)/.1 = 'not' (y/.1) by A22,BINARITH:def 1 .= 'not' FALSE by A2,A21,A23,FINSEQ_4:15 .= TRUE; then A24: (('not' y)/.1) '&' ((Bin1 n)/.1) = TRUE by A22,BINARI_2:5; thus (carry('not' y,Bin1 n))/.2 = (carry('not' y,Bin1 n))/.(1 + 1) .= (('not' y)/.1) '&' ((Bin1 n)/.1) 'or' (('not' y)/.1) '&' ((carry( 'not' y,Bin1 n))/.1) 'or' ((Bin1 n)/.1) '&' ( (carry('not' y,Bin1 n))/.1) by A21,BINARITH:def 2 .= TRUE by A24; end; for i be non trivial Nat holds P[i] from NAT_2:sch 2(A20,A11); then (carry('not' y,Bin1 n))/.n = TRUE by A10; hence thesis by A5,Th20; end; end; theorem Th23: for n be non zero Nat for x,y be Tuple of n,BOOLEAN st y = 0*n holds add_ovfl(x,Bin1 n) = TRUE iff x = 'not' y proof let n be non zero Nat; let x,y be Tuple of n,BOOLEAN; assume A1: y = 0*n; A2: n in Seg n by FINSEQ_1:3; A3: 1 in Seg 1 by FINSEQ_1:3; thus add_ovfl(x,Bin1 n) = TRUE implies x = 'not' y proof assume A4: add_ovfl(x,Bin1 n) = TRUE; then A5: (x/.n) '&' ((Bin1 n)/.n) 'or' (x/.n) '&' ((carry(x,Bin1 n))/.n) 'or' ( (Bin1 n)/.n) '&' ((carry(x,Bin1 n))/.n) = TRUE by BINARITH:def 6; per cases; suppose A6: n <> 1; now per cases by A5,Th12; suppose A7: (x/.n) '&' ((Bin1 n)/.n) 'or' (x/.n) '&' ((carry(x,Bin1 n)) /.n) = TRUE; now per cases by A7,Th12; suppose A8: (x/.n) '&' ((Bin1 n)/.n) = TRUE; assume x <> 'not' y; ((Bin1 n)/.n) = TRUE by A8,MARGREL1:12; hence contradiction by A2,A6,BINARI_2:6; end; suppose A9: (x/.n) '&' ((carry(x,Bin1 n))/.n) = TRUE; then (x/.n) = TRUE by MARGREL1:12; hence thesis by A1,A9,Th21; end; end; hence thesis; end; suppose A10: ((Bin1 n)/.n) '&' ((carry(x,Bin1 n))/.n) = TRUE; assume x <> 'not' y; ((Bin1 n)/.n) = TRUE by A10,MARGREL1:12; hence contradiction by A2,A6,BINARI_2:6; end; end; hence thesis; end; suppose A11: n = 1; then len y = 1 by CARD_1:def 7; then 1 in dom y by A3,FINSEQ_1:def 3; then A12: (y/.1) = y.1 by PARTFUN1:def 6 .= 0 by A1,A11,FINSEQ_1:3,FUNCOP_1:7; consider d be Element of BOOLEAN such that A13: x = <*d*> by A11,FINSEQ_2:97; A14: d = TRUE by A4,A11,A13,Th10,Th13; now let i be Nat; assume i in Seg n; then i = 1 by A11,FINSEQ_1:2,TARSKI:def 1; hence x/.i = 'not' (y/.i) by A13,A14,A12,FINSEQ_4:16; end; hence thesis by BINARITH:def 1; end; end; assume A15: x = 'not' y; per cases; suppose A16: n <> 1; A17: (carry(x,Bin1 n))/.n = ('not' Bin1 n)/.n by A1,A15,Th22 .= 'not' ((Bin1 n)/.n) by A2,BINARITH:def 1 .= 'not' FALSE by A2,A16,BINARI_2:6 .= TRUE; len y = n by CARD_1:def 7; then n in dom y by A2,FINSEQ_1:def 3; then A18: (y/.n) = y.n by PARTFUN1:def 6 .= 0 by A1,FINSEQ_1:3,FUNCOP_1:7; A19: x/.n = 'not' (y/.n) by A2,A15,BINARITH:def 1 .= TRUE by A18; thus add_ovfl(x,Bin1 n) = (x/.n) '&' ((Bin1 n)/.n) 'or' (x/.n) '&' ((carry (x,Bin1 n))/.n) 'or' ((Bin1 n)/.n) '&' ((carry(x,Bin1 n))/.n) by BINARITH:def 6 .= TRUE by A19,A17; end; suppose A20: n = 1; then len y = 1 by CARD_1:def 7; then 1 in dom y by A3,FINSEQ_1:def 3; then A21: (y/.1) = y.1 by PARTFUN1:def 6 .= 0 by A1,A20,FINSEQ_1:3,FUNCOP_1:7; consider d be Element of BOOLEAN such that A22: x = <*d*> by A20,FINSEQ_2:97; d = ('not' y)/.1 by A15,A22,FINSEQ_4:16 .= 'not' (y/.1) by A3,A20,BINARITH:def 1 .= TRUE by A21; hence thesis by A20,A22,Th10,Th13; end; end; theorem Th24: for n be non zero Nat for z be Tuple of n,BOOLEAN st z = 0*n holds 'not' z + Bin1 n = z proof let n be non zero Nat; let z be Tuple of n,BOOLEAN; assume A1: z = 0*n; then A2: add_ovfl('not' z,Bin1 n) = TRUE by Th23; Absval ('not' z + Bin1 n) = Absval ('not' z + Bin1 n) + 2 to_power n - 2 to_power n .= Absval ('not' z + Bin1 n) + IFEQ(add_ovfl('not' z,Bin1 n),FALSE, 0,2 to_power (n)) - 2 to_power n by A2,FUNCOP_1:def 8 .= Absval 'not' z + Absval Bin1 n - 2 to_power n by BINARITH:21 .= - Absval(z) + 2 to_power n - 1 + Absval Bin1 n - 2 to_power n by BINARI_2:13 .= - Absval(z) + 2 to_power n - 1 + 1 - 2 to_power n by Th11 .= -0 by A1,Th6 .= Absval z by A1,Th6; hence thesis by Th2; end; begin :: Binary Sequences definition let n,k be Nat; func n-BinarySequence k -> Tuple of n,BOOLEAN means :Def1: for i be Nat st i in Seg n holds it/.i = IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE); existence proof reconsider n9 = n as Nat; deffunc F(Nat) = IFEQ((k div 2 to_power ($1-'1)) mod 2,0,FALSE,TRUE); consider p be FinSequence of BOOLEAN such that A1: len p = n9 and A2: for i be Nat st i in dom p holds p.i = F(i) from FINSEQ_2:sch 1; A3: dom p = Seg n9 by A1,FINSEQ_1:def 3; reconsider p as Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92; take p; let i be Nat; assume A4: i in Seg n; then i in dom p by A1,FINSEQ_1:def 3; hence p/.i = p.i by PARTFUN1:def 6 .= IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A2,A3,A4; end; uniqueness proof let p1,p2 be Tuple of n,BOOLEAN such that A5: for i be Nat st i in Seg n holds p1/.i = IFEQ((k div 2 to_power (i -'1)) mod 2,0,FALSE,TRUE) and A6: for i be Nat st i in Seg n holds p2/.i = IFEQ((k div 2 to_power (i -'1)) mod 2,0,FALSE,TRUE); A7: len p1 = n by CARD_1:def 7; then A8: dom p1 = Seg n by FINSEQ_1:def 3; A9: len p2 = n by CARD_1:def 7; now let i be Nat; assume A10: i in dom p1; then A11: i in dom p2 by A9,A8,FINSEQ_1:def 3; thus p1.i = p1/.i by A10,PARTFUN1:def 6 .= IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A5,A8,A10 .= p2/.i by A6,A8,A10 .= p2.i by A11,PARTFUN1:def 6; end; hence thesis by A7,A9,FINSEQ_2:9; end; end; theorem Th25: for n be Nat holds n-BinarySequence 0 = 0*n proof let n be Nat; 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider F = 0*n as Tuple of n,BOOLEAN; now let i be Nat; assume A1: i in Seg n; len (n-BinarySequence 0) = n by CARD_1:def 7; then i in dom (n-BinarySequence 0) by A1,FINSEQ_1:def 3; hence (n-BinarySequence 0).i = (n-BinarySequence 0)/.i by PARTFUN1:def 6 .= IFEQ((0 div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A1,Def1 .= IFEQ(0 mod 2,0,FALSE,TRUE) by NAT_2:2 .= IFEQ(0,0,FALSE,TRUE) by NAT_D:26 .= 0 by FUNCOP_1:def 8 .= F.i by A1,FUNCOP_1:7; end; hence thesis by FINSEQ_2:119; end; theorem Th26: for n,k be Nat st k < 2 to_power n holds ((n+1)-BinarySequence k ).(n+1) = FALSE proof let n,k be Nat; A1: n+1-'1 = n+1-1 by NAT_D:37 .= n; assume k < 2 to_power n; then A2: (k div 2 to_power (n+1-'1)) mod 2 = 0 mod 2 by A1,NAT_D:27 .= 0 by NAT_D:26; A3: n + 1 in Seg (n+1) by FINSEQ_1:4; then n + 1 in Seg len ((n+1)-BinarySequence k) by CARD_1:def 7; then n + 1 in dom ((n+1)-BinarySequence k) by FINSEQ_1:def 3; hence ((n+1)-BinarySequence k).(n+1) = ((n+1)-BinarySequence k)/.(n+1) by PARTFUN1:def 6 .= IFEQ((k div 2 to_power (n+1-'1)) mod 2,0,FALSE,TRUE) by A3,Def1 .= FALSE by A2,FUNCOP_1:def 8; end; theorem Th27: for n be non zero Nat for k be Nat st k < 2 to_power n holds (n +1)-BinarySequence k = (n-BinarySequence k)^<*FALSE*> proof let n be non zero Nat; let k be Nat; assume A1: k < 2 to_power n; now let i be Nat; assume A2: i in Seg (n + 1); then i in Seg len ((n+1)-BinarySequence k) by CARD_1:def 7; then A3: i in dom ((n+1)-BinarySequence k) by FINSEQ_1:def 3; now per cases by A2,FINSEQ_2:7; suppose A4: i in Seg n; then i in Seg len (n-BinarySequence k) by CARD_1:def 7; then A5: i in dom (n-BinarySequence k) by FINSEQ_1:def 3; thus ((n+1)-BinarySequence k).i = ((n+1)-BinarySequence k)/.i by A3, PARTFUN1:def 6 .= IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A2,Def1 .= (n-BinarySequence k)/.i by A4,Def1 .= (n-BinarySequence k).i by A5,PARTFUN1:def 6 .= ((n-BinarySequence k)^<*FALSE*>).i by A5,FINSEQ_1:def 7; end; suppose A6: i = n + 1; hence ((n+1)-BinarySequence k).i = FALSE by A1,Th26 .= ((n-BinarySequence k)^<*FALSE*>).i by A6,FINSEQ_2:116; end; end; hence ((n+1)-BinarySequence k).i = ((n-BinarySequence k)^<*FALSE*>).i; end; hence thesis by FINSEQ_2:119; end; Lm1: for n be non zero Nat holds (n+1)-BinarySequence 2 to_power n = 0*n^<* TRUE*> proof let n be non zero Nat; 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider 0n = 0*n as Tuple of n,BOOLEAN; now let i be Nat; assume A1: i in Seg (n+1); now per cases by A1,FINSEQ_2:7; suppose A2: i in Seg n; then A3: i >= 1 by FINSEQ_1:1; i <= n + 1 by A1,FINSEQ_1:1; then i - 1 <= n + 1 - 1 by XREAL_1:9; then A4: i-'1 <= n + 1 - 1 by A3,XREAL_1:233; n = n-(i-'1)+(i-'1) .= n-'(i-'1)+(i-'1) by A4,XREAL_1:233; then A5: 2 to_power n = 2 to_power (n-'(i-'1)) * 2 to_power (i-'1) by POWER:27; i in Seg len 0n by A2,CARD_1:def 7; then A6: i in dom 0n by FINSEQ_1:def 3; n >= i by A2,FINSEQ_1:1; then n + 1 > i by NAT_1:13; then n > i - 1 by XREAL_1:19; then n - (i - 1) > 0 by XREAL_1:50; then n - (i-'1) > 0 by A3,XREAL_1:233; then n-'(i-'1) > 0 by A4,XREAL_1:233; then consider n1 be Nat such that A7: n-'(i-'1) = n1 + 1 by NAT_1:6; reconsider n1 as Nat; A8: 2 to_power (n -' (i-'1)) = 2 to_power n1 * 2 to_power 1 by A7,POWER:27 .= 2 to_power n1 * 2 by POWER:25; 2 to_power (i-'1) > 0 by POWER:34; then A9: ((2 to_power n) div 2 to_power (i-'1)) mod 2 = (2 to_power (n-'(i -'1))) mod 2 by A5,NAT_D:18 .= 0 by A8,NAT_D:13; i in Seg len ((n+1)-BinarySequence 2 to_power n) by A1,CARD_1:def 7; then i in dom ((n+1)-BinarySequence 2 to_power n) by FINSEQ_1:def 3; hence ((n+1)-BinarySequence 2 to_power n).i = ((n+1)-BinarySequence 2 to_power n)/.i by PARTFUN1:def 6 .= IFEQ(((2 to_power n) div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A1,Def1 .= 0 by A9,FUNCOP_1:def 8 .= 0n.i by A2,FUNCOP_1:7 .= (0n^<*TRUE*>).i by A6,FINSEQ_1:def 7; end; suppose A10: i = n + 1; A11: 2 to_power n > 0 by POWER:34; i-'1 = n+1-1 by A10,NAT_D:37 .= n; then A12: ((2 to_power n) div 2 to_power (i-'1)) mod 2 = 1 mod 2 by A11,NAT_2:3 .= 1 by NAT_D:14; n + 1 in Seg (n+1) by FINSEQ_1:4; then n + 1 in Seg len ((n+1)-BinarySequence 2 to_power n) by CARD_1:def 7; then n + 1 in dom ((n+1)-BinarySequence 2 to_power n) by FINSEQ_1:def 3 ; hence ((n+1)-BinarySequence 2 to_power n).i = ((n+1)-BinarySequence 2 to_power n)/.i by A10,PARTFUN1:def 6 .= IFEQ(((2 to_power n) div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A1,Def1 .= TRUE by A12,FUNCOP_1:def 8 .= (0n^<*TRUE*>).i by A10,FINSEQ_2:116; end; end; hence ((n+1)-BinarySequence 2 to_power n).i = (0n^<*TRUE*>).i; end; hence thesis by FINSEQ_2:119; end; Lm2: for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds ((n+1)-BinarySequence k).(n+1) = TRUE proof let n be non zero Nat; let k be Nat; assume that A1: 2 to_power n <= k and A2: k < 2 to_power (n+1); k < 2 to_power n * 2 to_power 1 by A2,POWER:27; then k < 2 * 2 to_power n by POWER:25; then A3: k < 2 to_power n + 2 to_power n; n+1-'1 = n+1-1 by NAT_D:37 .= n; then A4: (k div 2 to_power (n+1-'1)) mod 2 = 1 mod 2 by A1,A3,NAT_2:20 .= 1 by NAT_D:24; A5: n + 1 in Seg (n+1) by FINSEQ_1:4; then n + 1 in Seg len ((n+1)-BinarySequence k) by CARD_1:def 7; then n + 1 in dom ((n+1)-BinarySequence k) by FINSEQ_1:def 3; hence ((n+1)-BinarySequence k).(n+1) = ((n+1)-BinarySequence k)/.(n+1) by PARTFUN1:def 6 .= IFEQ((k div 2 to_power (n+1-'1)) mod 2,0,FALSE,TRUE) by A5,Def1 .= TRUE by A4,FUNCOP_1:def 8; end; Lm3: for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds (n+1)-BinarySequence k = (n-BinarySequence (k -' 2 to_power n))^<* TRUE*> proof let n be non zero Nat; let k be Nat; assume that A1: 2 to_power n <= k and A2: k < 2 to_power (n+1); now let i be Nat; reconsider z = i as Nat; assume A3: i in Seg (n+1); then i in Seg len ((n+1)-BinarySequence k) by CARD_1:def 7; then A4: i in dom ((n+1)-BinarySequence k) by FINSEQ_1:def 3; now per cases by A3,FINSEQ_2:7; suppose A5: i in Seg n; then A6: 1 <= i by FINSEQ_1:1; A7: 2 * 2 to_power (i-'1) = 2 to_power (i-'1) * 2 to_power 1 by POWER:25 .= 2 to_power (i-'1+1) by POWER:27 .= 2 to_power (i-1+1) by A6,XREAL_1:233 .= 2 to_power i; 2 to_power (i-'1) > 0 by POWER:34; then A8: 0 + 1 <= 2 to_power (i-'1) by NAT_1:13; i <= n by A5,FINSEQ_1:1; then A9: 2 * 2 to_power (z-'1) divides 2 to_power n by A7,NAT_2:11; A10: now per cases; suppose A11: k div 2 to_power (i-'1) is even; then A12: (k div 2 to_power (i-'1)) mod 2 = 0 by NAT_2:21; (k-' 2 to_power n) div 2 to_power (i-'1) is even by A1,A8,A9,A11, NAT_2:23; hence (k div 2 to_power (i-'1)) mod 2 = ((k -' 2 to_power n) div 2 to_power (i-'1)) mod 2 by A12,NAT_2:21; end; suppose A13: k div 2 to_power (i-'1) is odd; then A14: (k div 2 to_power (i-'1)) mod 2 = 1 by NAT_2:22; (k -' 2 to_power n) div 2 to_power (i-'1) is odd by A1,A8,A9,A13, NAT_2:23; hence (k div 2 to_power (i-'1)) mod 2 = ((k -' 2 to_power n) div 2 to_power (i-'1)) mod 2 by A14,NAT_2:22; end; end; i in Seg len (n-BinarySequence (k -' 2 to_power n)) by A5,CARD_1:def 7; then A15: i in dom (n-BinarySequence (k -' 2 to_power n)) by FINSEQ_1:def 3; thus ((n+1)-BinarySequence k).i = ((n+1)-BinarySequence k)/.i by A4, PARTFUN1:def 6 .= IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A3,Def1 .= (n-BinarySequence (k -' 2 to_power n))/.i by A5,A10,Def1 .= (n-BinarySequence (k -' 2 to_power n)).i by A15,PARTFUN1:def 6 .= ((n-BinarySequence (k -' 2 to_power n))^<*TRUE*>).i by A15, FINSEQ_1:def 7; end; suppose A16: i = n + 1; hence ((n+1)-BinarySequence k).i = TRUE by A1,A2,Lm2 .= ((n-BinarySequence (k -' 2 to_power n))^<*TRUE*>).i by A16, FINSEQ_2:116; end; end; hence ((n+1)-BinarySequence k).i = ((n-BinarySequence (k -' 2 to_power n))^ <*TRUE*>).i; end; hence thesis by FINSEQ_2:119; end; Lm4: for n be non zero Nat for k be Nat st k < 2 to_power n for x be Tuple of n,BOOLEAN st x = 0*n holds n-BinarySequence k = 'not' x iff k = 2 to_power n - 1 proof let n be non zero Nat; let k be Nat; assume A1: k < 2 to_power n; let x be Tuple of n,BOOLEAN; assume A2: x = 0*n; thus n-BinarySequence k = 'not' x implies k = 2 to_power n - 1 proof defpred P[Nat] means for k be Nat holds (k < 2 to_power $1 implies for y be Tuple of $1,BOOLEAN st y = 0*$1 holds $1-BinarySequence k = 'not' y implies k = 2 to_power $1 - 1); assume A3: n-BinarySequence k = 'not' x; A4: for m be non zero Nat st P[m] holds P[m+1] proof let m be non zero Nat; assume A5: P[m]; A6: m + 1 in Seg (m + 1) by FINSEQ_1:4; A7: 0 + 1 <= m + 1 by XREAL_1:6; 0*m in BOOLEAN* by Th4; then 0*m is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider y1 = 0*m as Tuple of m,BOOLEAN; let k be Nat; assume A8: k < 2 to_power (m+1); let y be Tuple of m+1,BOOLEAN; assume that A9: y = 0*(m+1) and A10: (m+1)-BinarySequence k = 'not' y; A11: y.(m + 1) = FALSE by A9,FINSEQ_1:4,FUNCOP_1:7; A12: y = y1 ^ <* 0 *> by A9,FINSEQ_2:60; A13: len y = m + 1 by CARD_1:def 7; len 'not' y = m + 1 by CARD_1:def 7; then A14: ((m+1)-BinarySequence k).(m+1) = ('not' y)/.(m+1) by A10,A7,FINSEQ_4:15 .= 'not' (y/.(m+1)) by A6,BINARITH:def 1 .= 'not' FALSE by A13,A7,A11,FINSEQ_4:15 .= TRUE; then (m+1)-BinarySequence k = (m-BinarySequence (k -' 2 to_power m))^<* TRUE*> by A8,Lm3,Th26; then (m-BinarySequence (k -' 2 to_power m))^<*TRUE*> = 'not' y1^<*'not' FALSE*> by A10,A12,BINARI_2:9; then A15: m-BinarySequence (k -' 2 to_power m) = 'not' y1 by FINSEQ_2:17; k < (2 to_power m) * (2 to_power 1) by A8,POWER:27; then k < 2 * (2 to_power m) by POWER:25; then k < 2 to_power m + 2 to_power m; then k - 2 to_power m < 2 to_power m by XREAL_1:19; then k -' 2 to_power m < 2 to_power m by A14,Th26,XREAL_1:233; then k -' 2 to_power m = 2 to_power m - 1 by A5,A15; then k - 2 to_power m = 2 to_power m - 1 by A14,Th26,XREAL_1:233; hence k = (2 to_power m) * 2 - 1 .= (2 to_power m) * (2 to_power 1) - 1 by POWER:25 .= 2 to_power (m+1) - 1 by POWER:27; end; A16: P[1] proof let k be Nat; A17: 1 <= len (1-BinarySequence k) by CARD_1:def 7; assume k < 2 to_power 1; then A18: k < 2 by POWER:25; let y be Tuple of 1,BOOLEAN; assume y = 0*1; then A19: y = <*FALSE*> by FINSEQ_2:59; assume A20: 1-BinarySequence k = 'not' y; A21: 1 in Seg 1 by FINSEQ_1:3; A22: 1 = <*1*>.1 by FINSEQ_1:40 .= (1-BinarySequence k)/.1 by A19,A20,A17,Th14,FINSEQ_4:15 .= IFEQ((k div 2 to_power (1-'1)) mod 2,0,FALSE,TRUE) by A21,Def1; k = 1 proof assume k <> 1; then k = 0 by A18,NAT_1:23; then k div 2 to_power (1-'1) = 0 by NAT_D:27,POWER:34; then (k div 2 to_power (1-'1)) mod 2 = 0 by NAT_D:26; hence contradiction by A22,FUNCOP_1:def 8; end; hence k = 1 + 1 - 1 .= 2 to_power 1 - 1 by POWER:25; end; for m be non zero Nat holds P[m] from NAT_1:sch 10(A16,A4 ); hence thesis by A1,A2,A3; end; assume A23: k = 2 to_power n - 1; now let i be Nat; A24: len x = n by CARD_1:def 7; 2 to_power (i-'1) > 0 by POWER:34; then A25: 2 to_power (i-'1) >= 0 + 1 by NAT_1:13; A26: len 'not' x = n by CARD_1:def 7; A27: 2 to_power (n-'(i-'1)) > 0 by POWER:34; then A28: 2 to_power (n-'(i-'1)) >= 0 + 1 by NAT_1:13; reconsider z = i as Nat; assume A29: i in Seg n; then A30: 1 <= i by FINSEQ_1:1; i <= n by A29,FINSEQ_1:1; then i < n + 1 by NAT_1:13; then A31: i - 1 < n + 1 - 1 by XREAL_1:9; 1 <= i by A29,FINSEQ_1:1; then A32: 0 + (i-'1) < n by A31,XREAL_1:233; then n - (i-'1) > 0 by XREAL_1:20; then n-'(i-'1) > 0 by A32,XREAL_1:233; then A33: 2 to_power (n-'(i-'1)) mod 2 = 0 by NAT_2:17; 2 to_power n > 0 by POWER:34; then A34: 2 to_power n >= 0 + 1 by NAT_1:13; then k div 2 to_power (i-'1) = (2 to_power n -' 1) div 2 to_power (i-'1) by A23,XREAL_1:233 .= (2 to_power n div 2 to_power (i-'1)) - 1 by A25,A32,A34,NAT_2:11,15 .= (2 to_power (n-'(i-'1))) - 1 by A32,NAT_2:16 .= (2 to_power (n-'(i-'1))) -' 1 by A28,XREAL_1:233; then A35: (k div 2 to_power (i-'1)) mod 2 = 1 by A33,A27,NAT_2:18; A36: (x).i = FALSE by A2,A29,FUNCOP_1:7; A37: i <= n by A29,FINSEQ_1:1; i in Seg len (n-BinarySequence k) by A29,CARD_1:def 7; then i in dom (n-BinarySequence k) by FINSEQ_1:def 3; hence (n-BinarySequence k).i = (n-BinarySequence k)/.i by PARTFUN1:def 6 .= IFEQ((k div 2 to_power (i-'1)) mod 2,0,FALSE,TRUE) by A29,Def1 .= 'not' FALSE by A35,FUNCOP_1:def 8 .= 'not' (x/.z) by A24,A30,A37,A36,FINSEQ_4:15 .= ('not' x)/.z by A29,BINARITH:def 1 .= ('not' x).i by A26,A30,A37,FINSEQ_4:15; end; hence thesis by FINSEQ_2:119; end; theorem Th28: for i being Nat holds (i+1)-BinarySequence 2 to_power i= 0*i^<*1 *> proof deffunc Bi(Nat) = ($1+1)-BinarySequence 2 to_power $1; let i be Nat; set Bi = Bi(i); per cases; suppose A1: i = 0; then A2: 0*i = 0; reconsider i1 = i+1 as non zero Nat; A3: 0*i1 = <*FALSE*> by A1,FINSEQ_2:59; then reconsider x = 0*i1 as Tuple of i1, BOOLEAN; 2 to_power i1 = 2 by A1,POWER:25; then 1 = (2 to_power i1) - 1; then i1-BinarySequence 1 = 'not' x by Lm4; hence Bi = <*TRUE*> by A1,A3,Th14,POWER:24 .= 0*i^<*1*> by A2,FINSEQ_1:34; end; suppose i > 0; then reconsider i9 = i as non zero Nat; Bi = 0*(i9)^<*1*> by Lm1; hence thesis; end; end; theorem for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds ((n+1)-BinarySequence k).(n+1) = TRUE by Lm2; theorem for n be non zero Nat for k be Nat st 2 to_power n <= k & k < 2 to_power (n+1) holds (n+1)-BinarySequence k = (n-BinarySequence (k -' 2 to_power n))^<*TRUE*> by Lm3; theorem for n be non zero Nat for k be Nat st k < 2 to_power n for x be Tuple of n,BOOLEAN st x = 0*n holds n-BinarySequence k = 'not' x iff k = 2 to_power n - 1 by Lm4; theorem Th32: for n be non zero Nat for k be Nat st k + 1 < 2 to_power n holds add_ovfl(n-BinarySequence k,Bin1 n) = FALSE proof let n be non zero Nat; let k be Nat; assume A1: k + 1 < 2 to_power n; then A2: k < 2 to_power n by NAT_1:13; 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider y = 0*n as Tuple of n,BOOLEAN; k < 2 to_power n - 1 by A1,XREAL_1:20; then n-BinarySequence k <> 'not' y by A2,Lm4; then add_ovfl(n-BinarySequence k,Bin1 n) <> TRUE by Th23; hence thesis by XBOOLEAN:def 3; end; theorem Th33: for n be non zero Nat for k be Nat st k + 1 < 2 to_power n holds n-BinarySequence (k+1) = n-BinarySequence k + Bin1 n proof defpred P[non zero Nat] means for k be Nat st k + 1 < 2 to_power $1 holds $1-BinarySequence (k+1) = $1-BinarySequence k + Bin1 $1; A1: for n be non zero Nat st P[n] holds P[n+1] proof let n be non zero Nat; assume A2: P[n]; let k be Nat; assume A3: k + 1 < 2 to_power (n+1); then A4: k < 2 to_power (n+1) by NAT_1:13; now per cases by XXREAL_0:1; suppose A5: k + 1 < 2 to_power n; then A6: k < 2 to_power n by NAT_1:13; A7: add_ovfl(n-BinarySequence k,Bin1 n) = FALSE by A5,Th32; thus (n+1)-BinarySequence (k+1) = (n-BinarySequence (k+1))^<*FALSE*> by A5,Th27 .= (n-BinarySequence k + Bin1 n)^<*FALSE 'xor' FALSE 'xor' add_ovfl(n-BinarySequence k,Bin1 n)*> by A2,A5,A7 .= ((n-BinarySequence k)^<*FALSE*>) + (Bin1 n^<*FALSE*>) by BINARITH:19 .= ((n-BinarySequence k)^<*FALSE*>) + Bin1 (n+1) by BINARI_2:7 .= (n+1)-BinarySequence k + Bin1 (n+1) by A6,Th27; end; suppose A8: k + 1 > 2 to_power n; then A9: k >= 2 to_power n by NAT_1:13; k + 1 < (2 to_power n) * (2 to_power 1) by A3,POWER:27; then k + 1 < (2 to_power n) * 2 by POWER:25; then k + 1 < 2 to_power n + 2 to_power n; then k + 1 - 2 to_power n < 2 to_power n by XREAL_1:19; then k - 2 to_power n + 1 < 2 to_power n; then A10: k -' 2 to_power n + 1 < 2 to_power n by A9,XREAL_1:233; then A11: add_ovfl(n-BinarySequence (k -' 2 to_power n),Bin1 n) = FALSE by Th32; thus (n+1)-BinarySequence (k+1) = (n-BinarySequence (k + 1 -' 2 to_power n))^<*TRUE*> by A3,A8,Lm3 .= (n-BinarySequence (k-'2 to_power n + 1))^<*TRUE*> by A9,NAT_D:38 .= (n-BinarySequence (k -' 2 to_power n) + Bin1 n)^<*TRUE 'xor' FALSE 'xor' add_ovfl(n-BinarySequence (k -' 2 to_power n),Bin1 n)*> by A2,A10 ,A11 .= (n-BinarySequence (k -' 2 to_power n))^<*TRUE*> + Bin1 n^<* FALSE*> by BINARITH:19 .= (n-BinarySequence (k -' 2 to_power n))^<*TRUE*> + Bin1 (n+1) by BINARI_2:7 .= (n+1)-BinarySequence k + Bin1 (n+1) by A4,A9,Lm3; end; suppose A12: k + 1 = 2 to_power n; 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider z = 0*n as Tuple of n,BOOLEAN; A13: k < 2 to_power n by A12,NAT_1:13; k = 2 to_power n - 1 by A12; then A14: n-BinarySequence k = 'not' z by A13,Lm4; thus (n+1)-BinarySequence (k+1) = 0*n^<*1*> by A12,Th28 .= ('not' z + Bin1 n)^<*TRUE*> by Th24 .= (n-BinarySequence k + Bin1 n)^<*FALSE 'xor' FALSE 'xor' add_ovfl(n-BinarySequence k,Bin1 n)*> by A14,Th23 .= (n-BinarySequence k)^<*FALSE*> + Bin1 n^<*FALSE*> by BINARITH:19 .= (n-BinarySequence k)^<*FALSE*> + Bin1 (n+1) by BINARI_2:7 .= (n+1)-BinarySequence k + Bin1 (n+1) by A13,Th27; end; end; hence thesis; end; A15: P[1] proof 0*1 in BOOLEAN* by Th4; then 0*1 is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider x = 0*1 as Tuple of 1,BOOLEAN; let k be Nat; A16: 0*1 = <*FALSE*> by FINSEQ_2:59; assume A17: k + 1 < 2 to_power 1; then k + 1 < 1 + 1 by POWER:25; then k < 1 by XREAL_1:6; then A18: k = 0 by NAT_1:14; then k + 1 = 2 - 1 .= 2 to_power 1 - 1 by POWER:25; hence 1-BinarySequence (k+1) = 'not' x by A17,Lm4 .= 1-BinarySequence k + Bin1 1 by A18,A16,Th10,Th14,Th17,Th25; end; thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A15,A1); end; theorem for n,i be Nat holds (n+1)-BinarySequence i = <*i mod 2*> ^ (n -BinarySequence (i div 2)) proof let n,i be Nat; A1: len ((n+1)-BinarySequence i) = n + 1 by CARD_1:def 7; then A2: dom ((n+1)-BinarySequence i) = Seg(n+1) by FINSEQ_1:def 3; A3: len (<*i mod 2*> ^ (n-BinarySequence (i div 2))) = 1 + len (n -BinarySequence (i div 2)) by FINSEQ_5:8 .= n + 1 by CARD_1:def 7; now let j be Nat; reconsider z = j as Nat; assume A4: j in dom ((n+1)-BinarySequence i); then A5: 1 <= j by A2,FINSEQ_1:1; A6: j <= n + 1 by A2,A4,FINSEQ_1:1; A7: len <*i mod 2*> = 1 by FINSEQ_1:39; now per cases by A5,XXREAL_0:1; suppose A8: j > 1; A9: 2 to_power (j-'1-'1 + 1) = (2 to_power (j-'1-'1)) * (2 to_power 1 ) by POWER:27 .= 2 * 2 to_power (j-'1-'1) by POWER:25; j - 1 > 1 - 1 by A8,XREAL_1:9; then j-'1 > 0 by A5,XREAL_1:233; then A10: j-'1 >= 0 + 1 by NAT_1:13; then A11: i div 2 to_power (j-'1) = i div 2 to_power (j-'1-'1 + 1) by XREAL_1:235 .= (i div 2) div 2 to_power (j-'1-'1) by A9,NAT_2:27; j - 1 <= n by A6,XREAL_1:20; then A12: j-'1 <= n by A5,XREAL_1:233; then A13: j-'1 <= len (n-BinarySequence (i div 2)) by CARD_1:def 7; A14: j-'1 in Seg n by A10,A12,FINSEQ_1:1; j <= len ((n+1)-BinarySequence i) by A6,CARD_1:def 7; hence ((n+1)-BinarySequence i).j = ((n+1)-BinarySequence i)/.z by A5, FINSEQ_4:15 .= IFEQ((i div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,A4,Def1 .= (n-BinarySequence (i div 2))/.(j-'1) by A14,A11,Def1 .= (n-BinarySequence (i div 2)).(j-'1) by A10,A13,FINSEQ_4:15 .= (n-BinarySequence (i div 2)).(j - 1) by A5,XREAL_1:233 .= (<*i mod 2*> ^ (n-BinarySequence (i div 2))).j by A3,A6,A7,A8, FINSEQ_1:24; end; suppose A15: j = 1; A16: now per cases; suppose i mod 2 = 0; hence IFEQ(i mod 2,0,FALSE,TRUE) = i mod 2 by FUNCOP_1:def 8; end; suppose A17: i mod 2 <> 0; hence IFEQ(i mod 2,0,FALSE,TRUE) = 1 by FUNCOP_1:def 8 .= i mod 2 by A17,NAT_D:12; end; end; A18: 2 to_power 0 = 1 by POWER:24; thus ((n+1)-BinarySequence i).j = ((n+1)-BinarySequence i)/.z by A1,A5 ,A6,FINSEQ_4:15 .= IFEQ((i div 2 to_power (1-'1)) mod 2,0,FALSE,TRUE) by A2,A4,A15 ,Def1 .= IFEQ((i div 1) mod 2,0,FALSE,TRUE) by A18,XREAL_1:232 .= IFEQ(i mod 2,0,FALSE,TRUE) by NAT_2:4 .= (<*i mod 2*> ^ (n-BinarySequence (i div 2))).j by A15,A16, FINSEQ_1:41; end; end; hence ((n+1)-BinarySequence i).j = (<*i mod 2*> ^ (n-BinarySequence (i div 2))).j; end; hence thesis by A1,A3,FINSEQ_2:9; end; theorem Th35: for n be non zero Nat for k be Nat holds k < 2 to_power n implies Absval (n-BinarySequence k) = k proof let n be non zero Nat; defpred P[Nat] means $1 < 2 to_power n implies Absval (n-BinarySequence $1) = $1; A1: for k be Nat st P[k] holds P[k+1] proof 0*n in BOOLEAN* by Th4; then 0*n is FinSequence of BOOLEAN by FINSEQ_1:def 11; then reconsider 0n = 0*n as Tuple of n,BOOLEAN; let k be Nat; assume A2: k < 2 to_power n implies Absval (n-BinarySequence k) = k; assume A3: k + 1 < 2 to_power n; then A4: k + 1 - 1 < 2 to_power n - 1 by XREAL_1:9; k < 2 to_power n by A3,NAT_1:13; then n-BinarySequence k <> 'not' 0n by A4,Lm4; then add_ovfl(n-BinarySequence k,Bin1 n) <> TRUE by Th23; then add_ovfl(n-BinarySequence k,Bin1 n) = FALSE by XBOOLEAN:def 3; then A5: n-BinarySequence k,Bin1 n are_summable by BINARITH:def 7; thus Absval (n-BinarySequence (k+1)) = Absval (n-BinarySequence k + Bin1 n ) by A3,Th33 .= Absval (n-BinarySequence k) + Absval (Bin1 n) by A5,BINARITH:22 .= k + 1 by A2,A3,Th11,NAT_1:13; end; A6: P[0] proof assume 0 < 2 to_power n; n-BinarySequence 0 = 0*n by Th25; hence thesis by Th6; end; thus for n being Nat holds P[n] from NAT_1:sch 2(A6,A1); end; theorem for n be non zero Nat for x be Tuple of n,BOOLEAN holds n -BinarySequence (Absval x) = x proof let n be non zero Nat; let x be Tuple of n,BOOLEAN; Absval x < 2 to_power n by Th1; then Absval (n-BinarySequence Absval x) = Absval x by Th35; hence thesis by Th2; end;