:: BINARITH semantic presentation

definition

let i be Nat;
let D be non empty set ;
mode Tuple of i,D is Element of i -tuples_on D;

end;

Lm1: for i, j being Nat holds addnat . i,j = i + j
by BINOP_2:def 23;

theorem :: BINARITH:1

canceled;

theorem Th2: :: BINARITH:2

for i, n being Nat
for D being non empty set
for d being Element of D
for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i

proof end;

theorem Th3: :: BINARITH:3

for n being Nat
for D being non empty set
for d being Element of D
for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

proof end;

theorem :: BINARITH:4

canceled;

theorem :: BINARITH:5

for i, n being Nat st i in Seg n holds
not i is empty by CARD_1:51, FINSEQ_1:3;

definition

let x, y be boolean set ;
func x 'or' y -> set equals :: BINARITH:def 1
'not' (('not' x) '&' ('not' y));
correctness ;
commutativity ;

end;

:: deftheorem defines 'or' BINARITH:def 1 :

definition

let x, y be boolean set ;
func x 'xor' y -> set equals :: BINARITH:def 2
(('not' x) '&' y) 'or' (x '&' ('not' y));
correctness ;
commutativity ;

end;

:: deftheorem defines 'xor' BINARITH:def 2 :

registration

let x, y be boolean set ;
cluster x 'or' y -> boolean ;
correctness ;

end;

registration

let x, y be boolean set ;
cluster x 'xor' y -> boolean ;
correctness ;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'or'
redefine func x 'or' y -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;
:: original: 'xor'
redefine func x 'xor' y -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

theorem :: BINARITH:6

canceled;

theorem Th7: :: BINARITH:7

for x being boolean set holds x 'or' FALSE = x

proof end;

theorem :: BINARITH:8

canceled;

theorem Th9: :: BINARITH:9

for x, y being boolean set holds 'not' (x '&' y) = ('not' x) 'or' ('not' y)

proof end;

theorem Th10: :: BINARITH:10

for x, y being boolean set holds 'not' (x 'or' y) = ('not' x) '&' ('not' y) by MARGREL1:40;

theorem :: BINARITH:11

canceled;

theorem :: BINARITH:12

for x, y being boolean set holds x '&' y = 'not' (('not' x) 'or' ('not' y))

proof end;

theorem :: BINARITH:13

for x being boolean set holds TRUE 'xor' x = 'not' x

proof end;

theorem :: BINARITH:14

for x being boolean set holds FALSE 'xor' x = x

proof end;

theorem Th15: :: BINARITH:15

for x being boolean set holds x 'xor' x = FALSE

proof end;

theorem Th16: :: BINARITH:16

for x being boolean set holds x '&' x = x

proof end;

theorem Th17: :: BINARITH:17

for x being boolean set holds x 'xor' ('not' x) = TRUE

proof end;

theorem Th18: :: BINARITH:18

for x being boolean set holds x 'or' ('not' x) = TRUE by MARGREL1:47;

theorem Th19: :: BINARITH:19

for x being boolean set holds x 'or' TRUE = TRUE

proof end;

theorem Th20: :: BINARITH:20

for x, y, z being boolean set holds (x 'or' y) 'or' z = x 'or' (y 'or' z)

proof end;

theorem Th21: :: BINARITH:21

for x being boolean set holds x 'or' x = x

proof end;

theorem Th22: :: BINARITH:22

for x, y, z being boolean set holds x '&' (y 'or' z) = (x '&' y) 'or' (x '&' z)

proof end;

theorem Th23: :: BINARITH:23

for x, y, z being boolean set holds x 'or' (y '&' z) = (x 'or' y) '&' (x 'or' z)

proof end;

theorem :: BINARITH:24

for x, y being boolean set holds x 'or' (x '&' y) = x

proof end;

theorem Th25: :: BINARITH:25

for x, y being boolean set holds x '&' (x 'or' y) = x

proof end;

theorem Th26: :: BINARITH:26

for x, y being boolean set holds x 'or' (('not' x) '&' y) = x 'or' y

proof end;

theorem :: BINARITH:27

for x, y being boolean set holds x '&' (('not' x) 'or' y) = x '&' y

proof end;

theorem :: BINARITH:28

canceled;

theorem :: BINARITH:29

canceled;

theorem :: BINARITH:30

canceled;

theorem :: BINARITH:31

canceled;

theorem :: BINARITH:32

canceled;

theorem Th33: :: BINARITH:33

TRUE 'xor' FALSE = TRUE

proof end;

theorem Th34: :: BINARITH:34

for x, y, z being boolean set holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)

proof end;

theorem :: BINARITH:35

for x, y being boolean set holds x 'xor' (('not' x) '&' y) = x 'or' y

proof end;

theorem :: BINARITH:36

for x, y being boolean set holds x 'or' (x 'xor' y) = x 'or' y

proof end;

theorem :: BINARITH:37

for x, y being boolean set holds x 'or' (('not' x) 'xor' y) = x 'or' ('not' y)

proof end;

theorem :: BINARITH:38

for x, y, z being boolean set holds x '&' (y 'xor' z) = (x '&' y) 'xor' (x '&' z)

proof end;

definition

let i, j be natural number ;
func i -' j -> Nat equals :Def3: :: BINARITH:def 3
i - j if i - j >= 0
otherwise 0;
coherence by INT_1:16;
correctness ;

end;

:: deftheorem Def3 defines -' BINARITH:def 3 :

theorem Th39: :: BINARITH:39

for i, j being natural number holds (i + j) -' j = i

proof end;

definition

let n be Nat;
let x be Tuple of n,BOOLEAN ;
func 'not' x -> Tuple of n,BOOLEAN means :: BINARITH:def 4
for i being Nat st i in Seg n holds
it /. i = 'not' (x /. i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines 'not' BINARITH:def 4 :

definition

let n be non empty Nat;
let x, y be Tuple of n,BOOLEAN ;
func carry x,y -> Tuple of n,BOOLEAN means :Def5: :: BINARITH:def 5
( it /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
it /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (it /. i))) 'or' ((y /. i) '&' (it /. i)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines carry BINARITH:def 5 :

definition

let n be Nat;
let x be Tuple of n,BOOLEAN ;
func Binary x -> Tuple of n,NAT means :Def6: :: BINARITH:def 6
for i being Nat st i in Seg n holds
it /. i = IFEQ (x /. i),FALSE ,0,(2 to_power (i -' 1));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Binary BINARITH:def 6 :

definition

let n be Nat;
let x be Tuple of n,BOOLEAN ;
func Absval x -> Nat equals :: BINARITH:def 7
addnat $$ (Binary x);
correctness ;

end;

:: deftheorem defines Absval BINARITH:def 7 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines + BINARITH:def 8 :

definition

let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
func add_ovfl z1,z2 -> Element of BOOLEAN equals :: BINARITH:def 9
(((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry z1,z2) /. n))) 'or' ((z2 /. n) '&' ((carry z1,z2) /. n));
correctness ;

end;

:: deftheorem defines add_ovfl BINARITH:def 9 :

scheme :: BINARITH:sch 1
Indfrom1{ P₁[ Nat] } :

for k being non empty Nat holds P₁[k]

provided

A1: P₁[1] and
A2: for k being non empty Nat st P₁[k] holds
P₁[k + 1]

proof end;

definition

let n be non empty Nat;
let z1, z2 be Tuple of n,BOOLEAN ;
pred z1,z2 are_summable means :Def10: :: BINARITH:def 10
add_ovfl z1,z2 = FALSE ;

end;

:: deftheorem Def10 defines are_summable BINARITH:def 10 :

theorem Th40: :: BINARITH:40

for z1 being Tuple of 1,BOOLEAN holds
( z1 = <*FALSE *> or z1 = <*TRUE *> )

proof end;

theorem Th41: :: BINARITH:41

for z1 being Tuple of 1,BOOLEAN st z1 = <*FALSE *> holds
Absval z1 = 0

proof end;

theorem Th42: :: BINARITH:42

for z1 being Tuple of 1,BOOLEAN st z1 = <*TRUE *> holds
Absval z1 = 1

proof end;

definition

let n1 be non empty Nat;
let n2 be Nat;
let D be non empty set ;
let z1 be Tuple of n1,D;
let z2 be Tuple of n2,D;
:: original: ^
redefine func z1 ^ z2 -> Tuple of (n1 + n2),D;
coherence by FINSEQ_2:127;

end;

definition

let D be non empty set ;
let d be Element of D;
:: original: <*
redefine func <*d*> -> Tuple of 1,D;
coherence by FINSEQ_2:118;

end;

theorem Th43: :: BINARITH:43

for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN
for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. i = (carry z1,z2) /. i

proof end;

theorem Th44: :: BINARITH:44

for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN
for d1, d2 being Element of BOOLEAN holds add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)

proof end;

theorem Th45: :: BINARITH:45

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

proof end;

theorem Th46: :: BINARITH:46

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

proof end;

theorem Th47: :: BINARITH:47

for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN holds (Absval (z1 + z2)) + (IFEQ (add_ovfl z1,z2),FALSE ,0,(2 to_power n)) = (Absval z1) + (Absval z2)

proof end;

theorem :: BINARITH:48

for n being non empty Nat
for z1, z2 being Tuple of n,BOOLEAN st z1,z2 are_summable holds
Absval (z1 + z2) = (Absval z1) + (Absval z2)

proof end;

theorem :: BINARITH:49

for c, a, b being natural number st c <= a & c <= b & a -' c = b -' c holds
a = b

proof end;

theorem :: BINARITH:50

for b, a being natural number st b <= a holds
a -' b = a - b

proof end;

theorem :: BINARITH:51

for a being natural number holds a -' a = 0

proof end;

theorem :: BINARITH:52

for a, b being natural number holds a -' b <= a

proof end;

theorem :: BINARITH:53

for i, j being natural number st i >= j holds
(i -' j) + j = i

proof end;