为什么以下是自然数的正确实现?
mod PEANO-NAT is
sort Nat .
op zero : -> Nat .
op succ : Nat -> Nat .
op plus : Nat Nat -> Nat .
vars N M : Nat .
eq plus(zero, M) = M .
eq plus(succ(N), M) = succ(plus(N, M)) .
endm
特别是我很难理解最后两行以及它们如何确保正确定义自然数。任何帮助