This is a term that performs modulo 32 addition on two 32-bit binary numbers efficiently on the abstract algorithm.

On this example, I compute `279739872 + 496122620 = 775862492`.

```
binSize= 32
binZero= (binSize r.a.b.c.(a r) a.b.c.c)
binSucc= (binSize r.x.a.b.c.(x b x.(a (r x)) c) a.a)
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)
binToNat= (binSize r.n.x.(x x.f.(f x) x.f.(add n (f x)) f.0 (r (mul 2 n))) n.x.0 1)
binAdd= a. b. (binToNat a binSucc (binToNat b binSucc binZero))

A= x.a.b.c.(a x)
B= x.a.b.c.(b x)
C= a.b.c.c
X= (A (A (A (A (A (B (B (B (B (A (B (B (B (B (B (A (A (A (B (B (A (B (A (B (A (A (A (A (B (A (A (A C))))))))))))))))))))))))))))))))
Y= (A (A (B (B (B (B (B (B (A (B (A (B (B (B (A (A (A (B (A (A (B (A (A (B (B (A (B (B (B (A (A (A C))))))))))))))))))))))))))))))))

(binFold (binAdd X Y))
```

This works by converting both bitstrings to unary (i.e., Nat), and then applying the binary `succ` function `279739872 + 496122620` times to the bitstring `zero`. So, yes, it applies a linear-time function millions of times to a term  that shouldn't even fit in your computer's memory, yet it reaches normal form in merely `152715` rewrites! That's amazing, isn't it? This example shows well the power of optimal sharing.

Of course, there are faster solutions. By understanding how to make those terms lightweight, you could write this:

```
binAdd= x.y.
  (x.(x x)
    r.x.y.k.(x
      xs.(y
        ys.xs.k.f.a.b.c.(k b a (f xs ys a.b.b))
        ys.xs.k.f.a.b.c.(k a b (f xs ys k))
        xs.k.f.a.b.c.c
        xs)
      xs.(y
        ys.xs.k.f.a.b.c.(k a b (f xs ys k))
        ys.xs.k.f.a.b.c.(k b a (f xs ys a.b.a))
        xs.k.f.a.b.c.c
        xs)
      k.f.a.b.c.c
      k
      (r r))
    x
    y
    a.b.b)

binSize= 32
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)

A= x.a.b.c.(a x)
B= x.a.b.c.(b x)
C= a.b.c.c
X= (A (A (A (A (A (B (B (B (B (A (B (B (B (B (B (A (A (A (B (B (A (B (A (B (A (A (A (A (B (A (A (A C))))))))))))))))))))))))))))))))
Y= (A (A (B (B (B (B (B (B (A (B (A (B (B (B (A (A (A (B (A (A (B (A (A (B (B (A (B (B (B (A (A (A C))))))))))))))))))))))))))))))))

(binFold (binAdd X Y))
```

It performs the same computation, but on arbitrary bit-strings instead of mod-32, and takes only `7817` total rewrites. It is just the equivalent of an usual Haskellish carry-passing recursive addition, though, so no sharing wizardry.

*Not so fun fact: it took me years to develop the right techniques and intuition to be able to write those. Yes, for all that time I wasn't able to code a fast binary addition term; and, trust me, I tried A LOT of things. All my previous attempts had exponential complexity. As expected, it turned out to be amazingly simple.*

Gist per request of Anton Salikhmetov, who is doing amazing progress :)