:: BINARI_3 semantic presentation

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

proof end;

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

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 + 1) = (0* n) ^ <*0*>

proof end;

theorem Th5: :: BINARI_3:5

for n being Nat holds 0* n in BOOLEAN *

proof end;

theorem Th6: :: BINARI_3:6

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

proof end;

theorem Th7: :: BINARI_3:7

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

proof end;

theorem :: BINARI_3:8

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

proof end;

theorem :: BINARI_3:9

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

proof end;

theorem :: BINARI_3:10

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

proof end;

theorem Th11: :: BINARI_3:11

Bin1 1 = <*TRUE *>

proof end;

theorem Th12: :: BINARI_3:12

for n being non empty Nat holds Absval (Bin1 n) = 1

proof end;

theorem Th13: :: BINARI_3:13

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 Th14: :: BINARI_3:14

for x, y being Element of BOOLEAN holds
( add_ovfl <*x*>,<*y*> = TRUE iff ( x = TRUE & y = TRUE ) )

proof end;

theorem Th15: :: BINARI_3:15

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

proof end;

theorem :: BINARI_3:16

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

proof end;

theorem :: BINARI_3:17

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

proof end;

theorem Th18: :: BINARI_3:18

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

proof end;

theorem :: BINARI_3:19

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

proof end;

theorem Th20: :: BINARI_3:20

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 )

proof end;

theorem Th21: :: BINARI_3:21

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)

proof end;

theorem Th22: :: BINARI_3:22

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

proof end;

theorem Th23: :: BINARI_3:23

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)

proof end;

theorem Th24: :: BINARI_3:24

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 )

proof end;

theorem Th25: :: BINARI_3:25

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

proof end;

uniqueness

proof end;

end;

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

theorem Th26: :: BINARI_3:26

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

proof end;

theorem Th27: :: BINARI_3:27

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

proof end;

theorem Th28: :: BINARI_3:28

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

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 Th29: :: BINARI_3:29

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

proof end;

theorem :: BINARI_3:30

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 by Lm2;

theorem Th31: :: BINARI_3:31

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 *> by Lm3;

theorem Th32: :: BINARI_3:32

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 Th33: :: BINARI_3:33

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

proof end;

theorem Th34: :: BINARI_3:34

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)

proof end;

theorem :: BINARI_3:35

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

proof end;

theorem Th36: :: BINARI_3:36

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

proof end;

theorem :: BINARI_3:37

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

proof end;