We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of nil, action prefix, choice, and the recursion construct.

@article{abs-1801-01180,
  title = {Rooted Divergence-Preserving Branching Bisimilarity is a Congruence},
  author = {Rob van Glabbeek and Bas Luttik and Linda Spaninks},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:14)2020}
}