We develop an elimination theory for addition and the Frobenius map over rings of polynomials. As a consequence we show that if F is a countable, recursive and perfect field of positive characteristic p, with decidable theory, then the structure of addition, the Frobenius map x→ xp and the property ‘x∈ F', over the ring of polynomials F[T], has a decidable theory.