:: Binary Representation of Natural Numbers
:: by Hiroyuki Okazaki
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

theorem LM000: :: BINARI_6:1

for x being Nat ex m being Nat st x < 2 to_power m

proof end;

theorem LM001: :: BINARI_6:2

for x being Nat st x <> 0 holds
ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) )

proof end;

theorem LM002: :: BINARI_6:3

for x, n1, n2 being Nat st 2 to_power n1 <= x & x < 2 to_power (n1 + 1) & 2 to_power n2 <= x & x < 2 to_power (n2 + 1) holds
n1 = n2

proof end;

theorem LM0020: :: BINARI_6:4

<*0*> = 0* 1 by FINSEQ_2:59;

theorem :: BINARI_6:5

for n1, n2 being Nat holds (0* n1) ^ (0* n2) = 0* (n1 + n2) by FINSEQ_2:123;

definition

let x be Nat;

func LenBSeq x -> non zero Nat means :Def1: :: BINARI_6:def 1
it = 1 if x = 0
otherwise ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & it = n + 1 );

existence
( ( x = 0 implies ex b₁ being non zero Nat st b₁ = 1 ) & ( not x = 0 implies ex b₁ being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₁ = n + 1 ) ) )

proof end;

uniqueness
for b₁, b₂ being non zero Nat holds
( ( x = 0 & b₁ = 1 & b₂ = 1 implies b₁ = b₂ ) & ( not x = 0 & ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₁ = n + 1 ) & ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₂ = n + 1 ) implies b₁ = b₂ ) ) by LM002;
consistency
for b₁ being non zero Nat holds verum ;

end;

:: deftheorem Def1 defines LenBSeq BINARI_6:def 1 :
for x being Nat
for b₂ being non zero Nat holds
( ( x = 0 implies ( b₂ = LenBSeq x iff b₂ = 1 ) ) & ( not x = 0 implies ( b₂ = LenBSeq x iff ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₂ = n + 1 ) ) ) );

theorem LM006: :: BINARI_6:6

for x being Nat holds x < 2 to_power (LenBSeq x)

proof end;

theorem LM007: :: BINARI_6:7

for x being Nat holds x = Absval ((LenBSeq x) -BinarySequence x)

proof end;

theorem LM0071: :: BINARI_6:8

for n being Nat
for x being Tuple of n + 1, BOOLEAN st x . (n + 1) = 1 holds
( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) )

proof end;

theorem :: BINARI_6:9

ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & F . x = Absval x0 )

proof end;

LM020: ex F being Function of NAT,(BOOLEAN *) st
for x being Element of NAT holds F . x = (LenBSeq x) -BinarySequence x

proof end;

LM030: for F being Function of NAT,(BOOLEAN *) st ( for x being Element of NAT holds F . x = (LenBSeq x) -BinarySequence x ) holds
F is one-to-one

proof end;

definition

func Nat2BL -> Function of NAT,(BOOLEAN *) means :Def2: :: BINARI_6:def 2
for x being Element of NAT holds it . x = (LenBSeq x) -BinarySequence x;

existence
ex b₁ being Function of NAT,(BOOLEAN *) st
for x being Element of NAT holds b₁ . x = (LenBSeq x) -BinarySequence x by LM020;
uniqueness
for b₁, b₂ being Function of NAT,(BOOLEAN *) st ( for x being Element of NAT holds b₁ . x = (LenBSeq x) -BinarySequence x ) & ( for x being Element of NAT holds b₂ . x = (LenBSeq x) -BinarySequence x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Nat2BL BINARI_6:def 2 :
for b₁ being Function of NAT,(BOOLEAN *) holds
( b₁ = Nat2BL iff for x being Element of NAT holds b₁ . x = (LenBSeq x) -BinarySequence x );

theorem :: BINARI_6:10

for x being Element of NAT
for y being Tuple of LenBSeq x, BOOLEAN st Nat2BL . x = y holds
Absval y = x

proof end;

theorem LM031: :: BINARI_6:11

rng Nat2BL = { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}

proof end;

theorem :: BINARI_6:12

Nat2BL is one-to-one

proof end;

definition

let x, y be Element of BOOLEAN * ;
assume AS: ( len x <> 0 & len y <> 0 ) ;

func LenMax (x,y) -> non zero Nat equals :Def15: :: BINARI_6:def 3
max ((len x),(len y));

correctness
coherence
max ((len x),(len y)) is non zero Nat;
by XXREAL_0:16, AS;

end;

:: deftheorem Def15 defines LenMax BINARI_6:def 3 :
for x, y being Element of BOOLEAN * st len x <> 0 & len y <> 0 holds
LenMax (x,y) = max ((len x),(len y));

definition

let K be Nat;
let x be Element of BOOLEAN * ;

func ExtBit (x,K) -> Tuple of K, BOOLEAN equals :Def20: :: BINARI_6:def 4
x ^ (0* (K -' (len x))) if len x <= K
otherwise x | K;

coherence
( ( len x <= K implies x ^ (0* (K -' (len x))) is Tuple of K, BOOLEAN ) & ( not len x <= K implies x | K is Tuple of K, BOOLEAN ) )

proof end;

consistency
for b₁ being Tuple of K, BOOLEAN holds verum ;

end;

:: deftheorem Def20 defines ExtBit BINARI_6:def 4 :
for K being Nat
for x being Element of BOOLEAN * holds
( ( len x <= K implies ExtBit (x,K) = x ^ (0* (K -' (len x))) ) & ( not len x <= K implies ExtBit (x,K) = x | K ) );

theorem LMExtBit1: :: BINARI_6:13

for K being Nat
for x being Element of BOOLEAN * st len x <= K holds
ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>

proof end;

theorem LMExtBit8: :: BINARI_6:14

for K being non zero Nat
for x being Element of BOOLEAN * st len x = K holds
ExtBit (x,K) = x

proof end;

theorem LMExtBit2: :: BINARI_6:15

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
x1,y1 are_summable

proof end;

theorem LMExtBit4: :: BINARI_6:16

for K being non zero Nat
for y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
y /. n = 0

proof end;

theorem LMExtBit501: :: BINARI_6:17

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN holds carry (x,y) = carry (y,x)

proof end;

theorem LMExtBit3: :: BINARI_6:18

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 )

proof end;

theorem LMExtBit500: :: BINARI_6:19

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN holds x + y = y + x

proof end;

theorem LMExtBit5: :: BINARI_6:20

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st y = 0* K holds
( x + y = x & y + x = x )

proof end;

theorem LMExtBit9: :: BINARI_6:21

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x . (len x) = 1 & y . (len y) = 1 holds
not x,y are_summable

proof end;

LMExtBit60: for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable & x . (len x) = 1 holds
(x + y) . (len (x + y)) = 1

proof end;

theorem LMExtBit61: :: BINARI_6:22

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable holds
y,x are_summable

proof end;

theorem LMExtBit6: :: BINARI_6:23

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) holds
(x + y) . (len (x + y)) = 1

proof end;

theorem LMExtBit7: :: BINARI_6:24

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
(x1 + y1) . (len (x1 + y1)) = 1

proof end;

definition

let x, y be Element of BOOLEAN * ;

func x + y -> Element of BOOLEAN * equals :Def3: :: BINARI_6:def 5
y if len x = 0
x if len y = 0
(ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) if ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 )
otherwise (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1)));

coherence
( ( len x = 0 implies y is Element of BOOLEAN * ) & ( len y = 0 implies x is Element of BOOLEAN * ) & ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) is Element of BOOLEAN * ) & ( not len x = 0 & not len y = 0 & ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable or not len x <> 0 or not len y <> 0 ) implies (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) is Element of BOOLEAN * ) ) by FINSEQ_1:def 11;
consistency
for b₁ being Element of BOOLEAN * holds
( ( len x = 0 & len y = 0 implies ( b₁ = y iff b₁ = x ) ) & ( len x = 0 & ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies ( b₁ = y iff b₁ = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) ) & ( len y = 0 & ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies ( b₁ = x iff b₁ = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) ) ) ;

end;

:: deftheorem Def3 defines + BINARI_6:def 5 :
for x, y being Element of BOOLEAN * holds
( ( len x = 0 implies x + y = y ) & ( len y = 0 implies x + y = x ) & ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) & ( not len x = 0 & not len y = 0 & ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable or not len x <> 0 or not len y <> 0 ) implies x + y = (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) ) );

definition

let F be Function of NAT,(BOOLEAN *);
let x be Element of NAT ;
:: original: .
redefine func F . x -> Element of BOOLEAN * ;
correctness
coherence
F . x is Element of BOOLEAN * ;
by FUNCT_2:5;

end;

theorem LM0710: :: BINARI_6:25

for x being Element of BOOLEAN * st x in rng Nat2BL holds
1 <= len x

proof end;

theorem LM071: :: BINARI_6:26

for x, y being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL holds
x + y in rng Nat2BL

proof end;

theorem LM080: :: BINARI_6:27

for n being non zero Nat
for x being Tuple of n, BOOLEAN
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x

proof end;

theorem LM090: :: BINARI_6:28

for n being Nat
for x being Element of NAT
for y being Tuple of n, BOOLEAN st y = Nat2BL . x holds
( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )

proof end;

theorem LM100: :: BINARI_6:29

for x, y being Element of NAT holds Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)

proof end;

theorem :: BINARI_6:30

for x, y being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL holds
x + y = y + x

proof end;

theorem :: BINARI_6:31

for x, y, z being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL & z in rng Nat2BL holds
(x + y) + z = x + (y + z)

proof end;

definition

let x be Element of BOOLEAN * ;

func ExAbsval x -> Nat means :Def100: :: BINARI_6:def 6
ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & it = Absval y );

existence
ex b₁, n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b₁ = Absval y )

proof end;

uniqueness
for b₁, b₂ being Nat st ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b₁ = Absval y ) & ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b₂ = Absval y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def100 defines ExAbsval BINARI_6:def 6 :
for x being Element of BOOLEAN *
for b₂ being Nat holds
( b₂ = ExAbsval x iff ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b₂ = Absval y ) );

D100: for x being Element of BOOLEAN * st len x = 0 holds
ExAbsval x = 0

proof end;

theorem LM210: :: BINARI_6:32

ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * holds F . x = ExAbsval x

proof end;

definition

func BL2Nat -> Function of (BOOLEAN *),NAT means :Def110: :: BINARI_6:def 7
for x being Element of BOOLEAN * holds it . x = ExAbsval x;

existence
ex b₁ being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * holds b₁ . x = ExAbsval x by LM210;
uniqueness
for b₁, b₂ being Function of (BOOLEAN *),NAT st ( for x being Element of BOOLEAN * holds b₁ . x = ExAbsval x ) & ( for x being Element of BOOLEAN * holds b₂ . x = ExAbsval x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def110 defines BL2Nat BINARI_6:def 7 :
for b₁ being Function of (BOOLEAN *),NAT holds
( b₁ = BL2Nat iff for x being Element of BOOLEAN * holds b₁ . x = ExAbsval x );

definition

let F be Function of (BOOLEAN *),NAT;
let x be Element of BOOLEAN * ;
:: original: .
redefine func F . x -> Element of NAT ;
correctness
coherence
F . x is Element of NAT ;
by FUNCT_2:5;

end;

LM220: for F being Function of (BOOLEAN *),NAT st ( for x being Element of BOOLEAN * holds F . x = ExAbsval x ) holds
F is onto

proof end;

registration

cluster BL2Nat -> onto ;

coherence
BL2Nat is onto

proof end;

end;

theorem LM230: :: BINARI_6:33

for x being Element of BOOLEAN *
for K being Nat st len x <> 0 & len x <= K holds
ExAbsval x = Absval (ExtBit (x,K))

proof end;

theorem LM240: :: BINARI_6:34

for x, y being Element of BOOLEAN * holds BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)

proof end;

definition

func EqBL2Nat -> Equivalence_Relation of (BOOLEAN *) means :Def300: :: BINARI_6:def 8
for x, y being object holds
( [x,y] in it iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) );

existence
ex b₁ being Equivalence_Relation of (BOOLEAN *) st
for x, y being object holds
( [x,y] in b₁ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of (BOOLEAN *) st ( for x, y being object holds
( [x,y] in b₁ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def300 defines EqBL2Nat BINARI_6:def 8 :
for b₁ being Equivalence_Relation of (BOOLEAN *) holds
( b₁ = EqBL2Nat iff for x, y being object holds
( [x,y] in b₁ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) );

definition

func QuBL2Nat -> Function of (Class EqBL2Nat),NAT means :Def400: :: BINARI_6:def 9
for A being Element of Class EqBL2Nat ex x being object st
( x in A & it . A = BL2Nat . x );

existence
ex b₁ being Function of (Class EqBL2Nat),NAT st
for A being Element of Class EqBL2Nat ex x being object st
( x in A & b₁ . A = BL2Nat . x )

proof end;

uniqueness
for b₁, b₂ being Function of (Class EqBL2Nat),NAT st ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & b₁ . A = BL2Nat . x ) ) & ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & b₂ . A = BL2Nat . x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def400 defines QuBL2Nat BINARI_6:def 9 :
for b₁ being Function of (Class EqBL2Nat),NAT holds
( b₁ = QuBL2Nat iff for A being Element of Class EqBL2Nat ex x being object st
( x in A & b₁ . A = BL2Nat . x ) );

LemmaQU: QuBL2Nat is onto

proof end;

LM600: QuBL2Nat is one-to-one

proof end;

registration

cluster QuBL2Nat -> one-to-one onto ;

coherence
( QuBL2Nat is one-to-one & QuBL2Nat is onto ) by LemmaQU, LM600;

end;

theorem LM700: :: BINARI_6:35

for x being Element of BOOLEAN * holds QuBL2Nat . (Class (EqBL2Nat,x)) = BL2Nat . x

proof end;

definition

let A, B be Element of Class EqBL2Nat;

func A + B -> Element of Class EqBL2Nat means :Def500: :: BINARI_6:def 10
ex x, y being Element of BOOLEAN * st
( x in A & y in B & it = Class (EqBL2Nat,(x + y)) );

existence
ex b₁ being Element of Class EqBL2Nat ex x, y being Element of BOOLEAN * st
( x in A & y in B & b₁ = Class (EqBL2Nat,(x + y)) )

proof end;

uniqueness
for b₁, b₂ being Element of Class EqBL2Nat st ex x, y being Element of BOOLEAN * st
( x in A & y in B & b₁ = Class (EqBL2Nat,(x + y)) ) & ex x, y being Element of BOOLEAN * st
( x in A & y in B & b₂ = Class (EqBL2Nat,(x + y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def500 defines + BINARI_6:def 10 :
for A, B, b₃ being Element of Class EqBL2Nat holds
( b₃ = A + B iff ex x, y being Element of BOOLEAN * st
( x in A & y in B & b₃ = Class (EqBL2Nat,(x + y)) ) );

theorem LM800: :: BINARI_6:36

for A, B being Element of Class EqBL2Nat
for x, y being Element of BOOLEAN * st x in A & y in B holds
A + B = Class (EqBL2Nat,(x + y))

proof end;

theorem :: BINARI_6:37

for A, B being Element of Class EqBL2Nat holds QuBL2Nat . (A + B) = (QuBL2Nat . A) + (QuBL2Nat . B)

proof end;

theorem LM910: :: BINARI_6:38

for A, B being Element of Class EqBL2Nat holds A + B = B + A

proof end;

theorem :: BINARI_6:39

for A, B, C being Element of Class EqBL2Nat holds (A + B) + C = A + (B + C)

proof end;

theorem LM930: :: BINARI_6:40

for n being Nat
for z, z1 being Element of BOOLEAN * st z = <*> BOOLEAN & z1 = 0* n holds
Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)

proof end;

theorem :: BINARI_6:41

for A, Z being Element of Class EqBL2Nat
for n being Nat
for z being Element of BOOLEAN * st Z = Class (EqBL2Nat,z) & z = 0* n holds
( A + Z = A & Z + A = A )

proof end;