:: 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 b1 being Nat st b1 is zero holds
not b1 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 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)
proof end;
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
proof end;
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
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;