General Recursive Function: Difference between revisions

Latest revision as of 17:25, 6 October 2026

General recursive functions (GRFs), also called µ-recursive functions or partial recursive functions, are the collection of partial functions $ℕ^{k} ⇀ ℕ$ that are computable. This definition is equivalent using any Turing complete system of computation. See Wikipedia:general recursive function for background.

Historically it was defined as the smallest class of partial functions $ℕ^{k} ⇀ ℕ$ that is closed under composition, recursion, and minimization, and includes zero, successor, and all projections (see formal definitions below). In the rest of this article, this is the formulation that we focus on exclusively. In this way, it can be considered to be a Turing complete model of computation. In fact, it is one of the oldest Turing complete models, first formalized by Kurt Gödel and Jacques Herbrand in 1933, 3 years before λ-calculus and Turing machines.

BBµ(n) is a Busy Beaver function for GRFs: $B B μ (n) = \max {f () | f \in {GRF}_{0}, | f | = n}$

where $f \in G R F_{k}$ means that $f : ℕ^{k} ⇀ ℕ$ is a k-ary GRF and $| f |$ is the "structural size" of f (the number of atoms and combinators in the definition, see details below). In other words, it is the largest number computable via a 0-ary function (a constant) with a limited "program" size. It is more akin to the traditional Sigma score for a Turing machine rather than the Step function in the sense that it maximizes over the produced value, not the number of steps needed to reach that value.

Definition

Structure

Define $G R F_{k}$ inductively based on the following construction rules, start with Atoms and combine them using Combinators.

Atoms

Zero: $\forall k \in ℕ, Z^{k} \in G R F_{k}$ is the constant 0 function $Z^{k} (x_{1}, \dots, x_{k}) = 0$
Successor: $S \in G R F_{1}$ is the successor function $S (x) = x + 1$
Projection: $\forall 1 \leq i \leq k \in ℕ, P_{i}^{k} \in G R F_{k}$ is a projection function $P_{i}^{k} (x_{1}, \dots x_{k}) = x_{i}$

Combinators

Composition: $\forall k, m \in ℕ, \forall h \in G R F_{m}, \forall g_{1}, \dots g_{m} \in G R F_{k}, C^{k} (h, g_{1}, \dots g_{m}) \in G R F_{k}$ is the composition or substitution of the gs into h: $C^{k} (h, g_{1}, \dots g_{m}) (x_{1}, \dots x_{k}) = h (g_{1} (x_{1}, \dots x_{k}), \dots g_{m} (x_{1}, \dots x_{k}))$
Primitive Recursion: $\forall k \in ℕ, \forall g \in G R F_{k}, \forall h \in G R F_{k + 2}, R^{k + 1} (g, h) \in G R F_{k + 1}$ is primitive recursion using g as the base case and h as the inductive step.
Minimization / Unlimited Search: $\forall k \in ℕ, \forall f \in G R F_{k + 1}, M^{k} (f) \in G R F_{k}$ is the µ-operator which allows unlimited search.

The arity superscripts for C, R and M are redundant (except for $C^{k} (h)$ ) and so are sometimes omitted below.

Size

The size of a GRF is the number of atoms and combinators in the definition:

$| Z^{k} | = | P_{i}^{k} | = | S | = 1$
$| C (h, g_{1}, \dots, g_{m}) | = 1 + | h | + | g_{1} | + \dots + | g_{m} |$
$| R (g, h) | = 1 + | g | + | h |$
$| M (f) | = 1 + | f |$

Primitive Recursion

$R$ models a typical iterative function definition over ℕ.

Base case: $R^{k} (g, h) (0, x_{2}, x_{3}, . . ., x_{k}) = g (x_{2}, x_{3}, . . ., x_{k})$

Iterative case (for $x_{1} > 0$ ): $R^{k} (g, h) (x_{1}, x_{2}, . . ., x_{k}) = h (x_{1} - 1, v, x_{2}, x_{3}, . . ., x_{k})$ where $v = R (g, h) (x_{1} - 1, x_{2}, x_{3}, . . ., x_{k})$ .

R can be recursively evaluated following its definition directly or it can be simulated as a bounded for loop like this python code:

# f = R(g,h)
def f(n, *xs):
  acc = g(*xs)
  for k in range(n):
    acc = h(k, acc, *xs)
  return acc

The iterative function h is passed two synthetic args in the front: (k) iteration number (0-indexed) and (acc) "accumulator" from previous iterations.

Both the base and iterative cases can be parameterized by values $x_{2}, x_{3}, . . ., x_{k}$ .

If you restrict functions to only those constructible with Z, S, P, C, R (no M) then this defines the Primitive Recursive Functions, a subset of the General Recursive Functions that always halt.

Minimization

$M^{k} (f) (x_{1}, . . ., x_{k}) ≜ \min {i \in ℕ : f (i, x_{1}, . . ., x_{k}) = 0}$

In computational language, when M(f) is evaluated it can be considered to calculate $f (i, x_{1}, . . ., x_{k})$ with $i = 0$ , then $i = 1$ , then $i = 2$ etc. until one of the calls to $f$ returns 0, at which point it returns the value of $i$ which first gave a result of 0. If no first argument causes $f$ to return 0, $M (f)$ doesn't return (this is the only way for a GRF to not halt).

Macros

In order to improve readability we define the following macros. For all $f \in G R F_{2}, g \in G R F_{1}$


	Macro	arity	Definition	Size	Function
Constant	$K^{k} [n]$	k	$\begin{array}{lcl} K^{k} [0] & : = & Z^{k} \\ K^{k} [n] & : = & C (P l u s [n], Z^{k}) \end{array}$	$2 n + 1$	$λ x_{1} \dots x_{k} . n$
Plus constant	$P l u s [n]$	1	$\begin{array}{lcl} P l u s [1] & : = & S \\ P l u s [n + 1] & : = & C (S, P l u s [n]) \end{array}$	$2 n - 1$	$λ x . x + n$
Addition	Add	2	$A d d : = R (P_{1}^{1}, C (S, P_{2}^{3}))$	5	$λ x y . x + y$
Triangular numbers	$T r i$	1	$T r i : = R (Z^{0}, R (S, C (S, P_{2}^{3})))$	7	$λ x . \frac{x (x + 1)}{2}$
Iteration	$R e p S u c c [g]$	2	$R e p S u c c [g] : = R (S, C (g, P_{2}^{3}))$	$\| g \| + 4$	$λ x y . g^{x} (y + 1)$
Iteration on first arg	$R e p F i r s t [f]$	2	$R e p F i r s t [f] : = R^{2} (S, R^{3} (f, P_{2}^{4}))$	$\| f \| + 4$	$λ x y . (λ z . f (z, y))^{x} (y + 1)$
Diagonalization & Iteration	$D i a g R e p [f]$	2	$D i a g R e p [f] : = R (S, C (f, P_{2}^{3}, P_{2}^{3}))$	$\| f \| + 5$	$λ x y . (λ z . f (z, z))^{x} (y + 1)$
Diagonalization	$D i a g S [f]$	1	$D i a g S [f] : = C (f, S, S)$	$\| f \| + 3$	$λ x . f (x + 1, x + 1)$
Ackermann iteration	$A c k D i a g 2 [n, f]$	2	$\begin{array}{lcl} A c k D i a g 2 [0, f] & : = & R e p S u c c [f] \\ A c k D i a g 2 [n + 1, f] & : = & D i a g R e p [A c k D i a g 2 [n, f]] \end{array}$	$5 n + 4 + \| f \|$
Ackermann iteration	$A c k D i a g [n, f]$	1	$A c k D i a g [n, f] : = D i a g S [A c k D i a g 2 [n, f]]$	$5 n + 7 + \| f \|$

Champions

We divide the champions tables up by enumeration categories. Starting from the simplest functions and moving to the most general.

Composition Functions

The simplest category are PRFs without Recursion. In other words, only atoms and Composition. All composition functions are equivalent to either $P l u s [n]$ , $C (P l u s [n], P_{i}^{k})$ or $K^{k} [n] = C (P l u s [n], Z^{k})$ . For BBµ, the only options are $K^{0} [n]$ which is size 2n+1. These can be trivially extended to $C^{0} (K^{0} [n])$ of size 2n+2. So this proves that $B B μ (2 n + 1), B B μ (2 n + 2) \geq n$ . These are the best known champions up to size 13.

Primitive Recursive Functions

We get considerably more complexity by allowing all Primitive Recursive Functions (PRFs). But PRFs are still all guaranteed to be total, are decidable and are all dominated by Ackermann growth functions. They are convenient to enumerate since none diverge, so any holdouts that remain when running limited computations must eventually halt. All PRF champions up to size 13 are simple composition functions as mentioned above. PRFs with R begin at size 14.

The size 21-24 PRF champions are also currently full GRF champions, although it seems likely that M(PRF) will surpass these values, it just hasn't been run out that far yet.

n	Max Score	Champions	Champion Found	# Holdouts
13	= 6	`K[6]`		0
14	= 7	`C(DiagS[RepSucc[S]], K[2])` `C(DiagS[RepSucc[Plus[2]]], K[1])`	Shawn Ligocki 10 Apr 2026	0
15	= 7	`K[7]`		0
16	= 10	`C(DiagS[RepSucc[Plus[2]]], K[2])`	Shawn Ligocki 11 Apr 2026	0
17	= 15	`C(DiagS[DiagRep[RepSucc[S]]], K[1])`	Shawn Ligocki 12 Apr 2026	0
18	= 21	`C(DiagS[RepSucc[Tri]], K[1])` `C(DiagS[RepFirst[RepSucc[Plus[2]]]], K[1])`	Jacob Mandelson 9 Apr 2026	0
19	= 39	`C(DiagS[DiagRep[RepSucc[S]]], K[2])`	Shawn Ligocki 12 Apr 2026	0
20	= 1540	`C(DiagS[RepSucc[Tri]], K[2])`	Jacob Mandelson 9 Apr 2026	0
21	= 8,589,934,591	`C(DiagS[RepFirst[DiagRep[RepSucc[S]]]], K[1])`	Shawn Ligocki 16 May 2026	0
22	$\approx 1 0^{1 0^{69}}$	`C(DiagS[RepFirst[RepSucc[Tri]]], K[1])`	Shawn Ligocki 17 May 2026	Deciders: 11 All decided by hand
23	$> 1 0^{1 0^{463}}$	`C(DiagS[DiagRep[RepSucc[Tri]]],K[1])`	Shawn Ligocki 24 Jun 2026	129
24	$> 2^{2^{2^{2^{2^{20}}}}}$	`C(DiagS[RepFirst[RepSucc[Tri]]], K[2])`	Shawn Ligocki 17 May 2026	Not yet enumerated

M(PRF)

We get another level of complexity by allowing Minimization, but only at the very top level. In other words, all of these GRF are M(f) for some PRF f. We call this M(PRF) or min_prf. This is a convenient set to explore because (1) it is Turing complete, (2) it is a smaller domain and easier to enumerate than full GRF, (3) all small known champions are of this form.

All M(PRF) champions up to size 13 are simple composition functions as mentioned above.

n	Max Score	Champions	Champion Found	# Holdouts
12	= 5	`C(K[5])`		0
13	= 6	`K[6]`		Deciders: 15 All proven by hand
14	≥ 32	$M^{0} (C^{1} (R^{2} (P_{1}^{1}, R^{3} (P_{1}^{2}, C^{4} (R^{2} (P_{1}^{1}, P_{1}^{3}), P_{2}^{4}, P_{1}^{4}))), P_{1}^{1}, S))$ $M^{0} (C^{1} (R^{2} (S, R^{3} (P_{1}^{2}, C^{4} (R^{2} (P_{1}^{1}, P_{1}^{3}), P_{2}^{4}, P_{1}^{4}))), P_{1}^{1}, P_{1}^{1}))$	Shawn Ligocki 29 Apr 2026	109
15	≥ 32	C^0(size 14 champ)		589
16	≥ 47	$M (C (R (S, R (P_{1}^{2}, R (P_{2}^{3}, C (R (S, P_{1}^{3}), P_{3}^{5}, P_{2}^{5})))), P_{1}^{1}, S))$	Shawn Ligocki 5 May 2026	3,430
17	≥ 58,471	`M(C(R(P(1,1),R(R(S,R(R(S,R(Z2,P(4,1))),P(4,2))),P(4,2))),S,P(1,1)))`	Shawn Ligocki 29 Jun 2026	19,862
18				93,738
19				1,419,487
20				7,508,624

Full GRF

The final level is full GRF where Minimization is allowed at any level. The only champions currently at this level are hand-constructed GRF designed to surpass Graham's number.

n	BBµ(n)	Champion	Champion Found
93	$> f_{ω + 1} (f_{ω} (2 ↑ ↑ ↑ 2 ↑ ↑ ↑ 6)) ≫ Graham's number$	Graham() from goodstein.mgrf	Racheline and Shawn Ligocki 19 May 2026
...
98	$> f_{ω}^{f_{ω}^{3} (3)} (3) ≫ Graham's number$	Graham() from ack_worm.mgrf	Shawn Ligocki 17 May 2026

Analysis of Champions

BBµ(14) ≥ 32

This is the smallest non-trivial champion:

Expression: M(C(R(P(1,1), R(P(2,1), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S))
Arity: 0 | Size: 14 | GRF

=== Sub-expressions ===

a := R(P(1,1), P(3,1))    [arity 2, size 3, PRF, used={1,2}]
  a(0, y) = y
  a(x, _) = x-1

b := R(P(2,1), C(a, P(4,2), P(4,1)))    [arity 3, size 8, PRF, used={1,2}]
    if 0 ≤ x ≤ y: b(x,y) = y-x
    if y+1 ≤ x ≤ 2y+1: b(x,y) = 2y+1-x
  b(x, y) = (y+1) 2^k - 1 - x  (where k is minimal such that this is ≥ 0)

c := R(P(1,1), b)    [arity 2, size 10, PRF, used={1,2}]
  def c(x, y):
    acc = y
    for i in range(x):
      acc = b(i,acc)
    return acc

=== Root ===
d := M(C(c, P(1,1), S))    [arity 0, size 14]
  def d():
    for n in 0..:
      acc = n+1
      for i in range(n):
        while acc < i:
          acc = 2*acc + 1
        acc -= i
      if acc == 0:
        return n
  d() = 32

This GRF subtracts numbers 0 to n-1 from accumulator starting at n+1 with a slightly complex underflow condition (what to do when the number goes negative). It repeats this on increasing n until this process happens to hit exactly 0. It appears to be chaotic. It can be parameterized in a couple of ways by swapping S <-> P(1,1). This parameterization seems to get the luckiest and make it up to n=32 before halting. The other co-champion has the exact same behavior, just by switching when we do S vs P(1,1) for the base case.

Cryptids

So far all Cryptids have been constructed by hand; no GRFs found in the wild have been categorized as Cryptids yet.

Hand Constructed Cryptids
Size	Problem	Authors	Ref
49	Brocard's problem	aparker, star and Shawn 3 May 2026	brocard.mgrf Discord
56	5x+1 trajectory of 7	Shawn Ligocki 2 May 2026	collatz.mgrf
81	Erdős ternary conjecture	Shawn Ligocki 28 Apr 2026	erdos.mgrf
139	Antihydra-like problem	Jacob Mandelson 8 Apr 2026	Orig (size 141) Size 139

There is also a size 133 GRF that searches for counterexamples to Fermat's Last Theorem, halting iff it ever found one (however, since FLT has been proven, this GRF can be shown to be non-terminating, and is therefore not considered a Cryptid): fermat.mgrf

Notable GRF

Unsolved GRFs

Size 16: M(C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S))Discord Discord
- It is known that if this function returns a value, it must be greater than 499 quadrillion. Discord

Solved GRFs

Hardest Size 12

This is subjective of course, but it seems like the hardest size 12 M(PRF) holdout is M(R(C(S, Z0), R(S, R(R(S, P(3,1)), P(4,2))))). Proving it seems requires noticing the pattern that d(x) = x-2 for all x ≥ 3 and proving that it inductively follows that pattern for all future values.^[1]

Expression: M(R(C(S, Z0), R(S, R(R(S, P(3,1)), P(4,2)))))
Arity: 0 | Size: 12 | GRF

=== Sub-expressions ===

a := R(S, P(3,1))    [arity 2, size 3, PRF, used={1,2}]
  a(0, y) = 1 + y
  a(x, _) = x-1

b := R(a, P(4,2))    [arity 3, size 5, PRF, used={1,2,3}]
  b(_, 0, z) = 1 + z
  b(_, y, _) = y-1

c := R(S, b)    [arity 2, size 7, PRF, used={1,2}]
  c(x, y) = (1 + y - x) %< (2 + y)

d := R(C(S, Z0), c)    [arity 1, size 11, PRF, used={1}]
  d(0) = 1
  d(1) = 2
  d(2) = 2
  d(x) = x - 2

=== Root ===
M(d)    [arity 0, size 12]
  = ∞

Hardest Size 13 (Triangular Divisibility)

Likewise, it seems like the hardest size 13 M(PRF) holdout is M(C(R(S, R(P(2,1), R(R(P(2,2), P(4,1)), P(5,2)))), P(1,1), P(1,1))) which halts iff there exists some n ≥ 1 such that n+2 divides $T r i (n) = \frac{n (n + 1)}{2}$ . There is no such n,^[2] therefore this GRF diverges, but this requires reasoning about divisibility and modular arithmetic.

Tetrahedral Divisibility

The GRF $M^{0} (C^{1} (R^{2} (S, R^{3} (P_{1}^{2}, R^{4} (P_{1}^{3}, R^{5} (R^{4} (P_{3}^{3}, P_{1}^{5}), P_{2}^{6})))), S, S))$ (Size 15) halts iff there exists some n ≥ 1 such that n+3 divides $T e t r (n) = \frac{n (n + 1) (n + 2)}{6}$ .^[3] aparker^[4] and star^[5] proved that there is no such n, therefore this GRF diverges.

Chaotic size 15

Expression: M(C(R(P(1,1), R(R(S, P(3,1)), R(R(P(2,2), P(4,1)), P(5,2)))), S, P(1,1)))
Arity: 0 | Size: 15 | GRF

=== Sub-expressions ===

a := R(S, P(3,1))    [arity 2, size 3, PRF, used={1,2}]
  a(0, y) = 1 + y
  a(x, _) = x-1

b := R(P(2,2), P(4,1))    [arity 3, size 3, PRF, used={1,3}]
  b(0, _, z) = z
  b(x, _, _) = x-1

c := R(b, P(5,2))    [arity 4, size 5, PRF, used={1,2,4}]
  c(_, 0, _, w) = w
  c(_, y, _, _) = y-1

d := R(a, c)    [arity 3, size 9, PRF, used={1,2,3}]
  d(x, 0, z) = (1 + z - x) %< (1 + z)
  d(x, y, z) = (y - x - 1) %< (1 + z)

e := R(P(1,1), d)    [arity 2, size 11, PRF, used={1,2}]
M(C(e, S, P(1,1)))    [arity 0, size 15]

(where a %< b is a if a ≥ 0 and a % b if a < 0) Racheline proved this diverges.^[6] The key here is that e(n+1, n) = d(n, y, n) for some y (the last step of the recursion) and for all y d(n, y, n) ≠ 0 since:

d(n, 0, n) = 1
d(n, y+1, n) = y+1

Macro Bounds

Let $C = \frac{1}{\log_{10} (2)} \approx 3.32$

AckDiag[k, S]

Let $A S_{k} (n) : = D i a g R e p^{k} [R e p S u c c [S]] (n, n) = A c k D i a g [k, S] (n - 1)$

$A S_{0} (n) = S^{n} (n + 1) = 2 n + 1$
$A S_{1} (n) = A S_{0}^{n} (n + 1) = (n + 2) 2^{n} - 1$
$A S_{1} (n) > C \cdot 1 0^{n / C}$ (for $n \geq 2$ )
$A S_{2} (n) = A S_{1}^{n} (n + 1) > C \cdot (10 ↑)^{n} (\frac{n + 1}{C}) > 10 ↑ ↑ n [↑ \frac{n + 1}{C}]$ (for $n \geq 2$ )
$A S_{k} (n) = A S_{k - 1}^{n} (n + 1) > (10 ↑^{k - 1})^{n} (n + 1)$ (for $k \geq 3$ and $n \geq 1$ )

AckDiag[k, Tri]

Let $A T_{k} (n) : = D i a g R e p^{k} [R e p S u c c [T r i]] (n, n) = A c k D i a g [k, T r i] (n - 1)$

$T r i (n) = \frac{n (n + 1)}{2} > \frac{1}{2} n^{2}$
$A T_{0} (n) = T r i^{n} (n + 1) > 2 {(\frac{n + 1}{2})}^{2^{n}}$
$A T_{0} (2) = 21$ , $A T_{0} (3) = 1540$ , $A T_{0} (4) > 1 0^{7.42}$
$A T_{0} (n) > C 1 0^{1 0^{(\frac{n - 1}{C})}} + 1$ (for $n \geq 5$ )
$A T_{1} (n) = A T_{0}^{n} (n + 1) > C (10 ↑)^{2 n - 2} (\frac{A T_{0} (n + 1)}{C})$
$A T_{1} (2) > 1 0^{1 0^{A T_{0} (3) / C}} > 1 0^{1 0^{463}}$ , $A T_{1} (3) > 1 0^{1 0^{1 0^{1 0^{A T_{0} (4) / C}}}} > 10 ↑ ↑ 5$
$A T_{1} (n) > 10 ↑ ↑ 2 n$ (for $n \geq 4$ )
$A T_{2} (n) = A T_{1}^{n} (n + 1) > (10 ↑ ↑)^{n - 1} (A T_{1} (n + 1))$
$A T_{2} (2) = A T_{1}^{2} (3) > A T_{1} (10 ↑ ↑ 5) > 10 ↑ ↑ 10 ↑ ↑ 5$ , $A T_{2} (3) = A T_{1}^{3} (4) > 10 ↑ ↑ 10 ↑ ↑ 10 ↑ ↑ 8$
$A T_{2} (n) > 10 ↑ ↑ ↑ (n + 1)$ (for $n \geq 4$ )
$A T_{3} (n) = A T_{2}^{n} (n + 1) > (10 ↑ ↑ ↑)^{n - 1} (A T_{2} (n + 1))$
$A T_{3} (2) = A T_{2}^{2} (3) > A T_{2} (10 ↑ ↑ ↑ 3) > 10 ↑ ↑ ↑ 10 ↑ ↑ ↑ 3$

Pairing Functions

In order to do arbitrary computation, GRF need to be able to store arbitrary data into a single integer (since the R combinator only passes a single accumulator). There are many ways to do that and the Graham champions above accomplish it via custom binary encodings. But the traditional way to store arbitrary data into an integer is to use a pairing function. Thus there is value in finding small pairing/unpairing functions.

We define two APIs here for pairing functions:

A triple of GRF Pair, Left, Right such that for all a,b: Left(Pair(a,b)) = a and Right(Pair(a,b)) = b
A GRF Pair and GRF Macro LRCall[f] such that for all a,b,f: LRCall[f](Pair(a,b)) = f(a,b)

The smallest known pairing functions are:

Smallest Pairing Functions
Macro	arity	Definition	Size	Function
$P a i r$	2	$P a i r : = C (A d d S, C (T r i, A d d), P_{1}^{2})$	20	$λ x y . \frac{(x + y) (x + y + 1)}{2} + x + 1$
$L e f t$	1	$L e f t : = C (R M o n u s, C (T r i P, I n v T r i C e i l), P r e d)$	38	$L e f t (P a i r (x, y)) = x$
$R i g h t$	1	$R i g h t : = C (R M o n u s, P_{1}^{1}, C (T r i, I n v T r i C e i l))$	36	$R i g h t (P a i r (x, y)) = y$
$L R C a l l [f^{2}]$	1	$L R C a l l [f] : = C (L R p a r t 3 [f], I n v T r i C e i l, P_{1}^{1})$	$59 + \| f \|$	$L R C a l l [f] (P a i r (x, y)) = f (x, y)$

Where these are based on the following definitions:

Macros
	Macro	arity	Definition	Size	Function
Addition	Add	2	$A d d : = R (P_{1}^{1}, C (S, P_{2}^{3}))$	5	$λ x y . x + y$
	AddXA	3	$A d d X A : = R (P_{1}^{2}, C (S, P_{2}^{4}))$	5	$λ x y z . x + y$
	AddS	2	$A d d S : = R (S, C (S, P_{2}^{3}))$	5	$λ x y . x + y + 1$
Predecesor	Pred	1	$P r e d : = R (Z^{0}, P_{1}^{2})$	3	$λ x . x \dot{-} 1$
Monus	RMonus	2	$R M o n u s : = R (P_{1}^{1}, C (P r e d, P_{2}^{3}))$	7	$λ x y . y \dot{-} x$
Triangular numbers	Tri	1	$T r i : = R (Z^{0}, A d d S)$	7	$λ x . \frac{x (x + 1)}{2}$
	TriP	1	$T r i P : = R (Z^{0}, A d d)$	7	$T r i P (x + 1) = T r i (x)$
	TriPXA	2	$T r i P X A : = R (Z^{1}, A d d X A)$	7	$T r i P X A (x, y) = T r i P (x)$
Inverting Tri	RMonusTri	2	$R M o n u s T r i : = C (R M o n u s, C (T r i, P_{1}^{2}), P_{2}^{2})$	18	$λ x y . y \dot{-} T r i (x)$
Inverting Tri	InvTriCeil	1	$I n v T r i C e i l : = M (R M o n u s T r i)$	19	$λ y . \min {x \| T r i (x) \geq y}$
Combined LRCall	RightPiece	3	$R i g h t P i e c e : = R (P_{2}^{2}, C (P r e d, P_{2}^{4}))$	7	$λ x y z . z \dot{-} x$
	LeftPiece	3	$L e f t P i e c e : = C (R M o n u s, C (S, P_{2}^{3}), P_{1}^{3})$	12	$λ x y z . x \dot{-} (y + 1)$
	LRpart1[f]	3	$L R p a r t 1 [f] : = C (f, L e f t P i e c e, R i g h t P i e c e)$	$20 + \| f \|$	$λ x y z . f (x \dot{-} (y + 1), z \dot{-} x)$
	LRpart2[f]	3	$L R p a r t 2 [f] : = C (L R p a r t 1 [f], P_{3}^{3}, P_{1}^{3}, A d d X A)$	$28 + \| f \|$	$λ x y z . f (z \dot{-} (x + 1), x + y \dot{-} z)$
	LRpart3[f]	2	$L R p a r t 3 [f] : = C (L R p a r t 2 [f], T r i P X A, P_{1}^{2}, P_{2}^{2})$	$38 + \| f \|$	$λ x y . f (y \dot{-} (T r i P (x) + 1), T r i P (x) + x \dot{-} y)$