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