Nonstandard Models for a Fragment of the Arithmetic and Their Decision Problem

M := {X I x E Z[[U]], z 2 o} , where 2 is the antilexicographical ordering in which the indeterminate u becomes infinitely small. (The variable x here also denotes elements of the model); the opera. tions +, are interpreted by the usual operations of addition and multiplication in z[[u]], sx and px are interpreted as x + 1 and x 1 respectively, o is the zero power series, and the operation x A y is defined by [r-y if x z y , otherwise. x’y=