Reserved{,Confl}{,Mut} are all removed and replaced by Reserved m cf where m := InteriorMut | TyFrz and cf := ResConflicted | ResActivable
The reachability statement is adapted with InteriorMut and TyFrz unreachable from each other, and ResActivable able to become ResConflicted but not the opposite.
This may be an opportunity to also simplify the transition function by merging similar cases, but not today.
