avewright/proofwiki-math huggingface dataset:
Theorem: Set Operations on Primitive Recursive Relations

Let $\RR_1 \subseteq N^k$ and $\RR_2 \subseteq N^k$ be $k$-ary relations on $N^k$.
Let $\RR_1$ and $\RR_2$ be primitive recursive.
Then the following are all primitive recursive relations:
:$\TT = \neg \RR_1$
:$\UU = \RR_1 \land \RR_2$
:$\VV = \RR_1 \lor \RR_2$

Proof:
By hypothesis, the characteristic functions $\chi_{\RR_1}, \chi_{\RR_2}$ of $\RR_1$ and $\RR_2$ are primitive recursive.
Then we have that the characteristic functions of $\TT, \UU, \VV$ are given by:
:$\chi_\TT = \map {\overline \sgn} {\chi_{\RR_1} }$
:$\chi_\UU = \chi_{\RR_1} \times \chi_{\RR_2}$
:$\chi_\VV = \map {\overline \sgn} {\chi_{\RR_1} + \chi_{\RR_2} }$
Compare Complement of Primitive Recursive Set, Intersection of Primitive Recursive Sets and Union of Primitive Recursive Sets.
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
bd7vwbs8dpjuo048h17gt4t8szki81l
Theorem: Ordering Relations are Primitive Recursive

The ordering relations on $\N^2$:
* $n < m$
* $n \le m$
* $n \ge m$
* $n > m$
are all primitive recursive.

Proof:
We note that:
: $n < m \iff m \mathop{\dot -} n > 0$
: $n \ge m \iff m \mathop{\dot -} n = 0$
So it can be seen that the characteristic function of $<$ is given by:
:$\map {\chi_<} {n, m} = \map \sgn {m \mathop{\dot -} n}$
So $\chi_<$ is defined by substitution from the signum and the partial subtraction.
From Signum Function is Primitive Recursive and Cut-Off Subtraction is Primitive Recursive, $\chi_<$ is primitive recursive.
So $<$ is a primitive recursive relation.
Next we see that $n \le m \iff n < m \lor n = m$ from the definition of strictly precedes.
From Equality Relation is Primitive Recursive, we have that $=$ is primitive recursive.
From above, we have that $<$ is primitive recursive.
Thus $\le$ is primitive recursive from Set Operations on Primitive Recursive Relations.
We could use the same reasoning for $>$ and $\ge$ but there's a different approach.
Note that $n \le m \iff n \not > m$, and so $>$ is primitive recursive from Set Operations on Primitive Recursive Relations.
Finally, {{mutatis}}, the same applies to $\ge$.
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
39xevqxattezb7fbgup32hm29ilu0fj
Theorem: Permutation of Variables of Primitive Recursive Function

Let $f: \N^k \to \N$ be a primitive recursive function.
Let $\sigma$ be a permutation of $\set {1, 2, \ldots, k}$.
Then the function $h: \N^k \to \N$ defined as:
:$\map h {n_1, n_2, \ldots, n_k} = \map f {n_{\map \sigma 1}, n_{\map \sigma 2}, \ldots, n_{\map \sigma k} }$
is also primitive recursive.

Proof:
We have that:
:$\forall j \in \set {1, 2, \ldots, k}: n_{\map \sigma j} = \pr^k_{\map \sigma j}$.
Thus $h$ is obtained by substitution from $f$ and the projection functions $\pr^k_{\map \sigma j}$.
The result follows.
{{qed}}
It follows that if a function $h$ can be obtained from known primitive recursive functions by primitive recursion where a variable other than the last one is taken as the recursion variable, then $h$ is primitive recursive.
Category:Primitive Recursive Functions
g05qyre4jhxmyrq61tctfq1k47zr1ce
Theorem: Definition by Cases is Primitive Recursive

Let $\RR_1, \RR_2, \ldots, \RR_k$ be primitive recursive relations on $\N^l$ such that:
:$\forall i, j \in \set{1, 2, \ldots, k}: \RR_i \implies \lnot \RR_j$, that is, all relations are mutually exclusive
:$\forall \tuple {n_1, n_2, \ldots, n_l} \in \N^l: \exists i \in \set {1, 2, \ldots, k}: \map {\RR_i} {n_1, n_2, \ldots, n_l}$, that is, the set of relations is exhaustive.
Let $\forall i \in \set {1, 2, \ldots, k}: g_i: \N^l \to \N$  be primitive recursive functions.
Then the function $f: \N^l \to \N$ defined as:
:<nowiki>$\quad \map f {n_1, n_2, \ldots, n_l} = \begin{cases}
\map {g_1} {n_1, n_2, \ldots, n_l} & : \map {\RR_1} {n_1, n_2, \ldots, n_l} \\
\map {g_2} {n_1, n_2, \ldots, n_l} & : \map {\RR_2} {n_1, n_2, \ldots, n_l} \\
\quad \vdots & \quad \vdots \\
\map {g_k} {n_1, n_2, \ldots, n_l} & : \map {\RR_k} {n_1, n_2, \ldots, n_l}
\end{cases}$</nowiki>
is primitive recursive.

Proof:
We have:
{{begin-eqn}}     
{{eqn | l = \map f {n_1, n_2, \ldots, n_l}
      | r = \map {g_1} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\RR_1} } {n_1, n_2, \ldots, n_l}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \map {g_2} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\RR_2} } {n_1, n_2, \ldots, n_l}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \cdots
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \map {g_k} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\RR_k} } {n_1, n_2, \ldots, n_l}
      | c = 
}}
{{end-eqn}}
because if $\tuple {n_1, n_2, \ldots, n_l} \in \N^k$, there is a unique $r$ such that $\map {\RR_r} {n_1, n_2, \ldots, n_l}$.
Then $\map {\chi_{\RR_r} } {n_1, n_2, \ldots, n_l} = 1$ and $\map {\chi_{\RR_s} } {n_1, n_2, \ldots, n_l} = 0$ for $s \ne r$.
Then the value of the {{RHS}} is $\map {g_r} {n_1, n_2, \ldots, n_l}$ as required.
Since $\RR_1, \RR_2, \ldots, \RR_k$ are primitive recursive, the functions $\chi_{\RR_1}, \chi_{\RR_2}, \ldots, \chi_{\RR_k}$ are primitive recursive as well.
Hence $f$ is obtained by substitution from:
:the primitive recursive function $\Add$
:the primitive recursive functions $g_j$
:the primitive recursive functions $\chi_{\RR_j}$.
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
Category:Definition by Cases is Primitive Recursive
o4o1f5j1re5iuxsyxbb1bv1c21gotw8
Theorem: Factorial is Primitive Recursive

The factorial function $\operatorname{fac}: \N \to \N$ defined as:
:$\map {\operatorname{fac} } n = n!$
is primitive recursive.

Proof:
From the definition of the factorial, we have that:
:$\map {\operatorname{fac} } n = \begin{cases}
1 & : n = 0 \\
\map {\operatorname{mult} } {n, \map {\operatorname{fac} } {n - 1} } & : n > 0
\end{cases}$
Thus $\operatorname{fac}$ is obtained by primitive recursion from the constant $1$ and the primitive recursive function $\operatorname{mult}$.
Hence $\operatorname{fac}$ is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
5lwp9agm6j8uoegyid0nmhda8kwewr9
Theorem: Domain of Injection to Countable Set is Countable

Let $X$ be a set, and let $Y$ be a countable set.
Let $f: X \to Y$ be an injection.
Then $X$ is also countable.

Proof:
Since $Y$ is countable, there exists an injection $g: Y \to \N$.
From Composite of Injections is Injection, $g \circ f: X \to \N$ is also an injection.
That is, $X$ is countable.
{{qed}}
Category:Injections
Category:Countable Sets
s54rmrwnmbz2900fs883itl41t5hk5a
Theorem: Unique Code for URM Instruction

Each basic instruction $I$ in a URM Program can be identified with a unique '''code number''' $\beta \left({I}\right)$.
We also define the following sets:
* $\operatorname{Zinstr}$ is the set of codes of all the <tt>Zero</tt> instructions
* $\operatorname{Sinstr}$ is the set of codes of all the <tt>Successor</tt> instructions
* $\operatorname{Cinstr}$ is the set of codes of all the <tt>Copy</tt> instructions
* $\operatorname{Jinstr}$ is the set of codes of all the <tt>Jump</tt> instructions.
Then we define $\operatorname{Instr}$ to be the set of codes of all basic URM instructions.
That is:
:$\operatorname{Instr} = \operatorname{Zinstr} \cup \operatorname{Sinstr} \cup \operatorname{Cinstr} \cup \operatorname{Jinstr}$.

Proof:
Each basic URM instruction is of one of the following forms:
{| border="1"
|-
| <tt>Zero</tt> 
| $Z \left({n}\right)$
|-
| <tt>Successor</tt> 
| $S \left({n}\right)$
|-
| <tt>Copy</tt> 
| $C \left({m, n}\right)$
|-
| <tt>Jump</tt> 
| $J \left({m, n, q}\right)$
|}
Let $\Bbb I$ be the set of all basic URM instructions.
We define the mapping $\beta: \Bbb I \to \N$ as follows:
* $\beta \left({Z \left({n}\right)}\right) = 6 n - 3$
* $\beta \left({S \left({n}\right)}\right) = 6 n$
* $\beta \left({C \left({m, n}\right)}\right) = 2^m 3^n + 1$
* $\beta \left({J \left({m, n, q}\right)}\right) = 2^m 3^n 5^q + 2$
We note that:
* $\beta \left({Z \left({n}\right)}\right) \equiv 3 \pmod 6$
* $\beta \left({S \left({n}\right)}\right) \equiv 0 \pmod 6$
* $\beta \left({C \left({m, n}\right)}\right) \equiv 1 \pmod 3$
* $\beta \left({J \left({m, n, q}\right)}\right) \equiv 2 \pmod 3$
So, if $\beta \left({I_1}\right) = \beta \left({I_2}\right)$, then both instructions must be of the same type.
Hence it follows from the Fundamental Theorem of Arithmetic that $\beta$ is uniquely specified for any given basic URM instruction.
Thus $\beta$ is an injection.
{{qed}}
Theorem: URM Instructions are Countably Infinite

The set $\Bbb I$ of all basic URM instructions is countably infinite.

Proof:
We can immediately see that $\Bbb I$ is infinite as, for example, $\phi: \N \to \Bbb I$ defined as:
:$\phi \left({n}\right) = Z \left({n}\right)$
is definitely injective.
From Unique Code for URM Instruction, we see that $\beta: \Bbb I \to \N$ is also an injection.
The result follows from Domain of Injection to Countable Set is Countable.
{{qed}}
Category:URM Programs
Category:Countable Sets
n69gjs30q6i5j68nxtq7ihj5mlfxb16
Theorem: URM Programs are Countably Infinite

The set $\mathbf P$ of all URM programs is countably infinite.

Proof:
We can immediately see that $\mathbf P$ is infinite as the number of URM instructions is infinite.
From Unique Code for URM Program, we see that $\gamma: \mathbf P \to \N$ is also an injection.
The result follows from Domain of Injection to Countable Set is Countable.
{{qed}}
Category:URM Programs
Category:Countable Sets
tf5zjy0plb8azcrkkhzbnumrur7l5sb
Theorem: Unique Code for URM Program

Any URM program can be assigned a unique '''code number'''.

Proof:
Let $\mathbf P$ be the set of all URM programs.
Let $P \in \mathbf P$ be a URM program with $k$ basic instructions:
{|
|-
! align="right" | Line !!
! align="left" | Command !!
|-
| align="right" | $1$ ||
| align="left" | $I_1$ ||
|-
| align="right" | $2$ ||
| align="left" | $I_2$ ||
|-
| align="right" | $\vdots$ ||
| align="left" | $\vdots$ ||
|-
| align="right" | $k$ ||
| align="left" | $I_k$ ||
|}
We define the mapping $\gamma: \mathbf P \to \N$ as follows:
:$\ds \map \gamma P = \prod_{i \mathop = 1}^k p_i^{\map \beta {I_i} }$
where:
* $p_i$ is the $i$th prime number;
* $\map \beta {I_i}$ is the unique code for instruction $i$.
Hence it follows from the Fundamental Theorem of Arithmetic that $\gamma$ is uniquely specified for any given URM program.
Thus $\gamma$ is an injection.
{{qed}}
For a given $P$, the number $\map \gamma P$ is referred to as the '''code number of $P$'''.
Theorem: URM Computable Functions of One Variable is Countably Infinite

The set $\mathbf U$ of all URM computable functions of $1$ variable is countably infinite.

Proof:
Let $\mathbf U$ be the set of all URM computable functions.
For each $f \in \mathbf U$, let $P_f$ be a URM program which computes $f$.
Such a program is very probably not unique, so in order to be definite about it, we can pick $P_f$ to be the URM program with the smallest code $\gamma \left({P_f}\right)$.
This is possible from the Well-Ordering Principle.
Let us define the function $h: \mathbf U \to \N$ as:
:$h \left({f}\right) = \gamma \left({P_f}\right)$
Since the same URM program can not compute two different functions of $1$ variable, it can be seen that $h$ is injective.
The result follows from Domain of Injection to Countable Set is Countable.
{{qed}}
Category:URM Programs
Category:Countable Sets
ep1nq4tsj6obs9kfxfnz1ms7j0mzu5u
Theorem: Natural Number Functions are Uncountable

The set of all natural number one-variable functions $\set {f: \N \to \N}$ is uncountably infinite.

Proof:
Let $\Bbb F$ be the set of all functions from $\N$ to $\N$.
Clearly $\Bbb F$ is infinite because it contains for each $k \in \N$ the constant function $f_k: \N \to \N: \map {f_k} n = k$ and these are all different and (trivially) countably infinite in number.
Let $\Phi: \N \to \Bbb F$ be a function.
For each $n \in \N$ let $f_n: \N \to \N$ be the function $\map \Phi n$.
Let us define $g: \N \to \N$ by:
:$\map g n = \map {f_n} n + 1$
Then $g \in \Bbb F$, but $\forall n \in \N$, $\map g n \ne \map {f_n} n$ and so $g \ne f_n$.
Since $g$ is an element of $\Bbb F$ which is different from all the values taken by $\Phi$, it follows that $\Phi$ is not a surjection and hence not a bijection.
Thus no bijection exists between $\Bbb F$ and $\N$ and so $\Bbb F$ is not equivalent to $\N$.
Thus from Countably Infinite Iff Equivalent to Natural Numbers, $\Bbb F$ is uncountable.
{{qed}}
Category:Mapping Theory
Category:Uncountable Sets
jhoc6t2rpej55z9c6nn52t8wuoy9r46
Theorem: Not All Natural Number Functions are Primitive Recursive

Not all functions $f: \N \to \N$ are primitive recursive.

Proof:
All primitive recursive functions are URM computable.
The set of $\mathbf U$ of URM programs is countably infinite.
The set of $\Bbb F$ of natural number functions is uncountably infinite.
Hence there is no surjection from $\mathbf U \to \Bbb F$.
Hence $\mathbf U \subsetneq \Bbb F$.
Hence $\exists f \in \Bbb F: f \notin \mathbf U$.
{{qed}}
Category:Primitive Recursive Functions
0urfc305jilu8erji55syap7v41nfft
Theorem: Bounded Summation is Primitive Recursive

Let the function $f: \N^{k + 1} \to \N$ be primitive recursive.
Then so is the function $g: \N^{k + 1} \to \N$ defined as:
:<nowiki>$\ds \map g {n_1, n_2, \ldots, n_k, z} = \begin{cases}
0 & : z = 0 \\
\ds \sum_{y \mathop = 1}^z \map f {n_1, n_2, \ldots, n_k, y} & : z > 0
\end{cases}$</nowiki>

Proof:
The function $g$ satisfies:
:$\map g {n_1, n_2, \ldots, n_k, 0} = 0$
:$\map g {n_1, n_2, \ldots, n_k, z + 1} = \map g {n_1, n_2, \ldots, n_k, z} + \map f {n_1, n_2, \ldots, n_k, z + 1}$.
Hence $g$ is defined by primitive recursion from:
:the primitive recursive function $\Add$
:$f$, which is primitive recursive
:constants, which are primitive recursive.
Hence the result.
{{qed}}
Theorem: Bounded Product is Primitive Recursive

Let the function $f: \N^{k + 1} \to \N$ be primitive recursive.
Then so is the function $g: \N^{k + 1} \to \N$ defined as:
:<nowiki>$\map g {n_1, n_2, \ldots, n_k, z} = \begin{cases}
1 & : z = 0 \\
\ds \prod_{y \mathop = 1}^z \map f {n_1, n_2, \ldots, n_k, y} & : z > 0
\end{cases}$</nowiki>

Proof:
The function $g$ satisfies:
:$\map g {n_1, n_2, \ldots, n_k, z} = 0$
:$\map g {n_1, n_2, \ldots, n_k, z + 1} = \map g {n_1, n_2, \ldots, n_k, z} \times \map f {n_1, n_2, \ldots, n_k, z + 1}$
Hence $g$ is defined by primitive recursion from:
:the primitive recursive function $\Add$
:$f$, which is primitive recursive
:constants, which are primitive recursive.
Hence the result.
{{qed}}
Theorem: Divisor Relation is Primitive Recursive

The divisor relation $m \divides n$ in $\N^2$ is primitive recursive.

Proof:
We note that $m \divides n \iff n = q m$ where $q \in \Z$.
So we see that $m \divides n \iff \map \rem {n, m} = 0$ (see Remainder is Primitive Recursive).
Thus we define the function $\operatorname{div}: \N^2 \to \N$ as:
:$\map {\operatorname {div} } {n, m} = \map {\chi_{\operatorname {eq} } } {\map \rem {n, m}, 0}$
where $\map {\chi_{\operatorname {eq} } } {n, m}$ denotes the characteristic function of the equality relation.
So we have:
:$\map {\operatorname {div} } {n, y} = \begin{cases}
1 & : y \divides n \\
0 & : y \nmid n
\end{cases}$
So $\map {\operatorname {div} } {n, m}$ is defined by substitution from:
:the primitive recursive function $\rem$
:the primitive recursive relation $\operatorname {eq}$
:the constants $1$ and $0$.
Thus $\operatorname {div}$ is primitive recursive.
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
8wsr1duvmpkzioguxnb1iq0ghwdqwlv
Theorem: Divisor Count Function is Primitive Recursive

The divisor count function is primitive recursive.

Proof:
The divisor count function $\sigma_0: \N \to \N$ is defined as:
:$\ds \map {\sigma_0} n = \sum_{d \mathop \divides n} 1$
where $\ds \sum_{d \mathop \divides n}$ is the sum over all divisors of $n$.
Thus we can define $\map {\sigma_0} n$ as:
:$\ds \map {\sigma_0} n = \sum_{y \mathop = 1}^n \map {\operatorname {div} } {n, y}$
where
:$\map {\operatorname {div} } {n, y} = \begin{cases}
1 & : y \divides n \\
0 & : y \nmid n
\end{cases}$
Hence $\sigma_0$ is defined by substitution from:
:the primitive recursive function $\operatorname {div}$
:the primitive recursive bounded summation $\ds \sum_{y \mathop = 1}^n$.
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
Category:Divisor Count Function
d6aww7zxyr2xt7tfjz995ozj2ot2mg6
Theorem: Set of Prime Numbers is Primitive Recursive

The set $\Bbb P$ of prime numbers is primitive recursive.

Proof:
A prime number is defined as an element of $\N$ with '''exactly two''' positive divisors.
So, we have that $n > 0$ is prime {{iff}} $\map \tau n = 2$, where $\tau: \N \to \N$ is the divisor count function.
Thus we can define the characteristic function of the set of prime numbers $\Bbb P$ as:
:$\forall n > 0: \map {\chi_\Bbb P} n := \map {\chi_{\operatorname {eq} } } {\map \tau n, 2}$
Now we let $g: \N^2 \to \N$ be the function given by:
:$\map g {n, z} = \begin{cases}
0 & : z = 0 \\
\ds \sum_{y \mathop = 1}^z \map {\operatorname {div} } {n, y} & : z > 0
\end{cases}$
As:
:$\operatorname {div}$ is primitive recursive
:$\ds \sum_{y \mathop = 1}^z$ is primitive recursive
it follows that $g$ is primitive recursive.
Then for $n > 0$:
:$\ds \map g {n, n} = \sum_{y \mathop = 1}^n \map {\operatorname {div} } {n, y} = \map \tau n$
and from Divisor Count Function is Primitive Recursive we have that $g$ is primitive recursive.
Then let $h: \N \to \N$ be the function defined as:
:$\map h n = \map g {n, n}$
which is also primitive recursive.
So we have, for all $n \in \N$:
:$\map {\chi_\Bbb P} n = \map {\chi_{\operatorname {eq} } } {\map h n, 2}$
Hence the result.
{{qed}}
Category:Primitive Recursive Functions
bety5xmq55at7yog4d4md3af4caxkla
Theorem: Prime Enumeration Function is Primitive Recursive

Let the function $p: \N \to \N$ be the prime enumeration function, defined as:
:$\map p n = \begin{cases}
1 & : n = 0 \\
\mbox{the } n \mbox{th prime number} & : n > 0
\end{cases}$
Then $p$ is primitive recursive.

Proof:
We can define $p$ recursively by:
:$\map p {n + 1} = \text{the smallest } y \in \N \text { such that } y \text { is prime and } \map p n < y$
Hence we can express it as:
:$\map p {n + 1} = \map {\mu y} {\map {\chi_\Bbb P} y = 1 \land \map p n < y}$
where:
* $\map {\chi_\Bbb P} y$ is the characteristic function of the set of prime numbers $\Bbb P$
* $\map {\mu y} \RR$ means '''the smallest $y \in \N$ such that the relation $\RR$ holds'''.
Now consider the relation $\SS$ given by:
:$\map \SS {m, y} \iff \map {\chi_\Bbb P} y = 1$.
We have a reason for making $\SS$ a binary relation, even though $m$ is not actually invoked in its definition.
Then we have:
:$\map {\chi_\SS} {m, y} = \map {\chi_{\operatorname{eq} } } {\map {\chi_\Bbb P} y, 1}$.
So $\chi_\SS$ is primitive recursive as it is obtained by substitution from:
* the primitive recursive function $\chi_{\operatorname{eq} }$
* the primitive recursive function $\chi_\Bbb P$.
Then we have that $<$ is primitive recursive.
So we define the relation $\RR$ by:
:$\map \RR {m, y} \iff \map \SS {m, y} \land m < y \iff \map {\chi_\Bbb P} y = 1 \land m < y$.
This is primitive recursive from the above and Set Operations on Primitive Recursive Relations.
Now let us define the function $g: \N^2 \to \N$ as:
:$\map g {m, z} = \mu y \le \map z {\map {\chi_\Bbb P} y = 1 \land m < y}$
which is primitive recursive by Bounded Minimization is Primitive Recursive.
We note that $\map g {\map p n, z} = \map p {n + 1}$ as long as $\map p {n + 1} \le z$.
Next, let $h: \N \to \N$ be defined as $\map h n = \map \exp {2, \map \exp {2, n} }$.
Then $h$ is primitive recursive since it is obtained by substitution from:
* the primitive recursive function $\exp$;
* the constant $2$.
From Upper Bounds for Prime Numbers, we have $\map p {n + 1} \le 2^{2^n} = \map h n$.
It follows that:
:$\map p {n + 1} = \map g {\map p n, \map h n}$
where $g$ and $h$ are both primitive recursive.
So using the definition of $p$ as given above, we have:
:$\map p 0 = 1$
:$\map p {n + 1} = \map g {\map p n, \map h n}$.
So $p$ is defined by primitive recursion from the constant $1$ and the primitive recursive functions $g$ and $h$.
{{qed}}
Theorem: Length Function is Primitive Recursive

Let $n \in \N$.
Let $\map \len n$ denote the length of $n$.
Then the function $\len: \N \to \N$ is primitive recursive.

Proof:
Clearly $\map \len 0 = 0$.
For $n > 0$, we have:
:$\ds \map \len n = \sum_{y \mathop = 1}^n \map {\operatorname {div} } {n, \map p y}$
where:
:$\map {\operatorname {div} } {n, m}$ is defined as:
::$\map {\operatorname {div} } {n, y} = \begin{cases}
1 & : y \divides n \\
0 & : y \nmid n
\end{cases}$
:$\map p y$ is the $y$th prime number.
Let $g: \N^2 \to \N$ be the function defined by:
:$\ds \map g {n, z} = \begin{cases}
0 & : z = 0 \\
\ds \sum_{y \mathop = 1}^z \map {\operatorname {div} } {n, \map p y} & : z > 0
\end{cases}$
We have that:
:$\operatorname{div}$ is primitive recursive
:$p: \N \to \N$ is primitive recursive
:Bounded Summation is Primitive Recursive.
So it follows that $g$ is also primitive recursive.
Finally, as $\map \len n = \map g {n, n}$ it follows that $\len$ is primitive recursive.
{{qed}}
Category:Primitive Recursive Functions
p1l9foh4qqn9vz1268dkgpkjwpu1j5q
Theorem: Prime Exponent Function is Primitive Recursive

Let $n \in \N$ be a natural number.
Let $\tuple {n, j}: \N^2 \to \N$ be defined as:
:$\tuple {n, j} = \paren n_j$
where $\paren n_j$ is the prime exponent function.
Then $\tuple {n, j}$ is primitive recursive.

Proof:
Let $\map p j$ be the prime enumeration function.
For $n \ne 0$ and $j \ne 0$, we see that $\paren n_j$ is the largest value of $k$ for which $\map p j^k$ is a divisor of $n$.
Thus $\paren n_j$ is the ''smallest'' value of $k$ for which $\map p j^{k + 1}$ is ''not'' a divisor of $n$.
We note that if $r \ge n$ and $j \ne 0$, we have $\map p j^r \ge 2^r \ge 2^n > n$.
Thus $n$ is a (generous) upper bound of $\paren n_j$.
The condition that $\map p j^{k + 1}$ is not a divisor of $n$ can be expressed as:
:$\map {\operatorname{div} } {n, \map p j^{k + 1} } = 0$
where:
:$\operatorname{div}$ is primitive recursive
:The Equality Relation is Primitive Recursive
:$\map p j$ is primitive recursive
:Exponentiation is Primitive Recursive
:Addition is Primitive Recursive.
So we see that the relation:
:$\map \RR {n, j, k} \iff \map {\operatorname{div} } {n, \map p j^{k + 1} } = 0$
is primitive recursive.
From Bounded Minimization is Primitive Recursive, we also see that:
:$\paren n_j = \begin{cases}
\mu k \le n \map \RR {n, j, k} & : n \ne 0 \land j \ne 0 \\
0 & : \text{otherwise}
\end{cases}$
is primitive recursive.
The result follows.
{{qed}}
Category:Primitive Recursive Functions
kb3zmgn11ujf9uy9km9ivw8calqjifb