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.

翻译：有界证明因其穷举检查提供的高度自动化而便于使用。然而，它们无法提供无界证明所能提供的稳健保证。我们简要阐述了完备性阈值如何作为桥梁，使我们能够从有界证明中推导出无界保证。以冒泡排序实现为例，我们证明，有界证明只需考虑少数特定输入，即可产生无界保证。