The macro vocabulary stays far below its worst case

The general bound (Proposition 1) is ∑r=1..k|Δ|r. Reachable counts the guard-satisfiable blocks actually enumerated; merged applies canonical merging. For parity and mod 3, reachable counts equal 2(k+1) and 3(k+1), attaining the corrected Proposition 3 bound. The general bound and plotted counts are unchanged.

task
worst-case bound reachable merged