:: BINARI_4 semantic presentation

theorem Th1: :: BINARI_4:1

for b₁ being Nat st b₁ > 0 holds
b₁ * 2 >= b₁ + 1

proof end;

theorem Th2: :: BINARI_4:2

for b₁ being Nat holds 2 to_power b₁ >= b₁

proof end;

theorem Th3: :: BINARI_4:3

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

proof end;

theorem Th4: :: BINARI_4:4

for b₁, b₂, b₃ being Nat st b₃ <= b₁ & b₁ <= b₂ & not b₃ = b₁ holds
( b₃ + 1 <= b₁ & b₁ <= b₂ )

proof end;

theorem Th5: :: BINARI_4:5

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

proof end;

theorem Th6: :: BINARI_4:6

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

proof end;

theorem Th7: :: BINARI_4:7

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

proof end;

theorem Th8: :: BINARI_4:8

for b₁, b₂, b₃ being Nat st b₁ + b₂ <= b₃ - 1 holds
( b₁ < b₃ & b₂ < b₃ )

proof end;

theorem Th9: :: BINARI_4:9

for b₁, b₂, b₃ being Integer st b₁ <= b₂ + b₃ & b₂ < 0 & b₃ < 0 holds
( b₁ < b₂ & b₁ < b₃ )

proof end;

theorem Th10: :: BINARI_4:10

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

proof end;

theorem Th11: :: BINARI_4:11

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

proof end;

theorem Th12: :: BINARI_4:12

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN st b₂ /. b₁ = TRUE holds
Absval b₂ >= 2 to_power (b₁ -' 1)

proof end;

theorem Th13: :: BINARI_4:13

for b₁ being non empty Nat
for b₂, b₃ being Nat st b₂ + b₃ <= (2 to_power (b₁ -' 1)) - 1 holds
(carry (b₁ -BinarySequence b₂),(b₁ -BinarySequence b₃)) /. b₁ = FALSE

proof end;

theorem Th14: :: BINARI_4:14

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

proof end;

theorem Th15: :: BINARI_4:15

for b₁ being Tuple of 1,BOOLEAN st b₁ = <*TRUE *> holds
Intval b₁ = - 1

proof end;

theorem Th16: :: BINARI_4:16

for b₁ being Tuple of 1,BOOLEAN st b₁ = <*FALSE *> holds
Intval b₁ = 0

proof end;

theorem Th17: :: BINARI_4:17

for b₁ being boolean set holds TRUE 'or' b₁ = TRUE

proof end;

theorem Th18: :: BINARI_4:18

for b₁ being non empty Nat holds
( 0 <= (2 to_power (b₁ -' 1)) - 1 & - (2 to_power (b₁ -' 1)) <= 0 )

proof end;

theorem Th19: :: BINARI_4:19

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

proof end;

theorem Th20: :: BINARI_4:20

for b₁ being non empty Nat
for b₂ being Integer holds (b₂ * b₁) mod b₁ = 0

proof end;

definition

let c₁, c₂ be Nat;
func MajP c₁,c₂ -> Nat means :Def1: :: BINARI_4:def 1
( 2 to_power a₃ >= a₂ & a₃ >= a₁ & ( for b₁ being Nat st 2 to_power b₁ >= a₂ & b₁ >= a₁ holds
b₁ >= a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines MajP BINARI_4:def 1 :

theorem Th21: :: BINARI_4:21

for b₁, b₂, b₃ being Nat st b₁ >= b₂ holds
MajP b₃,b₁ >= MajP b₃,b₂

proof end;

theorem Th22: :: BINARI_4:22

for b₁, b₂, b₃ being Nat st b₁ >= b₂ holds
MajP b₁,b₃ >= MajP b₂,b₃

proof end;

theorem Th23: :: BINARI_4:23

for b₁ being Nat st b₁ >= 1 holds
MajP b₁,1 = b₁

proof end;

theorem Th24: :: BINARI_4:24

for b₁, b₂ being Nat st b₁ <= 2 to_power b₂ holds
MajP b₂,b₁ = b₂

proof end;

theorem Th25: :: BINARI_4:25

for b₁, b₂ being Nat st b₁ > 2 to_power b₂ holds
MajP b₂,b₁ > b₂

proof end;

definition

let c₁ be Nat;
let c₂ be Integer;
func 2sComplement c₁,c₂ -> Tuple of a₁,BOOLEAN equals :Def2: :: BINARI_4:def 2
a₁ -BinarySequence (abs ((2 to_power (MajP a₁,(abs a₂))) + a₂)) if a₂ < 0
otherwise a₁ -BinarySequence (abs a₂);
correctness ;

end;

:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :

theorem Th26: :: BINARI_4:26

for b₁ being Nat holds 2sComplement b₁,0 = 0* b₁

proof end;

theorem Th27: :: BINARI_4:27

for b₁ being non empty Nat
for b₂ being Integer st b₂ <= (2 to_power (b₁ -' 1)) - 1 & - (2 to_power (b₁ -' 1)) <= b₂ holds
Intval (2sComplement b₁,b₂) = b₂

proof end;

Lemma19: for b₁ being non empty Nat
for b₂, b₃ being Nat st b₂ mod b₁ = b₃ mod b₁ & b₂ > b₃ holds
ex b₄ being Integer st b₂ = b₃ + (b₄ * b₁)

proof end;

Lemma20: for b₁ being non empty Nat
for b₂, b₃ being Nat st b₂ mod b₁ = b₃ mod b₁ holds
ex b₄ being Integer st b₂ = b₃ + (b₄ * b₁)

proof end;

Lemma21: for b₁ being non empty Nat
for b₂, b₃, b₄ being Nat st b₄ < b₁ & b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
(b₂ div (2 to_power b₄)) mod 2 = (b₃ div (2 to_power b₄)) mod 2

proof end;

Lemma22: for b₁ being non empty Nat
for b₂, b₃ being Integer st b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
((2 to_power (MajP b₁,(abs b₂))) + b₂) mod (2 to_power b₁) = ((2 to_power (MajP b₁,(abs b₃))) + b₃) mod (2 to_power b₁)

proof end;

Lemma23: for b₁ being non empty Nat
for b₂, b₃ being Integer st b₂ >= 0 & b₃ >= 0 & b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
2sComplement b₁,b₂ = 2sComplement b₁,b₃

proof end;

Lemma24: for b₁ being non empty Nat
for b₂, b₃ being Integer st b₂ < 0 & b₃ < 0 & b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
2sComplement b₁,b₂ = 2sComplement b₁,b₃

proof end;

theorem Th28: :: BINARI_4:28

for b₁ being non empty Nat
for b₂, b₃ being Integer st ( ( b₂ >= 0 & b₃ >= 0 ) or ( b₂ < 0 & b₃ < 0 ) ) & b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
2sComplement b₁,b₂ = 2sComplement b₁,b₃ by Lemma23, Lemma24;

theorem Th29: :: BINARI_4:29

for b₁ being non empty Nat
for b₂, b₃ being Integer st ( ( b₂ >= 0 & b₃ >= 0 ) or ( b₂ < 0 & b₃ < 0 ) ) & b₂,b₃ are_congruent_mod 2 to_power b₁ holds
2sComplement b₁,b₂ = 2sComplement b₁,b₃

proof end;

theorem Th30: :: BINARI_4:30

for b₁ being non empty Nat
for b₂, b₃ being Nat st b₂ mod (2 to_power b₁) = b₃ mod (2 to_power b₁) holds
b₁ -BinarySequence b₂ = b₁ -BinarySequence b₃

proof end;

theorem Th31: :: BINARI_4:31

for b₁ being non empty Nat
for b₂, b₃ being Nat st b₂,b₃ are_congruent_mod 2 to_power b₁ holds
b₁ -BinarySequence b₂ = b₁ -BinarySequence b₃

proof end;

theorem Th32: :: BINARI_4:32

for b₁ being non empty Nat
for b₂ being Integer
for b₃ being Nat st 1 <= b₃ & b₃ <= b₁ holds
(2sComplement (b₁ + 1),b₂) /. b₃ = (2sComplement b₁,b₂) /. b₃

proof end;

theorem Th33: :: BINARI_4:33

for b₁ being Nat
for b₂ being Integer ex b₃ being Element of BOOLEAN st 2sComplement (b₁ + 1),b₂ = (2sComplement b₁,b₂) ^ <*b₃*>

proof end;

theorem Th34: :: BINARI_4:34

for b₁, b₂ being Nat ex b₃ being Element of BOOLEAN st (b₁ + 1) -BinarySequence b₂ = (b₁ -BinarySequence b₂) ^ <*b₃*>

proof end;

theorem Th35: :: BINARI_4:35

for b₁, b₂ being Integer
for b₃ being non empty Nat st - (2 to_power b₃) <= b₁ + b₂ & b₁ < 0 & b₂ < 0 & - (2 to_power (b₃ -' 1)) <= b₁ & - (2 to_power (b₃ -' 1)) <= b₂ holds
(carry (2sComplement (b₃ + 1),b₁),(2sComplement (b₃ + 1),b₂)) /. (b₃ + 1) = TRUE

proof end;

theorem Th36: :: BINARI_4:36

for b₁, b₂ being Integer
for b₃ being non empty Nat st - (2 to_power (b₃ -' 1)) <= b₁ + b₂ & b₁ + b₂ <= (2 to_power (b₃ -' 1)) - 1 & b₁ >= 0 & b₂ >= 0 holds
Intval ((2sComplement b₃,b₁) + (2sComplement b₃,b₂)) = b₁ + b₂

proof end;

theorem Th37: :: BINARI_4:37

for b₁, b₂ being Integer
for b₃ being non empty Nat st - (2 to_power ((b₃ + 1) -' 1)) <= b₁ + b₂ & b₁ + b₂ <= (2 to_power ((b₃ + 1) -' 1)) - 1 & b₁ < 0 & b₂ < 0 & - (2 to_power (b₃ -' 1)) <= b₁ & - (2 to_power (b₃ -' 1)) <= b₂ holds
Intval ((2sComplement (b₃ + 1),b₁) + (2sComplement (b₃ + 1),b₂)) = b₁ + b₂

proof end;

theorem Th38: :: BINARI_4:38

for b₁, b₂ being Integer
for b₃ being non empty Nat st - (2 to_power (b₃ -' 1)) <= b₁ & b₁ <= (2 to_power (b₃ -' 1)) - 1 & - (2 to_power (b₃ -' 1)) <= b₂ & b₂ <= (2 to_power (b₃ -' 1)) - 1 & - (2 to_power (b₃ -' 1)) <= b₁ + b₂ & b₁ + b₂ <= (2 to_power (b₃ -' 1)) - 1 & ( ( b₁ >= 0 & b₂ < 0 ) or ( b₁ < 0 & b₂ >= 0 ) ) holds
Intval ((2sComplement b₃,b₁) + (2sComplement b₃,b₂)) = b₁ + b₂

proof end;