:: BINARI_2 semantic presentation

definition

let X be non empty set ;
let D be non empty Subset of X;
let x, y be set ;
let a, b be Element of D;
:: original: IFEQ
redefine func IFEQ x,y,a,b -> Element of D;
coherence

proof end;

end;

Lm1: for n being Nat
for p, q being Tuple of n,BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q

proof end;

definition

let n be Nat;
func Bin1 n -> Tuple of n,BOOLEAN means :Def1: :: BINARI_2:def 1
for i being Nat st i in Seg n holds
it /. i = IFEQ i,1,TRUE ,FALSE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :

definition

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

end;

:: deftheorem defines Neg2 BINARI_2:def 2 :

definition

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

end;

:: deftheorem Def3 defines Intval BINARI_2:def 3 :

definition

let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
func Int_add_ovfl z1,z2 -> Element of BOOLEAN equals :: BINARI_2:def 4
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry z1,z2) /. n);
correctness ;

end;

:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :

definition

let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
func Int_add_udfl z1,z2 -> Element of BOOLEAN equals :: BINARI_2:def 5
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry z1,z2) /. n));
correctness ;

end;

:: deftheorem defines Int_add_udfl BINARI_2:def 5 :

theorem :: BINARI_2:1

canceled;

theorem :: BINARI_2:2

canceled;

theorem :: BINARI_2:3

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

proof end;

theorem Th4: :: BINARI_2:4

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

proof end;

theorem :: BINARI_2:5

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

proof end;

theorem :: BINARI_2:6

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

proof end;

theorem Th7: :: BINARI_2:7

for n, i being Nat st i in Seg n & i = 1 holds
(Bin1 n) /. i = TRUE

proof end;

theorem Th8: :: BINARI_2:8

for n, i being Nat st i in Seg n & i <> 1 holds
(Bin1 n) /. i = FALSE

proof end;

theorem Th9: :: BINARI_2:9

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

proof end;

theorem Th10: :: BINARI_2:10

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

proof end;

theorem Th11: :: BINARI_2:11

for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>

proof end;

theorem Th12: :: BINARI_2:12

for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = (Absval z) - (IFEQ d,FALSE ,0,(2 to_power m))

proof end;

theorem Th13: :: BINARI_2:13

for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))

proof end;

theorem Th14: :: BINARI_2:14

for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))) + (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(z2 ^ <*d2*>)),FALSE ,0,(2 to_power (m + 1)))

proof end;

theorem Th15: :: BINARI_2:15

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

proof end;

theorem Th16: :: BINARI_2:16

for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*>

proof end;

theorem Th17: :: BINARI_2:17

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

proof end;

theorem :: BINARI_2:18

for m being non empty Nat
for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>

proof end;

definition

let n be non empty Nat;
let x, y be Tuple of n,BOOLEAN ;
func x - y -> Tuple of n,BOOLEAN means :Def6: :: BINARI_2:def 6
for i being Nat st i in Seg n holds
it /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - BINARI_2:def 6 :

theorem Th19: :: BINARI_2:19

for m being non empty Nat
for x, y being Tuple of m,BOOLEAN holds x - y = x + (Neg2 y)

proof end;

theorem :: BINARI_2:20

for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl ('not' z2),(Bin1 m))) 'xor' (add_ovfl z1,(Neg2 z2)))*>

proof end;

theorem :: BINARI_2:21

for m being non empty Nat
for z1, z2 being Tuple of m,BOOLEAN
for d1, d2 being Element of BOOLEAN holds (((Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + (IFEQ (Int_add_ovfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0,(2 to_power (m + 1)))) - (IFEQ (Int_add_udfl (z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>))),FALSE ,0,(2 to_power (m + 1)))) + (IFEQ (Int_add_ovfl ('not' (z2 ^ <*d2*>)),(Bin1 (m + 1))),FALSE ,0,(2 to_power (m + 1))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))

proof end;