Konstrukce PRF z axiomů a odvozovacích pravidel

Konstanta C(x)=x

f_1 = o(x)
f_2 = I^2_3(x_1, x_2, x_3)
f_3 = s(x)
f_4 = S^1_3(f_3, f_2)
f_5 = R_2(f_1, f_4)
f_6 = S^2_1(f_5, I^1_1, I^1_1)

Sčítání

  f1 = s(x)
  f2 = I11(x)
  f3 = I23(x1, x2, x3)
  f4 = S13(f1, f3) = λx1x2x3[x2 + 1]
  f5 = R2(f2, f4)
      tj. f5(0, x2) = f2(x2) = x2
          f5(x1 + 1, x2) = f4(x1, f5(x1, x2), x2) = f5(x1, x2) + 1
  sum(x, y) = f5

Násobení

f1 = o(x)
f2 = I23
f3 = I33
f4 = S23(sum, f2, f3)
f5 = R2(f1, f4)
multiply(x, y) = f5

Sign(x)

f1 = o(x)
f2 = s(x)
f3 = S11(f2, f1)
f4 = I33(x1, x2, x3)
f5 = S11(f3, f4)
f6 = R2(f1, f5)
f7 = I11(x1)
f8 = S21(f6, f7, f7)
sign(x) = f8