⁴This theory is the same as that of linear arithmetic with rational coefficients for the real numbers. That is, for the algebra $(ℝ,Q,+,>,\ge )$. The key observation is that any system of linear equations with rational coefficients has a solution in the real numbers if and only if it has a solution in the rational numbers. The real numbers are relevant only in the case of non-linear equations not supported here. Therefore, in what follows we will not make any distinction between these two identical linear arithmetic theories and will just talk about “linear arithmetic on the rationals.” Likewise, the theory’s main sort can be called either Rat or Real, since this makes no difference. Actually, we will use Real to avoid confusion with the already existing sort Rat in the RAT module.