For citations:

Podymov V.V., Zakharov V.A. A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2014;26(3):145-166. (In Russ.) https://doi.org/10.15514/ISPRAS-2014-26(3)-8