:: by Hiroyuki Okazaki

::

:: Received September 29, 2018

:: Copyright (c) 2018-2021 Association of Mizar Users

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

n1 = n2

proof end;

definition

let x be Nat;

( ( x = 0 implies ex b_{1} being non zero Nat st b_{1} = 1 ) & ( not x = 0 implies ex b_{1} being non zero Nat ex n being Nat st

( 2 to_power n <= x & x < 2 to_power (n + 1) & b_{1} = n + 1 ) ) )

for b_{1}, b_{2} being non zero Nat holds

( ( x = 0 & b_{1} = 1 & b_{2} = 1 implies b_{1} = b_{2} ) & ( not x = 0 & ex n being Nat st

( 2 to_power n <= x & x < 2 to_power (n + 1) & b_{1} = n + 1 ) & ex n being Nat st

( 2 to_power n <= x & x < 2 to_power (n + 1) & b_{2} = n + 1 ) implies b_{1} = b_{2} ) )
by LM002;

consistency

for b_{1} being non zero Nat holds verum
;

end;
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 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 );

( ( x = 0 implies ex b

( 2 to_power n <= x & x < 2 to_power (n + 1) & b

proof end;

uniqueness for b

( ( x = 0 & b

( 2 to_power n <= x & x < 2 to_power (n + 1) & b

( 2 to_power n <= x & x < 2 to_power (n + 1) & b

consistency

for b

:: deftheorem Def1 defines LenBSeq BINARI_6:def 1 :

for x being Nat

for b_{2} being non zero Nat holds

( ( x = 0 implies ( b_{2} = LenBSeq x iff b_{2} = 1 ) ) & ( not x = 0 implies ( b_{2} = LenBSeq x iff ex n being Nat st

( 2 to_power n <= x & x < 2 to_power (n + 1) & b_{2} = n + 1 ) ) ) );

for x being Nat

for b

( ( x = 0 implies ( b

( 2 to_power n <= x & x < 2 to_power (n + 1) & b

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) )

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 )

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

ex b_{1} being Function of NAT,(BOOLEAN *) st

for x being Element of NAT holds b_{1} . x = (LenBSeq x) -BinarySequence x
by LM020;

uniqueness

for b_{1}, b_{2} being Function of NAT,(BOOLEAN *) st ( for x being Element of NAT holds b_{1} . x = (LenBSeq x) -BinarySequence x ) & ( for x being Element of NAT holds b_{2} . x = (LenBSeq x) -BinarySequence x ) holds

b_{1} = b_{2}
end;

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 for x being Element of NAT holds it . x = (LenBSeq x) -BinarySequence x;

ex b

for x being Element of NAT holds b

uniqueness

for b

b

proof end;

:: deftheorem Def2 defines Nat2BL BINARI_6:def 2 :

for b_{1} being Function of NAT,(BOOLEAN *) holds

( b_{1} = Nat2BL iff for x being Element of NAT holds b_{1} . x = (LenBSeq x) -BinarySequence x );

for b

( b

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

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

Absval y = x

proof end;

definition

let x, y be Element of BOOLEAN * ;

assume AS: ( len x <> 0 & len y <> 0 ) ;

correctness

coherence

max ((len x),(len y)) is non zero Nat;

by XXREAL_0:16, AS;

end;
assume AS: ( len x <> 0 & len y <> 0 ) ;

correctness

coherence

max ((len x),(len y)) is non zero Nat;

by XXREAL_0:16, AS;

:: 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));

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 * ;

( ( 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 ) )

for b_{1} being Tuple of K, BOOLEAN holds verum
;

end;
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 x ^ (0* (K -' (len x))) if len x <= K

otherwise x | K;

( ( 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

:: 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 ) );

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*>

for x being Element of BOOLEAN * st len x <= K holds

ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>

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

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

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 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 )

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 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 )

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

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

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

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

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 * ;

( ( 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_{1} being Element of BOOLEAN * holds

( ( len x = 0 & len y = 0 implies ( b_{1} = y iff b_{1} = x ) ) & ( len x = 0 & ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies ( b_{1} = y iff b_{1} = (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_{1} = x iff b_{1} = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) ) )
;

end;
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 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)));

( ( 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

( ( len x = 0 & len y = 0 implies ( b

:: 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))) ) );

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;
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;

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

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 )

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 :: 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)

(x + y) + z = x + (y + z)

proof end;

definition

let x be Element of BOOLEAN * ;

ex b_{1}, n being Nat ex y being Tuple of n, BOOLEAN st

( y = x & b_{1} = Absval y )

for b_{1}, b_{2} being Nat st ex n being Nat ex y being Tuple of n, BOOLEAN st

( y = x & b_{1} = Absval y ) & ex n being Nat ex y being Tuple of n, BOOLEAN st

( y = x & b_{2} = Absval y ) holds

b_{1} = b_{2}

end;
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 n being Nat ex y being Tuple of n, BOOLEAN st

( y = x & it = Absval y );

ex b

( y = x & b

proof end;

uniqueness for b

( y = x & b

( y = x & b

b

proof end;

:: deftheorem Def100 defines ExAbsval BINARI_6:def 6 :

for x being Element of BOOLEAN *

for b_{2} being Nat holds

( b_{2} = ExAbsval x iff ex n being Nat ex y being Tuple of n, BOOLEAN st

( y = x & b_{2} = Absval y ) );

for x being Element of BOOLEAN *

for b

( b

( y = x & b

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

ExAbsval x = 0

proof end;

definition

ex b_{1} being Function of (BOOLEAN *),NAT st

for x being Element of BOOLEAN * holds b_{1} . x = ExAbsval x
by LM210;

uniqueness

for b_{1}, b_{2} being Function of (BOOLEAN *),NAT st ( for x being Element of BOOLEAN * holds b_{1} . x = ExAbsval x ) & ( for x being Element of BOOLEAN * holds b_{2} . x = ExAbsval x ) holds

b_{1} = b_{2}
end;

func BL2Nat -> Function of (BOOLEAN *),NAT means :Def110: :: BINARI_6:def 7

for x being Element of BOOLEAN * holds it . x = ExAbsval x;

existence for x being Element of BOOLEAN * holds it . x = ExAbsval x;

ex b

for x being Element of BOOLEAN * holds b

uniqueness

for b

b

proof end;

:: deftheorem Def110 defines BL2Nat BINARI_6:def 7 :

for b_{1} being Function of (BOOLEAN *),NAT holds

( b_{1} = BL2Nat iff for x being Element of BOOLEAN * holds b_{1} . x = ExAbsval x );

for b

( b

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;
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;

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;

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))

for K being Nat st len x <> 0 & len x <= K holds

ExAbsval x = Absval (ExtBit (x,K))

proof end;

definition

ex b_{1} being Equivalence_Relation of (BOOLEAN *) st

for x, y being object holds

( [x,y] in b_{1} iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) )

for b_{1}, b_{2} being Equivalence_Relation of (BOOLEAN *) st ( for x, y being object holds

( [x,y] in b_{1} iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) holds

b_{1} = b_{2}
end;

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 for x, y being object holds

( [x,y] in it iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) );

ex b

for x, y being object holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def300 defines EqBL2Nat BINARI_6:def 8 :

for b_{1} being Equivalence_Relation of (BOOLEAN *) holds

( b_{1} = EqBL2Nat iff for x, y being object holds

( [x,y] in b_{1} iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) );

for b

( b

( [x,y] in b

definition

ex b_{1} being Function of (Class EqBL2Nat),NAT st

for A being Element of Class EqBL2Nat ex x being object st

( x in A & b_{1} . A = BL2Nat . x )

for b_{1}, b_{2} being Function of (Class EqBL2Nat),NAT st ( for A being Element of Class EqBL2Nat ex x being object st

( x in A & b_{1} . A = BL2Nat . x ) ) & ( for A being Element of Class EqBL2Nat ex x being object st

( x in A & b_{2} . A = BL2Nat . x ) ) holds

b_{1} = b_{2}
end;

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 for A being Element of Class EqBL2Nat ex x being object st

( x in A & it . A = BL2Nat . x );

ex b

for A being Element of Class EqBL2Nat ex x being object st

( x in A & b

proof end;

uniqueness for b

( x in A & b

( x in A & b

b

proof end;

:: deftheorem Def400 defines QuBL2Nat BINARI_6:def 9 :

for b_{1} being Function of (Class EqBL2Nat),NAT holds

( b_{1} = QuBL2Nat iff for A being Element of Class EqBL2Nat ex x being object st

( x in A & b_{1} . A = BL2Nat . x ) );

for b

( b

( x in A & b

LemmaQU: QuBL2Nat is onto

proof end;

LM600: QuBL2Nat is one-to-one

proof end;

definition

let A, B be Element of Class EqBL2Nat;

ex b_{1} being Element of Class EqBL2Nat ex x, y being Element of BOOLEAN * st

( x in A & y in B & b_{1} = Class (EqBL2Nat,(x + y)) )

for b_{1}, b_{2} being Element of Class EqBL2Nat st ex x, y being Element of BOOLEAN * st

( x in A & y in B & b_{1} = Class (EqBL2Nat,(x + y)) ) & ex x, y being Element of BOOLEAN * st

( x in A & y in B & b_{2} = Class (EqBL2Nat,(x + y)) ) holds

b_{1} = b_{2}

end;
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 x, y being Element of BOOLEAN * st

( x in A & y in B & it = Class (EqBL2Nat,(x + y)) );

ex b

( x in A & y in B & b

proof end;

uniqueness for b

( x in A & y in B & b

( x in A & y in B & b

b

proof end;

:: deftheorem Def500 defines + BINARI_6:def 10 :

for A, B, b_{3} being Element of Class EqBL2Nat holds

( b_{3} = A + B iff ex x, y being Element of BOOLEAN * st

( x in A & y in B & b_{3} = Class (EqBL2Nat,(x + y)) ) );

for A, B, b

( b

( x in A & y in B & b

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))

for x, y being Element of BOOLEAN * st x in A & y in B holds

A + B = Class (EqBL2Nat,(x + y))

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)

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 )

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;