pith. machine review for the scientific record. sign in
def 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)

 127def empiricalProgramCert : EmpiricalProgramCert where
 128  program_injective := programSpec_injective

proof body

Definition body.

 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
 135  action_classes_nodup := firstPassProgram_actions_nodup
 136  deliverable_classes_nodup := firstPassProgram_deliverables_nodup
 137  pipeline_records_nodup := firstPassProgram_pipelines_nodup
 138  exact_top_priority := firstPassProgram_exact_top_priority
 139
 140end OptionAEmpiricalProgram
 141end Foundation
 142end IndisputableMonolith

depends on (12)

Lean names referenced from this declaration's body.