Model of concatenation theory with left-cancellation but no right-cancellation

The theory of concatenation (TC) can be equivalently expressed as the following assumptions:

1. Closure of strings under concatenation $+$.
2. Existence of an empty string $e$, namely $e+x = x = x+e$ for any string $x$.
3. Associativity of $+$ on strings, namely $(x+y)+z = x+(y+z)$ for any strings $x,y,z$.
4. Existence of distinct symbols $p,q$, namely distinct non-empty strings $p,q$ such that
   $p \ne u+v$ and $q \ne u+v$ for any non-empty strings $u,v$.
5. Given any strings $a,b,c,d$ such that $a+b = c+d$, there is a string $x$ such that
   either ( $a+x = c$ and $b = x+d$ ) or ( $a = c+x$ and $x+b = d$ ).

Formally in first-order logic, TC is axiomatized as the theory with a binary function-symbol $+$ and constant-symbols $e,p,q$ and the following axioms:

1. $∀x\ ( \ x+e = x = e+x \ )$.
2. $∀x,y,z\ ( \ (x+y)+z = x+(y+z) \ )$.
3. $p≠q ∧ p≠e ∧ q≠e$
   ${} ∧ ¬∃u,v\ ( \ u≠e ∧ v≠e ∧ ( p=u+v ∨ q=u+v ) \ )$.
4. $∀a,b,c,d\ ( \ a+b = c+d$
   ${} ⇒ ∃x\ ( \ a+x=c ∧ b=x+d ∨ a=c+x ∧ x+b=d \ ) \ )$.

Someone asked me (essentially) whether TC proves the cancellation property. This can be split into left-cancellation (LC) and right-cancellation (RC):

• (LC) $∀x,y,c\ ( \ c+x = c+y ⇒ x=y \ )$.
• (RC) $∀x,y,c\ ( \ x+c = y+c ⇒ x=y \ )$.

Of course, finite strings (the intended model of TC) satisfy cancellation (both LC and RC). So the question can be understood as asking whether these are independent over TC. Incidentally, LC and RC can be proven by TC plus a suitable induction schema.

I came up with countable binary-labelled linear orders modulo isomorphism (with $+$ interpreted as concatenation modulo isomorphism) as a model of TC that fails to satisfy cancellation. I also realize that countable binary-labelled well-orders modulo isomorphism is a model of TC and LC but not RC, because for any well-ordering every prefix embeds uniquely into itself, but not suffixes. An explicit counter-example for RC is $(0)+(0,0,0,\cdots) = ()+(0,0,0,\cdots)$.

My questions are:

What are other simple models of TC+LC+¬RC?

Is there a more systematic way of finding a model? (Mine was ad-hoc.)

I think TC and PA$^-$ are bi-interpretable. If so, can we utilize that to find nice models?

The downside to "countable binary-labelled well-orders modulo isomorphism" is of course that you cannot compute explicitly in it -- it has uncountably many elements.

We get something better behaved if we consider only those elements where (a) the well-order is shorter than $\omega^2$, and (b) only finitely many positions are labeled $1$.

This is isomorphic to

The monoid of finite strings over $\{0,1,\infty\}$, modulo the relation $0\infty=\infty$.

where $\infty$ intuitively represents a sequence of $\omega$ many $0$s.

More systematically, lack of right cancellation plus the $abcd$ axiom implies that there must be elements $a,x,d$ such that $$ ax \ne a \qquad\text{and}\qquad xd=d $$ If we simply make this into the presentation of a monoid, we get $$ \langle a, x, d \mid xd=d \rangle $$ which is isomorphic to the above -- so what we have is in a certain sense the "simplest" model in that every solution must contain a homomorphic image of this that distinguishes between $ax$ and $a$.