Decidability questions for a ring of Laurent polynomials

We prove that the additive structure of the ring of Laurent polynomials augmented by the predicate symbol PP, where P(x)P(x) if and only if xx is a power of tt, is decidable. We also prove that the first-order theory of the previous structure together with the relation ∣t∣t, where x∣tyx∣ty if and only if ∃s∈Zy=x⋅ts, is undecidable.

► We study the additive structure of the ring of Laurent polynomials, say AA.
► We show decidability of first-order theory of AA augmented by relation for powers of tt.
► We study the previous structure together with a weak form of divisibility, say BB.
► We prove that the first-order theory of BB is undecidable.