Kleene's normal form theorem for arithmetical petri nets

This paper gives a proof of the normal form theorem for arithmetical Petri nets (APN). The normal form theorem was introduced by Kleene for the general recursive computation paradigm in terms of system of equations. APN are inhibitor Petri nets that perform three types of arithmetical operations; increment, decrement and test for zero. The proof is based on the idea of computation tree, where each node of such a tree will tell us how a value needed for the arithmetical operations can be inductively obtained. Then, using arithmetization plus course of value recursion a primitive recursive predicate is defined from which by means of a primitive recursive function the desired characterization for the value of the output function is established.