Let $E$ be the ring of integer valued polynomials over $\mathbb{Z}$. This ring is known to be a Prüfer domain. But it seems there does not exist an algorithm for inverting a nonzero finitely generated ideal of $E$. In this note we show how to obtain such an algorithm by deciphering a classical abstract proof that uses localisations of $E$ at all prime ideals of $E$. This confirms a general program of deciphering abstract classical proofs in order to obtain algorithmic proofs.

We prove that for any ring $𝐑$ of Krull dimension not greater than 1 and $n\ge 3$, the group ${\mathrm{E}}_n\left(𝐑[X,X^{-1}]\right)$ acts transitively on ${\mathrm{Um}}_n\left(𝐑[X,X^{-1}]\right)$. In particular, we obtain that for any ring $𝐑$ with Krull dimension not greater than 1, all finitely generated stably free modules over $𝐑[X,X^{-1}]$ are free. All the obtained results are proved constructively.