firstPassProgram_exact_top_priority

formal source

  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
  92
  93/-- First-pass completion gate: every scheduled row is ready and every output
  94class is collision-free. -/
  95def FirstPassProgramComplete : Prop :=
  96  FirstPassReady ∧
  97    firstPassProgram.length = 5 ∧