Add internalised rules for derived resource algebras
Working with the resource algebras at different levels (e.g. in the model and in the logic), requires different rewriting rules to avoid breaking abstraction.
An example of these are the rules of auth
, which have auth_both_valid
(in the model), auth_both_validN
(in the model, with step-indices), and auth_both_validI
(in the logic).
Some derived resource algebras are missing their "internalised rules" (those of the logic).
This issue is then to address the lack of these rules.
One example of a resource algebra with missing rules are mono_list
.
In full, to solve this issue we should:
- Identify all resource algebras with missing internalised rules
- Add the missing rules
- (Settle on a potential pipeline for future algebras to ensure that the rules are included)