What corresponds to $\forall m\forall n(2m \neq 2n+1)$ or $\forall p\forall q(p^2 \neq 2q^2)$ in the monadic theory of the real line?

[Shelah (1975)][1] proved that arithmetic can be reduced the monadic theory of the real line. The paper gives a procedure to input a sentence of first-order arithmetic, and then output a sentence with the same truth value in the structure $\{\mathcal{P}(\mathbf{R}), \subset, <\}$, where $<$ is a version of the order that applies to singleton sets. But the procedure does not do this via an interpretation of one theory in the other.

What does this procedure give for simple sentences?

The procedure is on pp. 415-416 of Shelah's paper, but I can't make sense of it. Gurevich (1985), as linked to [here][2], gave a similar procedure interpreting arithmetic in the monadic second-order theory of the Cantor set, but I can't make sense of that either. What do these procedures do with addition and multiplication? I'm hoping that someone with more experience or skill reading Shelah can clarify.

*To clarify:* The algorithm (or perhaps, partially-described algorithm) would begin with these statements in the equivalent relational forms $$\forall m,n,u,v (\neg Smmu \vee \neg Snnv \vee \neg S1uv)$$ $$\forall m,n,u,v (\neg Pmmu \vee \neg Pnnv \vee \neg P2uv)$$ where $S$ and $P$ are symbols for the relations of sum and product. It remains unclear what the algorithm does with $S$ and $P$, or indeed how the algorithm treats these two sentences differently at all.

  [1]: https://www.jstor.org/stable/1971037?seq=1#page_scan_tab_contents
  [2]: https://mathoverflow.net/questions/332867/monadic-second-order-theories-of-the-reals