let x, y be Element of BOOLEAN * ; :: thesis: BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)
XP1: BL2Nat . x = ExAbsval x by Def110;
XP2: BL2Nat . y = ExAbsval y by Def110;
set ENx = ExtBit (x,(LenMax (x,y)));
set ENy = ExtBit (y,(LenMax (x,y)));
set ENx1 = ExtBit (x,((LenMax (x,y)) + 1));
set ENy1 = ExtBit (y,((LenMax (x,y)) + 1));

per cases ( len x = 0 or len y = 0 or ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 ) or ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 ) ) ;

suppose C1: len x = 0 ; :: thesis: BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)

hence BL2Nat . (x + y) = 0 + (BL2Nat . y) by Def3
.= (BL2Nat . x) + (BL2Nat . y) by XP1, C1, D100 ;
:: thesis: verum

end;

suppose C2: len y = 0 ; :: thesis: BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)

hence BL2Nat . (x + y) = (BL2Nat . x) + 0 by Def3
.= (BL2Nat . x) + (BL2Nat . y) by XP2, C2, D100 ;
:: thesis: verum

end;

suppose C3: ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 ) ; :: thesis: BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)

then C4: x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) by Def3;
PXP3: LenMax (x,y) = max ((len x),(len y)) by Def15, C3;
XP7: BL2Nat . x = ExAbsval x by Def110
.= Absval (ExtBit (x,(LenMax (x,y)))) by PXP3, C3, LM230, XXREAL_0:25 ;
XP8: BL2Nat . y = ExAbsval y by Def110
.= Absval (ExtBit (y,(LenMax (x,y)))) by PXP3, C3, LM230, XXREAL_0:25 ;
XP15: ExAbsval (x + y) = Absval ((ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y))))) by C4, Def100;
thus BL2Nat . (x + y) = ExAbsval (x + y) by Def110
.= (BL2Nat . x) + (BL2Nat . y) by XP7, XP8, C3, BINARITH:22, XP15 ; :: thesis: verum

end;

suppose C3: ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 ) ; :: thesis: BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)

then C4: x + y = (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) by Def3;
PXP3: LenMax (x,y) = max ((len x),(len y)) by Def15, C3;
then ( len x <= LenMax (x,y) & len y <= LenMax (x,y) ) by XXREAL_0:25;
then XP5: ( (len x) + 0 <= (LenMax (x,y)) + 1 & (len y) + 0 <= (LenMax (x,y)) + 1 ) by XREAL_1:7;
XP9: BL2Nat . x = ExAbsval x by Def110
.= Absval (ExtBit (x,((LenMax (x,y)) + 1))) by XP5, C3, LM230 ;
XP10: BL2Nat . y = ExAbsval y by Def110
.= Absval (ExtBit (y,((LenMax (x,y)) + 1))) by XP5, C3, LM230 ;
XX1: ExtBit (x,((LenMax (x,y)) + 1)) = (ExtBit (x,(LenMax (x,y)))) ^ <*0*> by PXP3, LMExtBit1, XXREAL_0:25;
XX2: ExtBit (y,((LenMax (x,y)) + 1)) = (ExtBit (y,(LenMax (x,y)))) ^ <*0*> by PXP3, LMExtBit1, XXREAL_0:25;
XP15: ExAbsval (x + y) = Absval ((ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1)))) by C4, Def100;
thus BL2Nat . (x + y) = ExAbsval (x + y) by Def110
.= (BL2Nat . x) + (BL2Nat . y) by XP9, XP10, BINARITH:22, XP15, XX1, XX2, LMExtBit2 ; :: thesis: verum

end;

end;