firstPassProgramComplete

formal source

 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 :
 116    ∀ {c : CombinationID}, c ∈ firstPassSchedule →
 117      (programSpec c).ready = empiricallyReady_all c
 118  scheduled_pipeline :
 119    ∀ {c : CombinationID}, c ∈ firstPassSchedule →
 120      (programSpec c).pipeline = pipelineSpec c
 121  action_classes_nodup : firstPassActions.Nodup
 122  deliverable_classes_nodup : firstPassDeliverables.Nodup
 123  pipeline_records_nodup : firstPassPipelines.Nodup
 124  exact_top_priority :
 125    ∀ c : CombinationID, c ∈ firstPassSchedule ↔ isHighOrImmediate c
 126
 127def empiricalProgramCert : EmpiricalProgramCert where
 128  program_injective := programSpec_injective
 129  first_pass_length := firstPassProgram_length
 130  first_pass_nodup := firstPassProgram_nodup
 131  first_pass_ready := firstPassReady
 132  first_pass_complete := firstPassProgramComplete
 133  scheduled_ready := scheduled_program_ready
 134  scheduled_pipeline := scheduled_program_pipeline