X0:
2 + 1 < 2 to_power 2
by POWER:60;
X1:
2 = 2 to_power 1
;
log (2,3) < log (2,4)
by POWER:57;
then
log (2,3) < 2
by POWER:60, POWER:def 3;
then X4:
(log (2,3)) - 1 < 2 - 1
by XREAL_1:14;
log (2,2) < log (2,3)
by POWER:57;
then
1 < log (2,3)
by POWER:52;
then X5:
[\(log (2,3))/] = 1
by INT_1:def 6, X4;
LenBSeq 3 =
[\(log (2,3))/] + 1
by EXL2
.=
2
by X5
;
then X2: Nat2BL . 3 =
2 -BinarySequence 3
by BINARI_6:def 2
.=
(2 -BinarySequence 2) + (Bin1 2)
by BINARI_3:33, X0
;
X3:
2 -BinarySequence 2 = <*FALSE*> ^ <*TRUE*>
by XBOOLEAN:def 1, XBOOLEAN:def 2, BINARI_6:4, X1, BINARI_3:28;
X5:
Bin1 2 = <*TRUE*> ^ <*FALSE*>
by BINARI_3:10, BINARI_2:7;
set z1 = <*FALSE*>;
set z2 = <*TRUE*>;
X7:
(carry (<*FALSE*>,<*TRUE*>)) /. 1 = FALSE
by BINARITH:def 2;
X70:
<*FALSE*> /. 1 = FALSE
by FINSEQ_4:16;
<*TRUE*> /. 1 = TRUE
by FINSEQ_4:16;
then X6: add_ovfl (<*FALSE*>,<*TRUE*>) =
(FALSE 'or' (FALSE '&' FALSE)) 'or' (TRUE '&' FALSE)
by MARGREL1:13, X7, X70
.=
FALSE
by MARGREL1:13
;
(2 -BinarySequence 2) + (Bin1 2) =
(<*FALSE*> + <*TRUE*>) ^ <*((TRUE 'xor' FALSE) 'xor' (add_ovfl (<*FALSE*>,<*TRUE*>)))*>
by BINARITH:19, X3, X5
.=
<*TRUE*> ^ <*(TRUE 'xor' (add_ovfl (<*FALSE*>,<*TRUE*>)))*>
by BINARITH:8, BINARI_3:17
.=
<*TRUE*> ^ <*TRUE*>
by X6, BINARITH:8
;
hence
Nat2BL . 3 = <*1,1*>
by X2, XBOOLEAN:def 2; verum