p. 65, worked example — the order (5, 1, 4, 3, 2) takes 47 units, the reversed order 78

Proved

JohnsonFlowShop.TwoStage.example_p65

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

flow-shopjohnson-rulep2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Consider the five items of Johnson's example, with processing times

item (paper)	1	2	3	4	5
$A_i$	4	4	30	6	2
$B_i$	5	1	4	30	3

For an order $\rho$ , write $T(\rho)$ for the total elapsed time of its as-soon-as-possible schedule. Then

the order $(5, 1, 4, 3, 2)$ has $T = 47$ ;
its total delay (idle) time on machine 2 is $47 - \sum_i B_i = 47 - 43 = 4$ ;
the reversed order $(2, 3, 4, 1, 5)$ has $T = 78$ ;
every order $\rho$ satisfies $47 \le T(\rho) \le 78$ .

So $(5, 1, 4, 3, 2)$ , the order the working rule produces, is optimal and the reversed order is the worst possible.

Formalization Note Items are 0-based in Lean: the paper's order $(5,1,4,3,2)$ is the permutation $\sigma$ with $\sigma = (4, 0, 3, 2, 1)$ (position $\mapsto$ item) and the reversed order $(2,3,4,1,5)$ is $\tau = (1, 2, 3, 0, 4)$ . "Optimal" and "worst" are stated over all orders with their as-soon-as-possible schedules.

Preamble

import Mathlib
import Definitions.Def_JohnsonFlowShop_Shared_makespan
import Definitions.Def_JohnsonFlowShop_TwoStage_asapStart2

Formal statement

namespace JohnsonFlowShop.TwoStage

/-- The worked example of p. 65, with items renumbered 0–4: `A = (4, 4, 30, 6, 2)`,
`B = (5, 1, 4, 30, 3)`. The order `(4, 0, 3, 2, 1)` (the paper's `(5, 1, 4, 3, 2)`) has
as-soon-as-possible total elapsed time 47 and total machine-2 idle time `47 - ∑ B = 4`; the
reversed order `(1, 2, 3, 0, 4)` has 78; every order has total elapsed time between 47 and 78. -/
theorem example_p65 :
    let A : Fin 5 → ℝ := ![4, 4, 30, 6, 2]
    let B : Fin 5 → ℝ := ![5, 1, 4, 30, 3]
    let σ : Equiv.Perm (Fin 5) := ⟨![4, 0, 3, 2, 1], ![1, 4, 3, 2, 0], by decide, by decide⟩
    let τ : Equiv.Perm (Fin 5) := ⟨![1, 2, 3, 0, 4], ![3, 0, 1, 2, 4], by decide, by decide⟩
    Shared.makespan B (asapStart2 A B σ) = 47 ∧
    Shared.makespan B (asapStart2 A B σ) - ∑ i, B i = 4 ∧
    Shared.makespan B (asapStart2 A B τ) = 78 ∧
    ∀ ρ : Equiv.Perm (Fin 5),
      47 ≤ Shared.makespan B (asapStart2 A B ρ) ∧ Shared.makespan B (asapStart2 A B ρ) ≤ 78 := by sorry

end JohnsonFlowShop.TwoStage

Source

Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, NRLQ 1(1) 1954, p. 65, worked example (table of A_i, B_i)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph