  Bounded proofs are convenient to use due to the high degree of automation
that exhaustive checking affords. However, they fall short of providing the
robust assurances offered by unbounded proofs. We sketch how completeness
thresholds serve as a bridge, allowing us to derive unbounded guarantees from
bounded proofs. Using a bubble sort implementation as example, we demonstrate
that a bounded proof only needs to consider a few specific inputs to yield
unbounded guarantees.
