Laver table computations and an algorithm that is not known to terminate in ZFC

Binary Lambda Calculus, 215 bits (27 bytes)

\io. let
  zero = \f\x. x;
  one = \x. x;
  two = \f\x. f (f x);
  sixteen = (\x. x x x) two;
  pred = \n\f\x. n (\g\h. h (g f)) (\h. x) (\x. x);
  laver = \mx.
    let laver = \b\a. a (\_. mx (b (laver (pred a))) zero) b
    in laver;
  sweet = sixteen;
  dblp1 = \n\f\x. n f (n f (f x)); -- map n to 2*n+1
  go2 = \mx. laver mx sweet mx (\_. mx) (go2 (dblp1 mx));
in go2 one

compiles to (using software at https://github.com/tromp/AIT)

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010

This solution is mostly due to https://github.com/int-e

CJam (36 32 bytes)

1{2*31TW$,(+a{0X$j@(@jj}2j)W$=}g

In practice, this errors out quite quickly because it overflows the call stack, but on a theoretical unlimited machine it is correct, and I understand that to be the assumption of this question.

The code for table(n,x,y) is rather inefficient and it can only compute in the Laver table A₄ in a reasonable amount of time.

is not actually correct if we cache computed values to avoid recomputing them. That's the approach I've taken, using the j (memoisation) operator. It tests A₆ in milliseconds and overflows the stack testing A₇ - and I've actually deoptimised table in the interests of golfing.

Dissection

If we assume that n is understood from the context, instead of

f(x,y) =
    x==2^n ? y :
    y==1 ? x+1 :
    f(f(x,y-1),x+1)

we can remove the first special case, giving

f(x,y) =
    y==1 ? x+1 :
    f(f(x,y-1),x+1)

and it still works because

f(2^n, 1) = 2^n + 1 = 1

and for any other y,

f(2^n, y) = f(f(2^n, y-1), 1) = f(2^n, y-1) + 1

so by induction we get f(2^n, y) = y.

For CJam it turns out to be more convenient to reverse the order of the parameters. And rather than using the range 1 .. 2^n I'm using the range 0 .. 2^n - 1 by decrementing each value, so the recursive function I'm implementing is

g(y,x) =
    y==0 ? x+1
         : g(x+1, g(y-1, x))

---

1           e# Initial value of 2^n
{           e# do-while loop
  2*        e#   Double 2^n (i.e. increment n)
  31T       e#   table(n,1,32) is g(31,0) so push 31 0
  W$,(+a    e#   Set up a lookup table for g(0,x) = x+1 % 2^n
  {         e#   Memoisation function body: stack is 2^n ... y x
    0X$j    e#     Compute g(0,x) = x+1 % 2^n
            e#     Stack is 2^n ... y x (x+1%2^n)
    @(      e#     Bring y to top, decrement (guaranteed not to underflow)
            e#     Stack is 2^n ... x (x+1%2^n) (y-1%2^n)
    @jj     e#     Rotate and apply memoised function twice: g(x+1,g(y-1,x))
  }
  2j        e#   Memoise two-parameter function
            e#   Stack: 2^n g(31,0)
  )W$=      e#   Test whether g(31,0)+1 is 2^n
}g          e# Loop while true