59structure CriticalPathCert where 60 cost_on_plan : ∀ d : ℝ, d ≠ 0 → scheduleVarianceCost d d = 0 61 cost_nonneg : ∀ a p : ℝ, 0 < a → 0 < p → 0 ≤ scheduleVarianceCost a p 62 buffer_pos : 0 < optimalBufferFraction 63 buffer_lt_half : optimalBufferFraction < 1 / 2 64
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.