for n being Nat st 0 < n holds
LenBSeq n = [\(log (2,n))/] + 1