Formal modelling of the electricity markets: the example of the load reduction of electricity mechanism "NEBEF". Issue 1 (November 2021)