let x, y be Element of BOOLEAN * ; :: thesis: ( x in rng Nat2BL & y in rng Nat2BL implies x + y in rng Nat2BL )
assume AS1: ( x in rng Nat2BL & y in rng Nat2BL ) ; :: thesis: x + y in rng Nat2BL
then ( x in { x where x is Element of BOOLEAN * : x . (len x) = 1 } or x in {<*0*>} ) by XBOOLE_0:def 3, LM031;
then PP1: ( ex x0 being Element of BOOLEAN * st
( x = x0 & x0 . (len x0) = 1 ) or x in {<*0*>} ) ;
( y in { y where y is Element of BOOLEAN * : y . (len y) = 1 } or y in {<*0*>} ) by XBOOLE_0:def 3, LM031, AS1;
then ( ex y0 being Element of BOOLEAN * st
( y = y0 & y0 . (len y0) = 1 ) or y in {<*0*>} ) ;

per cases then ( x = <*0*> or y = <*0*> or ( x . (len x) = 1 & y . (len y) = 1 ) ) by PP1, TARSKI:def 1;

suppose ( x = <*0*> or y = <*0*> ) ; :: thesis: x + y in rng Nat2BL

per cases then ( x = <*0*> or y = <*0*> ) ;

suppose C1: x = <*0*> ; :: thesis: x + y in rng Nat2BL

then reconsider z = x as Tuple of 1, BOOLEAN ;
P1: len x = 1 by FINSEQ_1:40, C1;
P2: 1 <= len y by LM0710, AS1;
P30: ( len x <> 0 & len y <> 0 ) by LM0710, AS1;
then P3: LenMax (x,y) = max ((len x),(len y)) by Def15
.= len y by P1, XXREAL_0:def 10, LM0710, AS1 ;
P6: (len y) -' (len y) = (len y) - (len y) by XREAL_0:def 2
.= 0 ;
P7: (len y) -' (len x) = (len y) - 1 by XREAL_0:def 2, XREAL_1:48, P1, P2;
set x1 = ExtBit (x,(LenMax (x,y)));
set y1 = ExtBit (y,(LenMax (x,y)));
P4: ExtBit (x,(LenMax (x,y))) = x ^ (0* ((len y) -' (len x))) by P1, P3, Def20, LM0710, AS1;
P5: ExtBit (y,(LenMax (x,y))) = y ^ (0* 0) by P6, P3, Def20
.= y by FINSEQ_1:34 ;
set K1 = LenMax (x,y);
reconsider K = (LenMax (x,y)) - 1 as Nat by P2, P3, INT_1:5, ORDINAL1:def 12;
P6: ExtBit (x,(LenMax (x,y))) = 0* (((len y) -' (len x)) + 1) by LM0020, P4, C1, FINSEQ_2:123
.= 0* (LenMax (x,y)) by P3, P7 ;
(carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y)) = 0 by P6, LMExtBit3;
then ((((ExtBit (x,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((ExtBit (y,(LenMax (x,y)))) /. (LenMax (x,y)))) 'or' (((ExtBit (x,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y))))) 'or' (((ExtBit (y,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y)))) = 0 by P6, LMExtBit4;
then add_ovfl ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y))))) = FALSE by BINARITH:def 6;
then x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) by Def3, P30, BINARITH:def 7;
hence x + y in rng Nat2BL by AS1, LMExtBit5, P6, P5; :: thesis: verum

end;

suppose C1: y = <*0*> ; :: thesis: x + y in rng Nat2BL

then reconsider z = y as Tuple of 1, BOOLEAN ;
P1: len y = 1 by FINSEQ_1:40, C1;
P2: 1 <= len x by LM0710, AS1;
P30: ( len x <> 0 & len y <> 0 ) by LM0710, AS1;
then P3: LenMax (x,y) = max ((len x),(len y)) by Def15
.= len x by P1, XXREAL_0:def 10, LM0710, AS1 ;
P6: (len x) -' (len x) = (len x) - (len x) by XREAL_0:def 2
.= 0 ;
P7: (len x) -' (len y) = (len x) - 1 by XREAL_0:def 2, XREAL_1:48, P1, P2;
set x1 = ExtBit (x,(LenMax (x,y)));
set y1 = ExtBit (y,(LenMax (x,y)));
P4: ExtBit (y,(LenMax (x,y))) = y ^ (0* ((len x) -' (len y))) by P1, P3, Def20, LM0710, AS1;
P5: ExtBit (x,(LenMax (x,y))) = x ^ (0* 0) by P6, P3, Def20
.= x by FINSEQ_1:34 ;
set K1 = LenMax (x,y);
reconsider K = (LenMax (x,y)) - 1 as Nat by P2, P3, INT_1:5, ORDINAL1:def 12;
P6: ExtBit (y,(LenMax (x,y))) = 0* (((len x) -' (len y)) + 1) by LM0020, P4, C1, FINSEQ_2:123
.= 0* (LenMax (x,y)) by P3, P7 ;
(carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y)) = 0 by P6, LMExtBit3;
then ((((ExtBit (x,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((ExtBit (y,(LenMax (x,y)))) /. (LenMax (x,y)))) 'or' (((ExtBit (x,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y))))) 'or' (((ExtBit (y,(LenMax (x,y)))) /. (LenMax (x,y))) '&' ((carry ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y)))))) /. (LenMax (x,y)))) = 0 by P6, LMExtBit4;
then add_ovfl ((ExtBit (x,(LenMax (x,y)))),(ExtBit (y,(LenMax (x,y))))) = FALSE by BINARITH:def 6;
then x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) by Def3, P30, BINARITH:def 7;
hence x + y in rng Nat2BL by AS1, LMExtBit5, P6, P5; :: thesis: verum

end;

end;

end;

suppose Y1: ( x . (len x) = 1 & y . (len y) = 1 ) ; :: thesis: x + y in rng Nat2BL

X1: ( len x <> 0 & len y <> 0 )

proof

assume ( len x = 0 or len y = 0 ) ; :: thesis: contradiction
then ( x = {} or y = {} ) ;
hence contradiction by Y1; :: thesis: verum

end;

(x + y) . (len (x + y)) = 1

proof

per cases ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable or not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable ) ;

suppose C1: ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable ; :: thesis: (x + y) . (len (x + y)) = 1

then C2: x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) by X1, Def3;
set x1 = ExtBit (x,(LenMax (x,y)));
set y1 = ExtBit (y,(LenMax (x,y)));
len x <> len y

proof

assume C10: len x = len y ; :: thesis: contradiction
C11: LenMax (x,y) = max ((len x),(len y)) by X1, Def15
.= len y by C10 ;
LenMax (x,y) = max ((len x),(len y)) by X1, Def15
.= len x by C10 ;
then ( ExtBit (x,(LenMax (x,y))) = x & ExtBit (y,(LenMax (x,y))) = y ) by LMExtBit8, C11;
hence contradiction by C1, LMExtBit9, Y1; :: thesis: verum

end;

per cases then ( len x < len y or len y < len x ) by XXREAL_0:1;

suppose C11: len x < len y ; :: thesis: (x + y) . (len (x + y)) = 1

LenMax (x,y) = max ((len x),(len y)) by X1, Def15
.= len y by C11, XXREAL_0:def 10 ;
then ExtBit (y,(LenMax (x,y))) = y by LMExtBit8;
hence (x + y) . (len (x + y)) = 1 by Y1, C1, LMExtBit6, C2; :: thesis: verum

end;

suppose C11: len y < len x ; :: thesis: (x + y) . (len (x + y)) = 1

LenMax (x,y) = max ((len x),(len y)) by X1, Def15
.= len x by C11, XXREAL_0:def 10 ;
then ExtBit (x,(LenMax (x,y))) = x by LMExtBit8;
hence (x + y) . (len (x + y)) = 1 by C2, C1, LMExtBit6, Y1; :: thesis: verum

end;

end;

end;

suppose C12: not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable ; :: thesis: (x + y) . (len (x + y)) = 1

then C13: x + y = (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) by X1, Def3;
set Nx = ExtBit (x,(LenMax (x,y)));
set Ny = ExtBit (y,(LenMax (x,y)));
set Nx1 = ExtBit (x,((LenMax (x,y)) + 1));
set Ny1 = ExtBit (y,((LenMax (x,y)) + 1));
C16: LenMax (x,y) = max ((len x),(len y)) by X1, Def15;
then C14: ExtBit (x,((LenMax (x,y)) + 1)) = (ExtBit (x,(LenMax (x,y)))) ^ <*0*> by LMExtBit1, XXREAL_0:25;
ExtBit (y,((LenMax (x,y)) + 1)) = (ExtBit (y,(LenMax (x,y)))) ^ <*0*> by C16, LMExtBit1, XXREAL_0:25;
hence (x + y) . (len (x + y)) = 1 by C13, C12, C14, LMExtBit7; :: thesis: verum

end;

end;

end;

then ( x + y in { y where y is Element of BOOLEAN * : y . (len y) = 1 } or x + y in {<*0*>} ) ;
hence x + y in rng Nat2BL by LM031, XBOOLE_0:def 3; :: thesis: verum

end;

end;