Lambda the Ultimate

Some time ago, I found an impure solution to the problem of matching fans in Lamping's abstract algorithm. It is described in [1] and implemented in [2], the essential part of source code being available in [3].

My understanding is that the algorithm effectively eliminates the need in bookkeeping nodes (so-called "oracle") for optimal reduction in case of arbitrary untyped λ-terms. Although I have no formal proof for its correctness yet, the amount of testing [4, 5] that have already been done leaves little room for counterexamples.

Questions remaining open are: how to (dis)prove correctness of the algorithm as well as how to simplify and improve the algorithm? Any help would be highly appreciated.

[1] https://arxiv.org/abs/1710.07516
[2] https://codedot.github.io/lambda/
[3] https://github.com/codedot/lambda/blob/master/encoding/abstract/template.txt
[4] https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487
[5] https://www.npmjs.com/package/@alexo/lambda (the "Benchmarks" section)