B model: Improve provability of the View service set (continued)

Cleanup the B specifications of the modules below service_set_view to make them provable (mostly by removing what is clearly incorrect or not corresponding to the implementation).

This is a follow-up of #1152 (closed).