:: BINARI_3 semantic presentation

theorem Th1: :: BINARI_3:1

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN holds Absval b₂ < 2 to_power b₁

proof end;

theorem Th2: :: BINARI_3:2

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN st Absval b₂ = Absval b₃ holds
b₂ = b₃

proof end;

theorem Th3: :: BINARI_3:3

for b₁, b₂ being FinSequence st Rev b₁ = Rev b₂ holds
b₁ = b₂

proof end;

theorem Th4: :: BINARI_3:4

for b₁ being Nat holds 0* (b₁ + 1) = (0* b₁) ^ <*0*>

proof end;

theorem Th5: :: BINARI_3:5

for b₁ being Nat holds 0* b₁ in BOOLEAN *

proof end;

theorem Th6: :: BINARI_3:6

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
'not' b₂ = b₁ |-> 1

proof end;

theorem Th7: :: BINARI_3:7

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
Absval b₂ = 0

proof end;

theorem Th8: :: BINARI_3:8

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
Absval ('not' b₂) = (2 to_power b₁) - 1

proof end;

theorem Th9: :: BINARI_3:9

for b₁ being Nat holds Rev (0* b₁) = 0* b₁

proof end;

theorem Th10: :: BINARI_3:10

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
Rev ('not' b₂) = 'not' b₂

proof end;

theorem Th11: :: BINARI_3:11

Bin1 1 = <*TRUE *>

proof end;

theorem Th12: :: BINARI_3:12

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

proof end;

theorem Th13: :: BINARI_3:13

for b₁, b₂ being Element of BOOLEAN holds
( ( not b₁ 'or' b₂ = TRUE or b₁ = TRUE or b₂ = TRUE ) & ( ( b₁ = TRUE or b₂ = TRUE ) implies b₁ 'or' b₂ = TRUE ) & ( b₁ 'or' b₂ = FALSE implies ( b₁ = FALSE & b₂ = FALSE ) ) & ( b₁ = FALSE & b₂ = FALSE implies b₁ 'or' b₂ = FALSE ) )

proof end;

theorem Th14: :: BINARI_3:14

for b₁, b₂ being Element of BOOLEAN holds
( add_ovfl <*b₁*>,<*b₂*> = TRUE iff ( b₁ = TRUE & b₂ = TRUE ) )

proof end;

theorem Th15: :: BINARI_3:15

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

proof end;

theorem Th16: :: BINARI_3:16

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

proof end;

theorem Th17: :: BINARI_3:17

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

proof end;

theorem Th18: :: BINARI_3:18

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

proof end;

theorem Th19: :: BINARI_3:19

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

proof end;

theorem Th20: :: BINARI_3:20

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN st b₂ /. b₁ = TRUE & (carry b₂,(Bin1 b₁)) /. b₁ = TRUE holds
for b₄ being non empty Nat st b₄ <> 1 & b₄ <= b₁ holds
( b₂ /. b₄ = TRUE & (carry b₂,(Bin1 b₁)) /. b₄ = TRUE )

proof end;

theorem Th21: :: BINARI_3:21

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ /. b₁ = TRUE & (carry b₂,(Bin1 b₁)) /. b₁ = TRUE holds
carry b₂,(Bin1 b₁) = 'not' (Bin1 b₁)

proof end;

theorem Th22: :: BINARI_3:22

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN st b₃ = 0* b₁ & b₂ /. b₁ = TRUE & (carry b₂,(Bin1 b₁)) /. b₁ = TRUE holds
b₂ = 'not' b₃

proof end;

theorem Th23: :: BINARI_3:23

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
carry ('not' b₂),(Bin1 b₁) = 'not' (Bin1 b₁)

proof end;

theorem Th24: :: BINARI_3:24

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN st b₃ = 0* b₁ holds
( add_ovfl b₂,(Bin1 b₁) = TRUE iff b₂ = 'not' b₃ )

proof end;

theorem Th25: :: BINARI_3:25

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ = 0* b₁ holds
('not' b₂) + (Bin1 b₁) = b₂

proof end;

definition

let c₁, c₂ be Nat;
func c₁ -BinarySequence c₂ -> Tuple of a₁,BOOLEAN means :Def1: :: BINARI_3:def 1
for b₁ being Nat st b₁ in Seg a₁ holds
a₃ /. b₁ = IFEQ ((a₂ div (2 to_power (b₁ -' 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 b₁ being Nat holds b₁ -BinarySequence 0 = 0* b₁

proof end;

theorem Th27: :: BINARI_3:27

for b₁, b₂ being Nat st b₂ < 2 to_power b₁ holds
((b₁ + 1) -BinarySequence b₂) . (b₁ + 1) = FALSE

proof end;

theorem Th28: :: BINARI_3:28

for b₁ being non empty Nat
for b₂ being Nat st b₂ < 2 to_power b₁ holds
(b₁ + 1) -BinarySequence b₂ = (b₁ -BinarySequence b₂) ^ <*FALSE *>

proof end;

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

proof end;

Lemma24: for b₁ being non empty Nat
for b₂ being Nat st 2 to_power b₁ <= b₂ & b₂ < 2 to_power (b₁ + 1) holds
((b₁ + 1) -BinarySequence b₂) . (b₁ + 1) = TRUE

proof end;

Lemma25: for b₁ being non empty Nat
for b₂ being Nat st 2 to_power b₁ <= b₂ & b₂ < 2 to_power (b₁ + 1) holds
(b₁ + 1) -BinarySequence b₂ = (b₁ -BinarySequence (b₂ -' (2 to_power b₁))) ^ <*TRUE *>

proof end;

Lemma26: for b₁ being non empty Nat
for b₂ being Nat st b₂ < 2 to_power b₁ holds
for b₃ being Tuple of b₁,BOOLEAN st b₃ = 0* b₁ holds
( b₁ -BinarySequence b₂ = 'not' b₃ iff b₂ = (2 to_power b₁) - 1 )

proof end;

theorem Th29: :: BINARI_3:29

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

proof end;

theorem Th30: :: BINARI_3:30

for b₁ being non empty Nat
for b₂ being Nat st 2 to_power b₁ <= b₂ & b₂ < 2 to_power (b₁ + 1) holds
((b₁ + 1) -BinarySequence b₂) . (b₁ + 1) = TRUE by Lemma24;

theorem Th31: :: BINARI_3:31

for b₁ being non empty Nat
for b₂ being Nat st 2 to_power b₁ <= b₂ & b₂ < 2 to_power (b₁ + 1) holds
(b₁ + 1) -BinarySequence b₂ = (b₁ -BinarySequence (b₂ -' (2 to_power b₁))) ^ <*TRUE *> by Lemma25;

theorem Th32: :: BINARI_3:32

for b₁ being non empty Nat
for b₂ being Nat st b₂ < 2 to_power b₁ holds
for b₃ being Tuple of b₁,BOOLEAN st b₃ = 0* b₁ holds
( b₁ -BinarySequence b₂ = 'not' b₃ iff b₂ = (2 to_power b₁) - 1 ) by Lemma26;

theorem Th33: :: BINARI_3:33

for b₁ being non empty Nat
for b₂ being Nat st b₂ + 1 < 2 to_power b₁ holds
add_ovfl (b₁ -BinarySequence b₂),(Bin1 b₁) = FALSE

proof end;

theorem Th34: :: BINARI_3:34

for b₁ being non empty Nat
for b₂ being Nat st b₂ + 1 < 2 to_power b₁ holds
b₁ -BinarySequence (b₂ + 1) = (b₁ -BinarySequence b₂) + (Bin1 b₁)

proof end;

theorem Th35: :: BINARI_3:35

for b₁, b₂ being Nat holds (b₁ + 1) -BinarySequence b₂ = <*(b₂ mod 2)*> ^ (b₁ -BinarySequence (b₂ div 2))

proof end;

theorem Th36: :: BINARI_3:36

for b₁ being non empty Nat
for b₂ being Nat st b₂ < 2 to_power b₁ holds
Absval (b₁ -BinarySequence b₂) = b₂

proof end;

theorem Th37: :: BINARI_3:37

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN holds b₁ -BinarySequence (Absval b₂) = b₂

proof end;