s≤′s (s≤′s (⌊n/2⌋≤′n n)) --> log2<′ n