Monoid condition for decidable exponentials (source code)

= Monoid condition for decidable exponentials
{title2=$\forall m\ \exists p,q:\ pmq=p$}

If each $m$ admits $p,q$ with $pmq=p$, then $B^A$ is decidable whenever the left <M-set> $B$ is. For equivariant $f,g$, equality of all values at $(1,a)$ implies equality at $(m,a)$: apply $p$ and use $f(pm,p a)=pm\cdot f(1,q a)$, then cancel the injective action of $p$ on $B$. Equality after the exponential action of $m$ then gives equal traces by cancelling its action on $B$.