speed up shift/rot formal proof by running stuff in parallel