structural:expansion, information:extraction
Truncated subtraction

The limited subtraction function (also called " monus ", and denoted " −. {\displaystyle {\stackrel {.}{-}}} ") is definable from the predecessor function. It satisfies the equations

Since the recursion runs over the second argument, we begin with a primitive recursive definition of the reversed subtraction, R S u b (y, x) = x −. y {\displaystyle RSub(y,x)=x{\stackrel {.}{-}}y}. Its recursion then runs over the first argument, so its primitive recursive definition can be obtained, similar to addition, as R S u b = ρ (P 1 1, P r e d ∘ P 2 3) {\displaystyle RSub=\rho (P_{1}^{1},Pred\circ P_{2}^{3})}. To get rid of the reversed argument order, then define S u b = R S u b ∘ (P 2 2, P 1 2) {\displaystyle Sub=RSub\circ (P_{2}^{2},P_{1}^{2})}. As a computation example,