theorem proved wrapper

`firstPassProgram_exact_top_priority`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
  68    c ∈ firstPassSchedule ↔ isHighOrImmediate c :=

One-line wrapper that applies firstPassSchedule_mem_iff_high_or_immediate.

  69  firstPassSchedule_mem_iff_high_or_immediate c
  70

From the project-wide theorem graph. These declarations reference this one in their body.

empiricalProgramCert in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use

Lean names referenced from this declaration's body.

isHighOrImmediate in IndisputableMonolith.Foundation.OptionAEmpiricalQueue decl_use
firstPassSchedule in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use
firstPassSchedule_mem_iff_high_or_immediate in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use
CombinationID in IndisputableMonolith.Foundation.OptionAFalsifierRegistry decl_use