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