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


begin

theorem Th1: :: BINARI_3:1
for n being non empty Nat
for F being Tuple of n, BOOLEAN holds Absval F < 2 to_power n
proofend;

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
proofend;

theorem :: BINARI_3:3
for t1, t2 being FinSequence st Rev t1 = Rev t2 holds
t1 = t2
proofend;

theorem Th4: :: BINARI_3:4
for n being Nat holds 0* n in BOOLEAN *
proofend;

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
proofend;

theorem Th6: :: BINARI_3:6
for n being non empty Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval F = 0
proofend;

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
proofend;

theorem :: BINARI_3:8
for n being Nat holds Rev (0* n) = 0* n
proofend;

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
proofend;

theorem Th10: :: BINARI_3:10
Bin1 1 = <*TRUE*>
proofend;

theorem Th11: :: BINARI_3:11
for n being non empty Nat holds Absval (Bin1 n) = 1
proofend;

theorem Th12: :: BINARI_3:12
for x, y being Element of BOOLEAN holds
( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) &amp; ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) &amp; ( x 'or' y = FALSE implies ( x = FALSE &amp; y = FALSE ) ) &amp; ( x = FALSE &amp; y = FALSE implies x 'or' y = FALSE ) )
proofend;

theorem Th13: :: BINARI_3:13
for x, y being Element of BOOLEAN holds
( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE &amp; y = TRUE ) )
proofend;

theorem Th14: :: BINARI_3:14
'not' <*FALSE*> = <*TRUE*>
proofend;

theorem :: BINARI_3:15
'not' <*TRUE*> = <*FALSE*>
proofend;

theorem :: BINARI_3:16
<*FALSE*> + <*FALSE*> = <*FALSE*>
proofend;

theorem Th17: :: BINARI_3:17
( <*FALSE*> + <*TRUE*> = <*TRUE*> &amp; <*TRUE*> + <*FALSE*> = <*TRUE*> )
proofend;

theorem :: BINARI_3:18
<*TRUE*> + <*TRUE*> = <*FALSE*>
proofend;

theorem Th19: :: BINARI_3:19
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st x /. n = TRUE &amp; (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non empty Nat st k <> 1 &amp; k <= n holds
( x /. k = TRUE &amp; (carry (x,(Bin1 n))) /. k = TRUE )
proofend;

theorem Th20: :: BINARI_3:20
for n being non empty Nat
for x being Tuple of n, BOOLEAN st x /. n = TRUE &amp; (carry (x,(Bin1 n))) /. n = TRUE holds
carry (x,(Bin1 n)) = 'not' (Bin1 n)
proofend;

theorem Th21: :: BINARI_3:21
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st y = 0* n &amp; x /. n = TRUE &amp; (carry (x,(Bin1 n))) /. n = TRUE holds
x = 'not' y
proofend;

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

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

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
proofend;

begin

definition
let n, k be Nat;
funcn -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)
proofend;
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) ) &amp; ( 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
proofend;
end;

:: deftheorem Def1 defines -BinarySequence BINARI_3:def_1_:_
 for n, k being Nat
for b3 being Tuple of n, BOOLEAN holds
( b3 = n -BinarySequence k iff for i being Nat st i in Seg n holds
b3 /. 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
proofend;

theorem Th26: :: BINARI_3:26
for n, k being Nat st k < 2 to_power n holds
((n + 1) -BinarySequence k) . (n + 1) = FALSE
proofend;

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

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

Lm2:  for n being non empty Nat
for k being Nat st 2 to_power n <= k &amp; k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE
proofend;

Lm3:  for n being non empty Nat
for k being Nat st 2 to_power n <= k &amp; k < 2 to_power (n + 1) holds
(n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
proofend;

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

theorem Th28: :: BINARI_3:28
for i being Nat holds (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
proofend;

theorem :: BINARI_3:29
for n being non empty Nat
for k being Nat st 2 to_power n <= k &amp; k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE by Lm2;

theorem :: BINARI_3:30
for n being non empty Nat
for k being Nat st 2 to_power n <= k &amp; 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 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 ) by Lm4;

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
proofend;

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

theorem :: BINARI_3:34
for n, i being Nat holds (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2))
proofend;

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
proofend;

theorem :: BINARI_3:36
for n being non empty Nat
for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x
proofend;