AbstractDataType - Nat

Question

I got this abstract model here and try to understand how it works but can't figure it out.

type: NAT

constructor

null: → NAT 
succ: NAT → NAT 

operator

add: NAT×NAT→ NAT

axiom x,y : NAT

add(X, null) = X
add(X, succ(Y)) = succ(add(X, Y))

The problem is with the add. I tried to put some numbers in but ... how does it work? -

add(2, succ(3)) = succ(add(2, 3)) ... and now? I just want 2+3 = 5

Answer 1

NAT is the set of natural numbers together with '+' and succ is the successor function (often seen in relation with the Peano axioms)

Your example for 2+3 calculates like this:

add(2,3) = succ(add(2,2))
         = succ(succ(add(2,1))) 
         = succ(succ(succ(add(2,0))))
         = succ(succ(succ(2)))
         = succ(succ(3))
         = succ(4)
         = 5