pith. machine review for the scientific record. sign in
structure definition def or abbrev

EmpiricalProgramCert

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 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

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.