Legacy coverage adds interval counts. Critical cumulative coverage is an
exact prefix snapshot: repeated checkpoints replace totals, never add them.
One selected sequence is either accepted or dropped; policy exclusions
consume no sequence. Shared by cumulative coverage and live observer views.
410def aosSequenceAccounting =
411 (lambda unrestricted next : Nat . (lambda unrestricted accepted : Nat .
412 (lambda unrestricted dropped : Nat .
413 (naturalEqual next (naturalAdd accepted dropped)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.