C-D23-EARLY-CUTS

Tính VỮNG của cut sớm D23 đã chứng minh: mọi cut sớm (khả-dĩ số học hay impropriety refinement) là điều kiện CẦN cho một phản ví dụ có chặn, nên tổ hợp của chúng không loại phản ví dụ nào. Áp TRƯỚC ngưỡng tái dựng 2H, sửa D22 nơi kiểm toàn cục duy nhất đợi tới tái dựng

Nói dễ hiểu

Mọi cut sớm được chứng minh an toàn: nó chỉ loại các đối tượng mà một phản ví dụ thật không bao giờ là.

Phát biểu chính xác

Tính VỮNG của cut sớm D23 đã chứng minh: mọi cut sớm (khả-dĩ số học hay impropriety refinement) là điều kiện CẦN cho một phản ví dụ có chặn, nên tổ hợp của chúng không loại phản ví dụ nào. Áp TRƯỚC ngưỡng tái dựng 2H, sửa D22 nơi kiểm toàn cục duy nhất đợi tới tái dựng