Proof of correctness of the Firsov–Jeltsch order maintenance algorithm
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.