`firstPassProgram_nodup`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAEmpiricalProgram
domain: Foundation
line: 61 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAEmpiricalProgram on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  58  unfold firstPassProgram
  59  rw [List.length_map, firstPassSchedule_length]
  60
  61theorem firstPassProgram_nodup :
  62    firstPassProgram.Nodup := by
  63  unfold firstPassProgram
  64  exact List.Nodup.map programSpec_injective firstPassSchedule_nodup
  65
  66/-- The first-pass program contains exactly the high-or-immediate tests. -/
  67theorem firstPassProgram_exact_top_priority (c : CombinationID) :
  68    c ∈ firstPassSchedule ↔ isHighOrImmediate c :=
  69  firstPassSchedule_mem_iff_high_or_immediate c
  70
  71theorem scheduled_program_ready
  72    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  73    (programSpec c).ready = empiricallyReady_all c :=
  74  rfl
  75
  76theorem scheduled_program_pipeline
  77    {c : CombinationID} (_h : c ∈ firstPassSchedule) :
  78    (programSpec c).pipeline = pipelineSpec c :=
  79  rfl
  80
  81theorem firstPassProgram_actions_nodup :
  82    firstPassActions.Nodup :=
  83  firstPassActions_nodup
  84
  85theorem firstPassProgram_deliverables_nodup :
  86    firstPassDeliverables.Nodup :=
  87  firstPassDeliverables_nodup
  88
  89theorem firstPassProgram_pipelines_nodup :
  90    firstPassPipelines.Nodup :=
  91  firstPassPipelines_nodup

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.