:: Binary Arithmetics. Binary Sequences
:: by Robert Milewski
::
:: Received February 24, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem Th1: :: BINARI_3:1
theorem Th2: :: BINARI_3:2
theorem :: BINARI_3:3
theorem :: BINARI_3:4
canceled;
theorem Th5: :: BINARI_3:5
theorem Th6: :: BINARI_3:6
theorem Th7: :: BINARI_3:7
theorem :: BINARI_3:8
theorem :: BINARI_3:9
theorem :: BINARI_3:10
theorem Th11: :: BINARI_3:11
theorem Th12: :: BINARI_3:12
theorem Th13: :: BINARI_3:13
theorem Th14: :: BINARI_3:14
theorem Th15: :: BINARI_3:15
theorem :: BINARI_3:16
theorem :: BINARI_3:17
theorem Th18: :: BINARI_3:18
theorem :: BINARI_3:19
theorem Th20: :: BINARI_3:20
theorem Th21: :: BINARI_3:21
theorem Th22: :: BINARI_3:22
theorem Th23: :: BINARI_3:23
theorem Th24: :: BINARI_3:24
theorem Th25: :: BINARI_3:25
definition
let n,
k be
Nat;
func n -BinarySequence k -> Tuple of
n,
BOOLEAN means :
Def1:
:: BINARI_3:def 1
for
i being
Nat st
i in Seg n holds
it /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),
0 ,
FALSE ,
TRUE ;
existence
ex b1 being Tuple of n,BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE
uniqueness
for b1, b2 being Tuple of n,BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE ) holds
b1 = b2
end;
:: deftheorem Def1 defines -BinarySequence BINARI_3:def 1 :
theorem Th26: :: BINARI_3:26
theorem Th27: :: BINARI_3:27
theorem Th28: :: BINARI_3:28
Lm1:
for n being non empty Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE *>
Lm2:
for n being non empty Nat
for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE
Lm3:
for n being non empty Nat
for k being 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 *>
Lm4:
for n being non empty Nat
for k being Nat st k < 2 to_power n holds
for x being Tuple of n,BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
theorem Th29: :: BINARI_3:29
theorem :: BINARI_3:30
theorem :: BINARI_3:31
theorem :: BINARI_3:32
theorem Th33: :: BINARI_3:33
theorem Th34: :: BINARI_3:34
theorem :: BINARI_3:35
theorem Th36: :: BINARI_3:36
theorem :: BINARI_3:37