C-D24-REACHABLE

Ngữ nghĩa mod-84 toàn cục D24 PROVED-INTERNAL: biểu diễn reachable state bằng một residue multiset chung modulo 84 = lcm(14,28,42), một đồng hồ toàn cục duy nhất không chọn lại theo prime. Cut chính xác đóng băng: t=1/14 là thời điểm cô đơn khi và chỉ khi 14 không chia tốc độ nào, nên một phản ví dụ có chặn phải có ít nhất một V_i chia hết cho 14 (kiểm kích hoạt trên nhân chứng p=197); điều kiện test-time tương tự tại level 28 và 42 là chính xác, không tổng quát hóa thành impropriety level-l đầy đủ

Nói dễ hiểu

Một đồng hồ chung modulo 84 với quy tắc chính xác: mọi phản ví dụ phải có một người chạy tốc độ là bội của 14, nếu không thời điểm 1/14 sẽ cô đơn.

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

Ngữ nghĩa mod-84 toàn cục D24 PROVED-INTERNAL: biểu diễn reachable state bằng một residue multiset chung modulo 84 = lcm(14,28,42), một đồng hồ toàn cục duy nhất không chọn lại theo prime. Cut chính xác đóng băng: t=1/14 là thời điểm cô đơn khi và chỉ khi 14 không chia tốc độ nào, nên một phản ví dụ có chặn phải có ít nhất một V_i chia hết cho 14 (kiểm kích hoạt trên nhân chứng p=197); điều kiện test-time tương tự tại level 28 và 42 là chính xác, không tổng quát hóa thành impropriety level-l đầy đủ