theorem proved term proof

`firstPassProgram_nodup`

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

formal statement (Lean)

  61theorem firstPassProgram_nodup :
  62    firstPassProgram.Nodup := by

proof body

Term-mode proof.

  63  unfold firstPassProgram
  64  exact List.Nodup.map programSpec_injective firstPassSchedule_nodup
  65
  66/-- The first-pass program contains exactly the high-or-immediate tests. -/

used by (2)

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

empiricalProgramCert in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
firstPassProgramComplete in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use

depends on (8)

Lean names referenced from this declaration's body.

or in IndisputableMonolith.Constants.EulerMascheroni decl_use
contains in IndisputableMonolith.Ethics.StakeGraph decl_use
firstPassProgram in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
programSpec_injective in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
firstPassSchedule_nodup in IndisputableMonolith.Foundation.OptionAEmpiricalSchedule decl_use
tests in IndisputableMonolith.ILG.CPMInstance decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
contains in IndisputableMonolith.Numerics.Interval.Basic decl_use