  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 ∧
  98    firstPassProgram.Nodup ∧
  99    firstPassActions.Nodup ∧
 100    firstPassDeliverables.Nodup ∧
 101    firstPassPipelines.Nodup ∧
 102    (∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c)
 103
 104theorem firstPassProgramComplete : FirstPassProgramComplete := by
 105  exact ⟨firstPassReady, firstPassProgram_length, firstPassProgram_nodup,
 106    firstPassActions_nodup, firstPassDeliverables_nodup,
 107    firstPassPipelines_nodup, firstPassSchedule_mem_iff_high_or_immediate⟩
 108
 109structure EmpiricalProgramCert where
 110  program_injective : Function.Injective programSpec
 111  first_pass_length : firstPassProgram.length = 5
 112  first_pass_nodup : firstPassProgram.Nodup
 113  first_pass_ready : FirstPassReady
 114  first_pass_complete : FirstPassProgramComplete
 115  scheduled_ready :

papers checked against this theorem

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