Finiteness conjecture for unit equations in finite-dimensional division algebras

Let $A$ be a finite-dimensional division algebra over $\mathbb{Q}$, and let $\Gamma_1,\Gamma_2$ be finitely generated semigroups of the multiplicative group $A^\times$. Fix $a,a',b,b'\in A^\times$. Noncommutative unit-equation conjecture. The equation

$$afa'+bgb'=1$$

has only finitely many solutions with $f\in\Gamma_1$ and $g\in\Gamma_2$. Moreover, there is an effectively computable finite subset $S\subseteq\Gamma_1\times\Gamma_2$, determined by $a,a',b,b'$ and generators of $\Gamma_1,\Gamma_2$, such that every solution $(f,g)\in\Gamma_1\times\Gamma_2$ lies in $S$. This conjecture extends the preceding finiteness results for quaternion unit equations beyond the commutative setting and to arbitrary finite-dimensional division algebras; the effective finiteness assertion remains open.