:: Definitions of Radix-2k Signed-Digit number and its adder algorithm :: by Yoshinori Fujisawa and Yasushi Fuwa :: :: Received September 7, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin theorem Th1: :: RADIX_1:1 for n, k being Nat st n mod k = k - 1 holds (n + 1) mod k = 0 by NAT_D:69; theorem Th2: :: RADIX_1:2 for n, k being Nat st n mod k < k - 1 holds (n + 1) mod k = (n mod k) + 1 by NAT_D:70; theorem Th3: :: RADIX_1:3 for m, k, n being Nat st m <> 0 holds (k mod (m * n)) mod n = k mod n proofend; theorem :: RADIX_1:4 for k, n being Nat holds ( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 ) proofend; theorem Th5: :: RADIX_1:5 for i, k, n being Nat st i <> 0 & k <> 0 holds (n mod (i |^ k)) div (i |^ (k -' 1)) < i proofend; theorem :: RADIX_1:6 canceled; theorem :: RADIX_1:7 for i2, i3, i1 being Integer st i2 > 0 & i3 >= 0 holds (i1 mod (i2 * i3)) mod i3 = i1 mod i3 proofend; begin definition let n be Nat; func Radix n -> Element of NAT equals :: RADIX_1:def 1 2 to_power n; correctness coherence 2 to_power n is Element of NAT ; by ORDINAL1:def_12; end; :: deftheorem defines Radix RADIX_1:def_1_:_ for n being Nat holds Radix n = 2 to_power n; definition let k be Nat; funck -SD -> set equals :: RADIX_1:def 2 { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ; correctness coherence { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } is set ; ; end; :: deftheorem defines -SD RADIX_1:def_2_:_ for k being Nat holds k -SD = { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ; Lm1: for k being Nat st k >= 2 holds Radix k >= 2 + 2 proofend; theorem Th8: :: RADIX_1:8 for e being set holds ( e in 0 -SD iff e = 0 ) proofend; theorem :: RADIX_1:9 0 -SD = {0} by Th8, TARSKI:def_1; theorem Th10: :: RADIX_1:10 for k being Nat holds k -SD c= (k + 1) -SD proofend; theorem Th11: :: RADIX_1:11 for e being set for k being Nat st e in k -SD holds e is Integer proofend; theorem Th12: :: RADIX_1:12 for k being Nat holds k -SD c= INT proofend; theorem Th13: :: RADIX_1:13 for i1 being Integer for k being Nat st i1 in k -SD holds ( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 ) proofend; theorem Th14: :: RADIX_1:14 for k being Nat holds 0 in k -SD proofend; registration let k be Nat; clusterk -SD -> non empty ; coherence not k -SD is empty by Th14; end; definition let k be Nat; :: original:-SD redefine funck -SD -> non empty Subset of INT; coherence k -SD is non empty Subset of INT by Th12; end; begin theorem Th15: :: RADIX_1:15 for i, n, k being Nat for a being Tuple of n,k -SD st i in Seg n holds a . i is Element of k -SD proofend; definition let i, k, n be Nat; let x be Tuple of n,k -SD ; func DigA (x,i) -> Integer equals :Def3: :: RADIX_1:def 3 x . i if i in Seg n 0 if i = 0 ; coherence ( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def_2; consistency for b1 being Integer st i in Seg n & i = 0 holds ( b1 = x . i iff b1 = 0 ) by FINSEQ_1:1; end; :: deftheorem Def3 defines DigA RADIX_1:def_3_:_ for i, k, n being Nat for x being Tuple of n,k -SD holds ( ( i in Seg n implies DigA (x,i) = x . i ) & ( i = 0 implies DigA (x,i) = 0 ) ); definition let i, k, n be Nat; let x be Tuple of n,k -SD ; func DigB (x,i) -> Element of INT equals :: RADIX_1:def 4 DigA (x,i); coherence DigA (x,i) is Element of INT by INT_1:def_2; end; :: deftheorem defines DigB RADIX_1:def_4_:_ for i, k, n being Nat for x being Tuple of n,k -SD holds DigB (x,i) = DigA (x,i); theorem Th16: :: RADIX_1:16 for i, n, k being Nat for a being Tuple of n,k -SD st i in Seg n holds DigA (a,i) is Element of k -SD proofend; theorem Th17: :: RADIX_1:17 for m being Nat for x being Tuple of 1, INT st x /. 1 = m holds x = <*m*> proofend; definition let i, k, n be Nat; let x be Tuple of n,k -SD ; func SubDigit (x,i,k) -> Element of INT equals :: RADIX_1:def 5 ((Radix k) |^ (i -' 1)) * (DigB (x,i)); coherence ((Radix k) |^ (i -' 1)) * (DigB (x,i)) is Element of INT by INT_1:def_2; end; :: deftheorem defines SubDigit RADIX_1:def_5_:_ for i, k, n being Nat for x being Tuple of n,k -SD holds SubDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB (x,i)); definition let n, k be Nat; let x be Tuple of n,k -SD ; func DigitSD x -> Tuple of n, INT means :Def6: :: RADIX_1:def 6 for i being Nat st i in Seg n holds it /. i = SubDigit (x,i,k); existence ex b1 being Tuple of n, INT st for i being Nat st i in Seg n holds b1 /. i = SubDigit (x,i,k) proofend; uniqueness for b1, b2 being Tuple of n, INT st ( for i being Nat st i in Seg n holds b1 /. i = SubDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds b2 /. i = SubDigit (x,i,k) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines DigitSD RADIX_1:def_6_:_ for n, k being Nat for x being Tuple of n,k -SD for b4 being Tuple of n, INT holds ( b4 = DigitSD x iff for i being Nat st i in Seg n holds b4 /. i = SubDigit (x,i,k) ); definition let n, k be Nat; let x be Tuple of n,k -SD ; func SDDec x -> Integer equals :: RADIX_1:def 7 Sum (DigitSD x); coherence Sum (DigitSD x) is Integer ; end; :: deftheorem defines SDDec RADIX_1:def_7_:_ for n, k being Nat for x being Tuple of n,k -SD holds SDDec x = Sum (DigitSD x); definition let i, k, x be Nat; func DigitDC (x,i,k) -> Element of k -SD equals :: RADIX_1:def 8 (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)); coherence (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD proofend; end; :: deftheorem defines DigitDC RADIX_1:def_8_:_ for i, k, x being Nat holds DigitDC (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)); definition let k, n, x be Nat; func DecSD (x,n,k) -> Tuple of n,k -SD means :Def9: :: RADIX_1:def 9 for i being Nat st i in Seg n holds DigA (it,i) = DigitDC (x,i,k); existence ex b1 being Tuple of n,k -SD st for i being Nat st i in Seg n holds DigA (b1,i) = DigitDC (x,i,k) proofend; uniqueness for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds DigA (b1,i) = DigitDC (x,i,k) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = DigitDC (x,i,k) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines DecSD RADIX_1:def_9_:_ for k, n, x being Nat for b4 being Tuple of n,k -SD holds ( b4 = DecSD (x,n,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = DigitDC (x,i,k) ); begin definition let x be Integer; func SD_Add_Carry x -> Integer equals :Def10: :: RADIX_1:def 10 1 if x > 2 - 1 if x < - 2 otherwise 0 ; coherence ( ( x > 2 implies 1 is Integer ) & ( x < - 2 implies - 1 is Integer ) & ( not x > 2 & not x < - 2 implies 0 is Integer ) ) ; consistency for b1 being Integer st x > 2 & x < - 2 holds ( b1 = 1 iff b1 = - 1 ) ; end; :: deftheorem Def10 defines SD_Add_Carry RADIX_1:def_10_:_ for x being Integer holds ( ( x > 2 implies SD_Add_Carry x = 1 ) & ( x < - 2 implies SD_Add_Carry x = - 1 ) & ( not x > 2 & not x < - 2 implies SD_Add_Carry x = 0 ) ); theorem Th18: :: RADIX_1:18 SD_Add_Carry 0 = 0 by Def10; Lm2: for x being Integer holds ( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 ) proofend; definition let x be Integer; let k be Nat; func SD_Add_Data (x,k) -> Integer equals :: RADIX_1:def 11 x - ((SD_Add_Carry x) * (Radix k)); coherence x - ((SD_Add_Carry x) * (Radix k)) is Integer ; end; :: deftheorem defines SD_Add_Data RADIX_1:def_11_:_ for x being Integer for k being Nat holds SD_Add_Data (x,k) = x - ((SD_Add_Carry x) * (Radix k)); theorem :: RADIX_1:19 for k being Nat holds SD_Add_Data (0,k) = 0 by Th18; theorem Th20: :: RADIX_1:20 for i1, i2 being Integer for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds ( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 ) proofend; begin :: expressed as n digits Radix-2^k SD number definition let n, x, k be Nat; predx is_represented_by n,k means :Def12: :: RADIX_1:def 12 x < (Radix k) |^ n; end; :: deftheorem Def12 defines is_represented_by RADIX_1:def_12_:_ for n, x, k being Nat holds ( x is_represented_by n,k iff x < (Radix k) |^ n ); theorem Th21: :: RADIX_1:21 for m, k being Nat st m is_represented_by 1,k holds DigA ((DecSD (m,1,k)),1) = m proofend; theorem :: RADIX_1:22 for k, n being Nat st n >= 1 holds for m being Nat st m is_represented_by n,k holds m = SDDec (DecSD (m,n,k)) proofend; theorem Th23: :: RADIX_1:23 for m, k, n being Nat st m is_represented_by 1,k & n is_represented_by 1,k holds SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n) proofend; Lm3: for n, m, k, i being Nat st i in Seg n holds DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i) proofend; theorem Th24: :: RADIX_1:24 for m, n, k being Nat st m is_represented_by n + 1,k holds DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n) proofend; begin :: on Radix-2^k SD number definition let k, i, n be Nat; let x, y be Tuple of n,k -SD ; assume that A1: i in Seg n and A2: k >= 2 ; func Add (x,y,i,k) -> Element of k -SD equals :Def13: :: RADIX_1:def 13 (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))); coherence (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) is Element of k -SD proofend; end; :: deftheorem Def13 defines Add RADIX_1:def_13_:_ for k, i, n being Nat for x, y being Tuple of n,k -SD st i in Seg n & k >= 2 holds Add (x,y,i,k) = (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))); definition let n, k be Nat; let x, y be Tuple of n,k -SD ; funcx '+' y -> Tuple of n,k -SD means :Def14: :: RADIX_1:def 14 for i being Nat st i in Seg n holds DigA (it,i) = Add (x,y,i,k); existence ex b1 being Tuple of n,k -SD st for i being Nat st i in Seg n holds DigA (b1,i) = Add (x,y,i,k) proofend; uniqueness for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds DigA (b1,i) = Add (x,y,i,k) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = Add (x,y,i,k) ) holds b1 = b2 proofend; end; :: deftheorem Def14 defines '+' RADIX_1:def_14_:_ for n, k being Nat for x, y, b5 being Tuple of n,k -SD holds ( b5 = x '+' y iff for i being Nat st i in Seg n holds DigA (b5,i) = Add (x,y,i,k) ); theorem Th25: :: RADIX_1:25 for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k) proofend; theorem :: RADIX_1:26 for n being Nat st n >= 1 holds for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n))))) proofend;