We present sound and complete environmental bisimilarities for a

variant of Dybvig et al.'s calculus of multi-prompted

delimited-control operators with dynamic prompt generation. The

reasoning principles that we obtain generalize and advance the

existing techniques for establishing program equivalence in calculi

with single-prompted delimited control.

The basic theory that we develop is presented using Madiot et al.'s

framework that allows for smooth integration and composition of up-to

techniques facilitating bisimulation proofs. We also generalize the

framework in order to express environmental bisimulations that support

equivalence proofs of evaluation contexts representing

continuations. This change leads to a novel and powerful up-to

technique enhancing bisimulation proofs in the presence of control

operators.