We can inductively define familiar operations like addition and
multiplication.
There are several alternatives: we could induct on the second argument, on
the first argument, or on both arguments:
Let
[math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ}
[/math] be
given inductively by
[math]add(x,Z) := x
[/math] and
[math]add(x,S~n) := S~add(x,n)
[/math].
Let
[math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ}
[/math] be given
inductively by
[math]add(Z,x) := x
[/math] and
[math]add(S~n,x) := S~add(n,x)
[/math].
Let
[math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ}
[/math] be given
inductively by
[math]add(Z,Z) := Z
[/math],
[math]add(Z,S~n) := S~n
[/math],
[math]add(S~n,Z) := S~n
[/math], and
[math]add(S~n,S~m) := S~S~add(n,m)
[/math].
