:: by Robert Milewski

::

:: Received February 24, 1998

:: Copyright (c) 1998-2012 Association of Mizar Users

begin

theorem Th2: :: BINARI_3:2

for n being non empty Nat

for F1, F2 being Tuple of n, BOOLEAN st Absval F1 = Absval F2 holds

F1 = F2

for F1, F2 being Tuple of n, BOOLEAN st Absval F1 = Absval F2 holds

F1 = F2

proof end;

theorem :: BINARI_3:7

for n being non empty Nat

for F being Tuple of n, BOOLEAN st F = 0* n holds

Absval ('not' F) = (2 to_power n) - 1

for F being Tuple of n, BOOLEAN st F = 0* n holds

Absval ('not' F) = (2 to_power n) - 1

proof end;

theorem Th12: :: BINARI_3:12

for x, y being Element of BOOLEAN holds

( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) & ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )

( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) & ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )

proof end;

theorem Th13: :: BINARI_3:13

for x, y being Element of BOOLEAN holds

( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE & y = TRUE ) )

( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE & y = TRUE ) )

proof end;

theorem Th19: :: BINARI_3:19

for n being non empty Nat

for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

for k being non empty Nat st k <> 1 & k <= n holds

( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )

for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

for k being non empty Nat st k <> 1 & k <= n holds

( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )

proof end;

theorem Th20: :: BINARI_3:20

for n being non empty Nat

for x being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

carry (x,(Bin1 n)) = 'not' (Bin1 n)

for x being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

carry (x,(Bin1 n)) = 'not' (Bin1 n)

proof end;

theorem Th21: :: BINARI_3:21

for n being non empty Nat

for x, y being Tuple of n, BOOLEAN st y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

x = 'not' y

for x, y being Tuple of n, BOOLEAN st y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds

x = 'not' y

proof end;

theorem Th22: :: BINARI_3:22

for n being non empty Nat

for y being Tuple of n, BOOLEAN st y = 0* n holds

carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)

for y being Tuple of n, BOOLEAN st y = 0* n holds

carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)

proof end;

theorem Th23: :: BINARI_3:23

for n being non empty Nat

for x, y being Tuple of n, BOOLEAN st y = 0* n holds

( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )

for x, y being Tuple of n, BOOLEAN st y = 0* n holds

( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )

proof end;

theorem Th24: :: BINARI_3:24

for n being non empty Nat

for z being Tuple of n, BOOLEAN st z = 0* n holds

('not' z) + (Bin1 n) = z

for z being Tuple of n, BOOLEAN st z = 0* n holds

('not' z) + (Bin1 n) = z

proof end;

begin

definition

let n, k be Nat;

ex b_{1} being Tuple of n, BOOLEAN st

for i being Nat st i in Seg n holds

b_{1} /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

for b_{1}, b_{2} being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds

b_{1} /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) holds

b_{1} = b_{2}

end;
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 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);

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines -BinarySequence BINARI_3:def 1 :

for n, k being Nat

for b_{3} being Tuple of n, BOOLEAN holds

( b_{3} = n -BinarySequence k iff for i being Nat st i in Seg n holds

b_{3} /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) );

for n, k being Nat

for b

( b

b

theorem Th27: :: BINARI_3:27

for n being non empty Nat

for k being Nat st k < 2 to_power n holds

(n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>

for k being Nat st k < 2 to_power n holds

(n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>

proof end;

Lm1: for n being non empty Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*>

proof end;

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

proof end;

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*>

proof end;

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 )

proof end;

theorem :: BINARI_3:29

theorem :: BINARI_3:30

theorem :: BINARI_3:31

theorem Th32: :: BINARI_3:32

for n being non empty Nat

for k being Nat st k + 1 < 2 to_power n holds

add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE

for k being Nat st k + 1 < 2 to_power n holds

add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE

proof end;

theorem Th33: :: BINARI_3:33

for n being non empty Nat

for k being Nat st k + 1 < 2 to_power n holds

n -BinarySequence (k + 1) = (n -BinarySequence k) + (Bin1 n)

for k being Nat st k + 1 < 2 to_power n holds

n -BinarySequence (k + 1) = (n -BinarySequence k) + (Bin1 n)

proof end;

theorem Th35: :: BINARI_3:35

for n being non empty Nat

for k being Nat st k < 2 to_power n holds

Absval (n -BinarySequence k) = k

for k being Nat st k < 2 to_power n holds

Absval (n -BinarySequence k) = k

proof end;