let x, y be Element of BOOLEAN * ; 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 C3:
(
ExtBit (
x,
(LenMax (x,y))),
ExtBit (
y,
(LenMax (x,y)))
are_summable &
len x <> 0 &
len y <> 0 )
;
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
;
verum end; suppose C3:
( not
ExtBit (
x,
(LenMax (x,y))),
ExtBit (
y,
(LenMax (x,y)))
are_summable &
len x <> 0 &
len y <> 0 )
;
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
;
verum end; end;