multiset matchbounds

(known fact) context closure changes matchbounds. random example:

• R=\{abc \to caba\} full mb 2
• S=\{abca \to cabaa, abcb \to cabab, abcc \to cabc\} not mb (I think)

we can still use the match heights for R in a termination proof for S:

for each S-step, we no longer have \min h(l)>\min h(r) but we use multiset comparison. Comparison of the minimal element is just an over-approximation for that.

in technical terms: we finite automata (matrix interpretation) into the semiring of multisets of numbers (heights). (semiring addition: min (pick the smaller of the multisets), semiring multiplication: union). I think this is already detailed in https://jalc.de/issues/2007/issue_12_4/jalc-2007-545-570.php

(new? idea) But then the question is: is multiset-matchboundedness still

• decidable (for fixed height, but unrestricted size of automaton)
• REG-preserving

next, we can map the multiset to the sum of its elements, to obtain tropical matrix interpretations. (also in the JALC paper). Same questions. - Note: boundedness is decidable for fixed size of automaton, because existence of an interpretation is solvability of a constraint system. Is it really? It holds for matchbounds and tropical. What about multiset matchbounds?