:: Binary Arithmetics. Binary Sequences
:: by Robert Milewski
::
:: Received February 24, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

theorem Th1: :: BINARI_3:1

for n being non zero Nat
for F being Tuple of n, BOOLEAN holds Absval F < 2 to_power n

proof end;

theorem Th2: :: BINARI_3:2

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

proof end;

theorem :: BINARI_3:3

for t1, t2 being FinSequence st Rev t1 = Rev t2 holds
t1 = t2

proof end;

theorem Th4: :: BINARI_3:4

for n being Nat holds 0* n in BOOLEAN *

proof end;

theorem Th5: :: BINARI_3:5

for n being Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1

proof end;

theorem Th6: :: BINARI_3:6

for n being non zero Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval F = 0

proof end;

theorem :: BINARI_3:7

for n being non zero Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval ('not' F) = (2 to_power n) - 1

proof end;

theorem :: BINARI_3:8

for n being Nat holds Rev (0* n) = 0* n

proof end;

theorem :: BINARI_3:9

for n being Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
Rev ('not' y) = 'not' y

proof end;

theorem Th10: :: BINARI_3:10

Bin1 1 = <*TRUE*>

proof end;

theorem Th11: :: BINARI_3:11

for n being non zero Nat holds Absval (Bin1 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 ) )

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

proof end;

theorem Th14: :: BINARI_3:14

'not' <*FALSE*> = <*TRUE*>

proof end;

theorem :: BINARI_3:15

'not' <*TRUE*> = <*FALSE*>

proof end;

theorem :: BINARI_3:16

<*FALSE*> + <*FALSE*> = <*FALSE*>

proof end;

theorem Th17: :: BINARI_3:17

( <*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE*> )

proof end;

theorem :: BINARI_3:18

<*TRUE*> + <*TRUE*> = <*FALSE*>

proof end;

theorem Th19: :: BINARI_3:19

for n being non zero Nat
for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )

proof end;

registration

cluster V15() zero -> non positive for set ;

coherence
for b₁ being Nat st b₁ is zero holds
not b₁ is positive ;

end;

theorem Th20: :: BINARI_3:20

for n being non zero 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)

proof end;

theorem Th21: :: BINARI_3:21

for n being non zero 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

proof end;

theorem Th22: :: BINARI_3:22

for n being non zero Nat
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 zero Nat
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 zero Nat
for z being Tuple of n, BOOLEAN st z = 0* n holds
('not' z) + (Bin1 n) = z

proof end;

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 b₁ being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b₁ /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b₁ /. 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₂ /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines -BinarySequence BINARI_3:def 1 :
for n, k being Nat
for b₃ being Tuple of n, BOOLEAN holds
( b₃ = n -BinarySequence k iff for i being Nat st i in Seg n holds
b₃ /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) );

theorem Th25: :: BINARI_3:25

for n being Nat holds n -BinarySequence 0 = 0* n

proof end;

theorem Th26: :: BINARI_3:26

for n, k being Nat st k < 2 to_power n holds
((n + 1) -BinarySequence k) . (n + 1) = FALSE

proof end;

theorem Th27: :: BINARI_3:27

for n being non zero Nat
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 zero Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*>

proof end;

Lm2: for n being non zero 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 zero 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 zero 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 Th28: :: BINARI_3:28

for i being Nat holds (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>

proof end;

theorem :: BINARI_3:29

for n being non zero 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 by Lm2;

theorem :: BINARI_3:30

for n being non zero 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*> by Lm3;

theorem :: BINARI_3:31

for n being non zero 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 ) by Lm4;

theorem Th32: :: BINARI_3:32

for n being non zero Nat
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 zero Nat
for k being Nat st k + 1 < 2 to_power n holds
n -BinarySequence (k + 1) = (n -BinarySequence k) + (Bin1 n)

proof end;

theorem :: BINARI_3:34

for n, i being Nat holds (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2))

proof end;

theorem Th35: :: BINARI_3:35

for n being non zero Nat
for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k

proof end;

theorem :: BINARI_3:36

for n being non zero Nat
for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x

proof end;