consider the natural numbers defined by the following BNF
m,n::=Z｜S(n)
and the function add defined inductively as follows:
add(Z,m)= m
add(S(n),m)=S(add(n,m))
(1)compute add(S(S(Z)),S(Z));
(2)prove that Z is the left unit of add, i.e., add(n,Z)=n for all natural numbers n;
(3)prove by induction that Z is the right unit of add, i.e., add(Z,n)=n for all natural numbers n;
(4)prove by induction that add(n,S(m))=S(add(n,m)) for all natural numbers n and m;
(5)prove by induction that add is associative.

有些名词我不知道怎么翻译，就是先根据BNF范式定义了自然数（第一个式子），之后又定义了一个应用add,第一问就是计算add(),第二问是求证明Z是add的左单元（left unit）即，对于所有自然数n有add(Z,n)=n；第三问是求归纳证明Z是add的右单元（right unit）即，对于所有自然数n有add(n,Z)=n；第四问是对于所有自然数n和m有那个式子成立。第五问是归纳证明add是关联的（associative）.