Formal counterexample wave

Step through a formal counterexample trace {t, a, b, ok}. Highlight the failing cycle; use Prev/Next to walk time. Starter: failure at t=3 where ok=false.