:: BINARI_2 semantic presentation

definition

let c₁ be non empty set ;
let c₂ be non empty Subset of c₁;
let c₃, c₄ be set ;
let c₅, c₆ be Element of c₂;
redefine func IFEQ as IFEQ c₃,c₄,c₅,c₆ -> Element of a₂;
coherence

proof end;

end;

Lemma1: for b₁ being Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN st len b₂ = b₁ & len b₃ = b₁ & ( for b₄ being Nat st b₄ in Seg b₁ holds
b₂ /. b₄ = b₃ /. b₄ ) holds
b₂ = b₃

proof end;

definition

let c₁ be Nat;
func Bin1 c₁ -> Tuple of a₁,BOOLEAN means :Def1: :: BINARI_2:def 1
for b₁ being Nat st b₁ in Seg a₁ holds
a₂ /. b₁ = IFEQ b₁,1,TRUE ,FALSE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :

definition

let c₁ be non empty Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
func Neg2 c₂ -> Tuple of a₁,BOOLEAN equals :: BINARI_2:def 2
('not' a₂) + (Bin1 a₁);
correctness ;

end;

:: deftheorem Def2 defines Neg2 BINARI_2:def 2 :

definition

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
func Intval c₂ -> Integer equals :Def3: :: BINARI_2:def 3
Absval a₂ if a₂ /. a₁ = FALSE
otherwise (Absval a₂) - (2 to_power a₁);
correctness ;

end;

:: deftheorem Def3 defines Intval BINARI_2:def 3 :

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func Int_add_ovfl c₂,c₃ -> Element of BOOLEAN equals :: BINARI_2:def 4
(('not' (a₂ /. a₁)) '&' ('not' (a₃ /. a₁))) '&' ((carry a₂,a₃) /. a₁);
correctness ;

end;

:: deftheorem Def4 defines Int_add_ovfl BINARI_2:def 4 :

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func Int_add_udfl c₂,c₃ -> Element of BOOLEAN equals :: BINARI_2:def 5
((a₂ /. a₁) '&' (a₃ /. a₁)) '&' ('not' ((carry a₂,a₃) /. a₁));
correctness ;

end;

:: deftheorem Def5 defines Int_add_udfl BINARI_2:def 5 :

theorem Th1: :: BINARI_2:1

canceled;

theorem Th2: :: BINARI_2:2

canceled;

theorem Th3: :: BINARI_2:3

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

proof end;

theorem Th4: :: BINARI_2:4

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

proof end;

theorem Th5: :: BINARI_2:5

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

proof end;

theorem Th6: :: BINARI_2:6

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

proof end;

theorem Th7: :: BINARI_2:7

for b₁, b₂ being Nat st b₂ in Seg b₁ & b₂ = 1 holds
(Bin1 b₁) /. b₂ = TRUE

proof end;

theorem Th8: :: BINARI_2:8

for b₁, b₂ being Nat st b₂ in Seg b₁ & b₂ <> 1 holds
(Bin1 b₁) /. b₂ = FALSE

proof end;

theorem Th9: :: BINARI_2:9

for b₁ being non empty Nat holds Bin1 (b₁ + 1) = (Bin1 b₁) ^ <*FALSE *>

proof end;

theorem Th10: :: BINARI_2:10

for b₁ being non empty Nat holds Intval ((Bin1 b₁) ^ <*FALSE *>) = 1

proof end;

theorem Th11: :: BINARI_2:11

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN
for b₃ being Element of BOOLEAN holds 'not' (b₂ ^ <*b₃*>) = ('not' b₂) ^ <*('not' b₃)*>

proof end;

theorem Th12: :: BINARI_2:12

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN
for b₃ being Element of BOOLEAN holds Intval (b₂ ^ <*b₃*>) = (Absval b₂) - (IFEQ b₃,FALSE ,0,(2 to_power b₁))

proof end;

theorem Th13: :: BINARI_2:13

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN holds ((Intval ((b₂ ^ <*b₄*>) + (b₃ ^ <*b₅*>))) + (IFEQ (Int_add_ovfl (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)),FALSE ,0,(2 to_power (b₁ + 1)))) - (IFEQ (Int_add_udfl (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)),FALSE ,0,(2 to_power (b₁ + 1))) = (Intval (b₂ ^ <*b₄*>)) + (Intval (b₃ ^ <*b₅*>))

proof end;

theorem Th14: :: BINARI_2:14

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN holds Intval ((b₂ ^ <*b₄*>) + (b₃ ^ <*b₅*>)) = (((Intval (b₂ ^ <*b₄*>)) + (Intval (b₃ ^ <*b₅*>))) - (IFEQ (Int_add_ovfl (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)),FALSE ,0,(2 to_power (b₁ + 1)))) + (IFEQ (Int_add_udfl (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)),FALSE ,0,(2 to_power (b₁ + 1)))

proof end;

theorem Th15: :: BINARI_2:15

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

proof end;

theorem Th16: :: BINARI_2:16

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN
for b₃ being Element of BOOLEAN holds Neg2 (b₂ ^ <*b₃*>) = (Neg2 b₂) ^ <*(('not' b₃) 'xor' (add_ovfl ('not' b₂),(Bin1 b₁)))*>

proof end;

theorem Th17: :: BINARI_2:17

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN
for b₃ being Element of BOOLEAN holds (Intval (Neg2 (b₂ ^ <*b₃*>))) + (IFEQ (Int_add_ovfl ('not' (b₂ ^ <*b₃*>)),(Bin1 (b₁ + 1))),FALSE ,0,(2 to_power (b₁ + 1))) = - (Intval (b₂ ^ <*b₃*>))

proof end;

theorem Th18: :: BINARI_2:18

for b₁ being non empty Nat
for b₂ being Tuple of b₁,BOOLEAN
for b₃ being Element of BOOLEAN holds Neg2 (Neg2 (b₂ ^ <*b₃*>)) = b₂ ^ <*b₃*>

proof end;

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func c₂ - c₃ -> Tuple of a₁,BOOLEAN means :Def6: :: BINARI_2:def 6
for b₁ being Nat st b₁ in Seg a₁ holds
a₄ /. b₁ = ((a₂ /. b₁) 'xor' ((Neg2 a₃) /. b₁)) 'xor' ((carry a₂,(Neg2 a₃)) /. b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - BINARI_2:def 6 :

theorem Th19: :: BINARI_2:19

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN holds b₂ - b₃ = b₂ + (Neg2 b₃)

proof end;

theorem Th20: :: BINARI_2:20

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN holds (b₂ ^ <*b₄*>) - (b₃ ^ <*b₅*>) = (b₂ + (Neg2 b₃)) ^ <*(((b₄ 'xor' ('not' b₅)) 'xor' (add_ovfl ('not' b₃),(Bin1 b₁))) 'xor' (add_ovfl b₂,(Neg2 b₃)))*>

proof end;

theorem Th21: :: BINARI_2:21

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN holds (((Intval ((b₂ ^ <*b₄*>) - (b₃ ^ <*b₅*>))) + (IFEQ (Int_add_ovfl (b₂ ^ <*b₄*>),(Neg2 (b₃ ^ <*b₅*>))),FALSE ,0,(2 to_power (b₁ + 1)))) - (IFEQ (Int_add_udfl (b₂ ^ <*b₄*>),(Neg2 (b₃ ^ <*b₅*>))),FALSE ,0,(2 to_power (b₁ + 1)))) + (IFEQ (Int_add_ovfl ('not' (b₃ ^ <*b₅*>)),(Bin1 (b₁ + 1))),FALSE ,0,(2 to_power (b₁ + 1))) = (Intval (b₂ ^ <*b₄*>)) - (Intval (b₃ ^ <*b₅*>))

proof end;