In the order maintenance problem, the objective is to maintain a total order subject to insertions, deletions, and element comparisons.
This package provides a proof of correctness of the Firsov–Jeltsch order maintenance algorithm, carried out in Isabelle/HOL.