Matrix-Interpretationen (für SRS) als wfmA

• Universum: $\mathbb {N}$^d (Spaltenvektoren) mit x_d≥1

  Ordnung: x > y$\iff$x₁ > y₁∧$\bigwedge_{{i>1}}^{}$x_i≥y_i

  Interpretation [c](x) = M_c⋅x für Matrix M_c∈$\mathbb {N}$^d×d

• [a](x) = $\begin{pmatrix}1 & 1 & 0\\ 0 & 0 & 1\\ 0 & 0 & 1 \end{pmatrix}$⋅x,    [b](x) = $\begin{pmatrix}1 & 0 & 0\\ 0 & 0 & 0\\ 0 & 0 & 1 \end{pmatrix}$⋅x
• das Verifikation-Problem: ist Algebra? wohlfundiert? monoton? kompatibel mit aa→aba?
  • für dieses Beispiel,
  • allgemein (wie beweist man SN(a²b²→b³a³))?