:: BINARITH semantic presentation

definition

let c₁ be Nat;
let c₂ be non empty set ;
mode Tuple of a₁,a₂ is Element of a₁ -tuples_on a₂;

end;

Lemma1: for b₁, b₂ being Nat holds addnat . b₁,b₂ = b₁ + b₂
by BINOP_2:def 23;

theorem Th1: :: BINARITH:1

canceled;

theorem Th2: :: BINARITH:2

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being Tuple of b₂,b₃ st b₁ in Seg b₂ holds
(b₅ ^ <*b₄*>) /. b₁ = b₅ /. b₁

proof end;

theorem Th3: :: BINARITH:3

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being Tuple of b₁,b₂ holds (b₄ ^ <*b₃*>) /. (b₁ + 1) = b₃

proof end;

theorem Th4: :: BINARITH:4

canceled;

theorem Th5: :: BINARITH:5

for b₁, b₂ being Nat st b₁ in Seg b₂ holds
not b₁ is empty by CARD_1:51, FINSEQ_1:3;

definition

let c₁, c₂ be boolean set ;
func c₁ 'or' c₂ -> set equals :: BINARITH:def 1
'not' (('not' a₁) '&' ('not' a₂));
correctness ;
commutativity ;

end;

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

definition

let c₁, c₂ be boolean set ;
func c₁ 'xor' c₂ -> set equals :: BINARITH:def 2
(('not' a₁) '&' a₂) 'or' (a₁ '&' ('not' a₂));
correctness ;
commutativity ;

end;

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

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'or' a₂ -> boolean ;
correctness ;

end;

registration

let c₁, c₂ be boolean set ;
cluster a₁ 'xor' a₂ -> boolean ;
correctness ;

end;

definition

let c₁, c₂ be Element of BOOLEAN ;
redefine func 'or' as c₁ 'or' c₂ -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;
redefine func 'xor' as c₁ 'xor' c₂ -> Element of BOOLEAN ;
correctness by MARGREL1:def 15;

end;

theorem Th6: :: BINARITH:6

canceled;

theorem Th7: :: BINARITH:7

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

proof end;

theorem Th8: :: BINARITH:8

canceled;

theorem Th9: :: BINARITH:9

for b₁, b₂ being boolean set holds 'not' (b₁ '&' b₂) = ('not' b₁) 'or' ('not' b₂)

proof end;

theorem Th10: :: BINARITH:10

for b₁, b₂ being boolean set holds 'not' (b₁ 'or' b₂) = ('not' b₁) '&' ('not' b₂) by MARGREL1:40;

theorem Th11: :: BINARITH:11

canceled;

theorem Th12: :: BINARITH:12

for b₁, b₂ being boolean set holds b₁ '&' b₂ = 'not' (('not' b₁) 'or' ('not' b₂))

proof end;

theorem Th13: :: BINARITH:13

for b₁ being boolean set holds TRUE 'xor' b₁ = 'not' b₁

proof end;

theorem Th14: :: BINARITH:14

for b₁ being boolean set holds FALSE 'xor' b₁ = b₁

proof end;

theorem Th15: :: BINARITH:15

for b₁ being boolean set holds b₁ 'xor' b₁ = FALSE

proof end;

theorem Th16: :: BINARITH:16

for b₁ being boolean set holds b₁ '&' b₁ = b₁

proof end;

theorem Th17: :: BINARITH:17

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

proof end;

theorem Th18: :: BINARITH:18

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

theorem Th19: :: BINARITH:19

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

proof end;

theorem Th20: :: BINARITH:20

for b₁, b₂, b₃ being boolean set holds (b₁ 'or' b₂) 'or' b₃ = b₁ 'or' (b₂ 'or' b₃)

proof end;

theorem Th21: :: BINARITH:21

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

proof end;

theorem Th22: :: BINARITH:22

for b₁, b₂, b₃ being boolean set holds b₁ '&' (b₂ 'or' b₃) = (b₁ '&' b₂) 'or' (b₁ '&' b₃)

proof end;

theorem Th23: :: BINARITH:23

for b₁, b₂, b₃ being boolean set holds b₁ 'or' (b₂ '&' b₃) = (b₁ 'or' b₂) '&' (b₁ 'or' b₃)

proof end;

theorem Th24: :: BINARITH:24

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ '&' b₂) = b₁

proof end;

theorem Th25: :: BINARITH:25

for b₁, b₂ being boolean set holds b₁ '&' (b₁ 'or' b₂) = b₁

proof end;

theorem Th26: :: BINARITH:26

for b₁, b₂ being boolean set holds b₁ 'or' (('not' b₁) '&' b₂) = b₁ 'or' b₂

proof end;

theorem Th27: :: BINARITH:27

for b₁, b₂ being boolean set holds b₁ '&' (('not' b₁) 'or' b₂) = b₁ '&' b₂

proof end;

theorem Th28: :: BINARITH:28

canceled;

theorem Th29: :: BINARITH:29

canceled;

theorem Th30: :: BINARITH:30

canceled;

theorem Th31: :: BINARITH:31

canceled;

theorem Th32: :: BINARITH:32

canceled;

theorem Th33: :: BINARITH:33

TRUE 'xor' FALSE = TRUE

proof end;

theorem Th34: :: BINARITH:34

for b₁, b₂, b₃ being boolean set holds (b₁ 'xor' b₂) 'xor' b₃ = b₁ 'xor' (b₂ 'xor' b₃)

proof end;

theorem Th35: :: BINARITH:35

for b₁, b₂ being boolean set holds b₁ 'xor' (('not' b₁) '&' b₂) = b₁ 'or' b₂

proof end;

theorem Th36: :: BINARITH:36

for b₁, b₂ being boolean set holds b₁ 'or' (b₁ 'xor' b₂) = b₁ 'or' b₂

proof end;

theorem Th37: :: BINARITH:37

for b₁, b₂ being boolean set holds b₁ 'or' (('not' b₁) 'xor' b₂) = b₁ 'or' ('not' b₂)

proof end;

theorem Th38: :: BINARITH:38

for b₁, b₂, b₃ being boolean set holds b₁ '&' (b₂ 'xor' b₃) = (b₁ '&' b₂) 'xor' (b₁ '&' b₃)

proof end;

definition

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

end;

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

theorem Th39: :: BINARITH:39

for b₁, b₂ being natural number holds (b₁ + b₂) -' b₂ = b₁

proof end;

definition

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
func 'not' c₂ -> Tuple of a₁,BOOLEAN means :: BINARITH:def 4
for b₁ being Nat st b₁ in Seg a₁ holds
a₃ /. b₁ = 'not' (a₂ /. b₁);
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func carry c₂,c₃ -> Tuple of a₁,BOOLEAN means :Def5: :: BINARITH:def 5
( a₄ /. 1 = FALSE & ( for b₁ being Nat st 1 <= b₁ & b₁ < a₁ holds
a₄ /. (b₁ + 1) = (((a₂ /. b₁) '&' (a₃ /. b₁)) 'or' ((a₂ /. b₁) '&' (a₄ /. b₁))) 'or' ((a₃ /. b₁) '&' (a₄ /. b₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines carry BINARITH:def 5 :

definition

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
func Binary c₂ -> Tuple of a₁,NAT means :Def6: :: BINARITH:def 6
for b₁ being Nat st b₁ in Seg a₁ holds
a₃ /. b₁ = IFEQ (a₂ /. b₁),FALSE ,0,(2 to_power (b₁ -' 1));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Binary BINARITH:def 6 :

definition

let c₁ be Nat;
let c₂ be Tuple of c₁,BOOLEAN ;
func Absval c₂ -> Nat equals :: BINARITH:def 7
addnat $$ (Binary a₂);
correctness ;

end;

:: deftheorem Def7 defines Absval BINARITH:def 7 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines + BINARITH:def 8 :

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func add_ovfl c₂,c₃ -> Element of BOOLEAN equals :: BINARITH:def 9
(((a₂ /. a₁) '&' (a₃ /. a₁)) 'or' ((a₂ /. a₁) '&' ((carry a₂,a₃) /. a₁))) 'or' ((a₃ /. a₁) '&' ((carry a₂,a₃) /. a₁));
correctness ;

end;

:: deftheorem Def9 defines add_ovfl BINARITH:def 9 :

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

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

provided

E25: P₁[1] and
E26: for b₁ being non empty Nat st P₁[b₁] holds
P₁[b₁ + 1]

proof end;

definition

let c₁ be non empty Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
pred c₂,c₃ are_summable means :Def10: :: BINARITH:def 10
add_ovfl a₂,a₃ = FALSE ;

end;

:: deftheorem Def10 defines are_summable BINARITH:def 10 :

theorem Th40: :: BINARITH:40

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

proof end;

theorem Th41: :: BINARITH:41

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

proof end;

theorem Th42: :: BINARITH:42

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

proof end;

definition

let c₁ be non empty Nat;
let c₂ be Nat;
let c₃ be non empty set ;
let c₄ be Tuple of c₁,c₃;
let c₅ be Tuple of c₂,c₃;
redefine func ^ as c₄ ^ c₅ -> Tuple of (a₁ + a₂),a₃;
coherence by FINSEQ_2:127;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func <* as <*c₂*> -> Tuple of 1,a₁;
coherence by FINSEQ_2:118;

end;

theorem Th43: :: BINARITH:43

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN
for b₆ being Nat st b₆ in Seg b₁ holds
(carry (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)) /. b₆ = (carry b₂,b₃) /. b₆

proof end;

theorem Th44: :: BINARITH:44

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN
for b₄, b₅ being Element of BOOLEAN holds add_ovfl b₂,b₃ = (carry (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>)) /. (b₁ + 1)

proof end;

theorem Th45: :: BINARITH:45

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₂ + b₃) ^ <*((b₄ 'xor' b₅) 'xor' (add_ovfl b₂,b₃))*>

proof end;

theorem Th46: :: BINARITH:46

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

proof end;

theorem Th47: :: BINARITH:47

for b₁ being non empty Nat
for b₂, b₃ being Tuple of b₁,BOOLEAN holds (Absval (b₂ + b₃)) + (IFEQ (add_ovfl b₂,b₃),FALSE ,0,(2 to_power b₁)) = (Absval b₂) + (Absval b₃)

proof end;

theorem Th48: :: BINARITH:48

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

proof end;

theorem Th49: :: BINARITH:49

for b₁, b₂, b₃ being natural number st b₁ <= b₂ & b₁ <= b₃ & b₂ -' b₁ = b₃ -' b₁ holds
b₂ = b₃

proof end;

theorem Th50: :: BINARITH:50

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

proof end;

theorem Th51: :: BINARITH:51

for b₁ being natural number holds b₁ -' b₁ = 0

proof end;

theorem Th52: :: BINARITH:52

for b₁, b₂ being natural number holds b₁ -' b₂ <= b₁

proof end;

theorem Th53: :: BINARITH:53

for b₁, b₂ being natural number st b₁ >= b₂ holds
(b₁ -' b₂) + b₂ = b₁

proof end;