From the comments, it seems likely that the author doesn't have a precise definition of non-trivial. But the framework still feels potentially useful as a way t

From the comments, it seems likely that the author doesn't have a precise definition of non-trivial. But the framework still feels potentially useful as a way to precisely parameterize disagreements about whether or not a given semantics is declarative. That said, I'm also having some trouble with the concept. Take for example the rule: there exists x such that succ(x) = y ⊢ dec(y) = x. If we're used to operational semantics which include pattern matching, this feels trivial. But otherwise we have to be clever to avoid exhaustive search. I'm a bit out of my depth here, but it sort-of feels like 'non-trivial' here means 'I can't immediately/uniquely produce a corresponding well-moded operational semantics'. Whether this lends any clarity might be a matter of taste...