diff --git a/Makefile b/Makefile
index 4dc6f83..6c663d8 100644
--- a/Makefile
+++ b/Makefile
@@ -1,15 +1,12 @@
-all: compile.js
-	npm install
-	node lambda -e 'eval(1 << 3) f x'
-	node lambda -t 'S hello bye world'
-	node lambda -d 'x: (x: x) v1 x'
-	node debug.js 1000 M 1 5
-	sh bad.sh
-	sh test.sh
+CTX = (w: w M w) (x: x x)
 
-compile.js: grammar.jison
-	npm install --no-save jison@0.4.18
-	node_modules/.bin/jison $< -o $@
+all:
+	npm install
+	node generate.js "$(CTX)" 1 6 >terms.txt
+	node line.js abstract 150 <terms.txt >output.tsv
+	node compute.js abstract 150 "$(CTX)" 1 6 >abstract.tsv
+	awk -f stats.awk abstract.tsv
 
 clean:
 	-rm -fr node_modules
+	-rm -f abstract.tsv terms.txt output.tsv
diff --git a/README.md b/README.md
index b29e49c..d6b1a84 100644
--- a/README.md
+++ b/README.md
@@ -1,219 +1,33 @@
-This package implements the lambda calculus using
-interaction nets, providing CLI and API.
+Exhaustive search through MLC inputs
 
-Its browserified version is available as [an online demo][1].
-
-[1]: https://codedot.github.io/lambda/
-
-# Algorithms
-
-The following encodings of the lambda calculus are included:
-
-* `abstract`, an impure solution to the problem of matching fans
-in [Lamping's abstract algorithm][7],
-described in [arXiv:1710.07516][6],
-this is the default algorithm;
-
-* `closed`, the approach of [arXiv:1304.2290][2] applied to
-[_An Interaction Net Implementation of Closed Reduction_][3]
-by Ian Mackie;
-
-* `optimal`, an implementation of
-[_Lambdascope_][5] by Vincent van Oostrom et al;
-
-* `standard`, an implementation of optimal reduction as in
-[_The Optimal Implementation of Functional Programming Languages_][8],
-pp. 40-41.
-
-The embedded read-back mechanism is described
-in Section 7 of [10.4204/EPTCS.225.7][4].
-
-[2]: https://arxiv.org/abs/1304.2290
-[3]: http://dx.doi.org/10.1007/978-3-642-24452-0_3
-[4]: http://dx.doi.org/10.4204/EPTCS.225.7
-[5]: http://www.phil.uu.nl/~oostrom/publication/pdf/lambdascope.pdf
-[6]: https://arxiv.org/abs/1710.07516
-[7]: https://doi.org/10.1145/96709.96711
-[8]: https://books.google.com/books?id=Bod5HbPh-WwC
-
-# Benchmarks
-
-The following is output of the `test.sh` script provided in the package:
+# Usage
 
 ```
-SAMPLE          ABSTRACT         CLOSED        OPTIMAL       STANDARD
-counter              N/A         162/25         582/14        2322/14
-w2eta               37/7         137/16          207/7          374/7
-1021              199/55     11871/1088     1599877/55     4307803/55
-22210i            494/68       2539/254       58603/68            N/A
-3222i            1206/50       8638/819      804530/50            N/A
-1022i            4317/69     33369/3139            N/A            N/A
-2222101   2621862/327818            N/A            N/A            N/A
-facty6nt        1112/210     80562/2436    2790152/210    3013433/210
-facty9i         1629/287 3746232/130949            N/A            N/A
-33-fact4        3770/704      16114/912      80708/704     234075/704
-fibo16nt      24931/3042    134135/5673   5462375/3042   8959455/3042
-fact100i      28502/3752   121854/10565            N/A            N/A
-35-fact5     72944/13480   805218/16206  4702711/13480            N/A
-fibo20i       93534/6863   536843/24626   1961508/6863   4023117/6863
-fact1knt 6215039/1353692            N/A            N/A            N/A
+node generate.js ctx min max >file.txt
+node compute.js algo limit ctx min max >file.tsv
+tail -f -n +1 file.tsv | awk -f stats.awk
+paste left.tsv right.tsv | awk -f diff.awk
 ```
 
-`T/B` should be read as total of `T` interactions,
-of which `B` were β-reductions.
+where
 
-# CLI
+* `ctx` is a context `...M...` with one hole `M`;
+* `min`/`max` is the minimum/maximum size for terms;
+* `algo` is the MLC algorithm to use;
+* `limit` is the maximum number of interactions per term;
 
-This package provides the `lambda` command with the following interface:
+and
 
 ```
-Usage: lambda [options] (<term> | -f <file>)
-
-Options:
-  --algo, -a     Select algorithm         [string]
-  --debug, -d    Evaluate step by step   [boolean]
-  --exec, -e     Process m4(1) macros    [boolean]
-  --file, -f     Read term from file     [boolean]
-  --inet, -i     Show interaction net    [boolean]
-  --limit, -l    Limit interactions       [number]
-  --macros, -m   Read macros from file    [string]
-  --perf, -p     Print benchmarks        [boolean]
-  --stats, -s    Save statistics to file  [string]
-  --term, -t     Output expanded term    [boolean]
-  --help, -h     Show help               [boolean]
-  --version, -v  Show version number     [boolean]
-
+size(x) = 0;
+size(x: M) = 1 + size(M);
+size(M N) = 1 + size(M) + size(N).
 ```
 
-# Combinators
-
-CLI predefines a number of commonly used combinators:
-
-```
-# Common combinators
-I = x: x;
-K = x, y: x;
-S = x, y, z: x z (y z);
-Y = (a: a a) (a, f: f (a a f));
-
-# Booleans
-T = K;
-F = K I;
-Not = p, a, b: p b a;
-And = p, q: p q F;
-Or = p, q: p T q;
-Xor = p, q: p Not I q;
-
-# Pairs/lists
-[] = K T;
-[]? = l: l (h, t: F);
-Cons = h, t, x: x h t;
-Head = l: l T;
-Tail = l: l F;
-
-# Church arithmetic
-+1 = n, f, x: f (n f x);
-+ = m, n, f, x: m f (n f x);
-* = m, n, f: m (n f);
-^ = m, n: n m;
--1 = n, f, x: n (g, h: h (g f)) (K x) I;
-- = m, n: n -1 m;
-0? = n: n (K F) T;
-
-# Church numerals
-0 = f, x: x;
-1 = f, x: f x;
-2 = +1 1;
-3 = +1 2;
-4 = ^ 2 2;
-5 = + 2 3;
-6 = * 2 3;
-7 = +1 6;
-8 = ^ 2 3;
-9 = ^ 3 2;
-10 = * 2 5;
-16 = ^ 2 4;
-20 = * 2 10;
-30 = * 3 10;
-32 = ^ 2 5;
-64 = ^ 2 6;
-100 = ^ 10 2;
-128 = ^ 2 7;
-256 = ^ 2 8;
-512 = ^ 2 9;
-1k = ^ 10 3;
-1ki = ^ 2 10;
-1m = ^ 10 6;
-1mi = ^ 2 20;
-1g = ^ 10 9;
-1gi = ^ 2 30;
-
-# Recursive functions
-FactY = Y (f, n: (0? n) 1 (* (f (-1 n)) n));
-Fact = n: n (f, i: * (f (+1 i)) i) (K 1) 1;
-Fibo = n: n (f, a, b: f (+ a b) a) F 1 0;
-```
-
-# API
-
-`require("@alexo/lambda")` returns a function of a lambda term defined
-in a variant of the lambda calculus called Macro Lambda Calculus (MLC)
-that allows macro definitions in order to input complex expressions.
-The last term in the input is the term whose normal form is to be found.
-
-For developing and testing purposes, the package also exports
-two additional functions `.prepare(term)` and `.debug()`.
-The `.debug()` function applies a single reduction step to
-the interaction net compiled by the previous `.prepare()`
-call and returns a human-readable string representation of
-the current interaction net state.
-
-# Grammar
-
-Input consists of an optional list of macro definitions and a term:
-
-```
-%token NAME
-
-%%
-
-text : defs term
-     ;
-defs : /* empty */
-     | defs NAME '=' term ';'
-     ;
-term : appl
-     | abst
-     ;
-abst : NAME ',' abst
-     | NAME ':' term
-     ;
-appl :      atom
-     | appl atom
-     ;
-atom : '(' term ')'
-     |     NAME
-     ;
-```
-
-# License
-
-Copyright (c) 2017 Anton Salikhmetov
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
+* * *
 
-The above copyright notice and this permission notice shall be included in
-all copies or substantial portions of the Software.
+The idea was suggested by Gabriel Scherer:
+http://lambda-the-ultimate.org/node/5487
 
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
-THE SOFTWARE.
+Number of closed lambda-terms of size n with size 0 for the variables:
+http://oeis.org/A220894
diff --git a/bad.sh b/bad.sh
deleted file mode 100644
index e20c8dc..0000000
--- a/bad.sh
+++ /dev/null
@@ -1,28 +0,0 @@
-set -x
-
-alias lambda="node lambda -l 10000"
-
-lambda "((v0: ((v0 v0) v0)) (v0: (v1: (v0 (v2: (v1 (v0 v2)))))))"
-lambda "((v0: (v0 (v0 v0))) (v0: (v1: (v0 (v2: (v1 (v0 v2)))))))"
-lambda "((v0: (v0 v0)) (v0: (v0 (v1: (v0 (v2: (v1 (v0 v2))))))))"
-lambda "(2: (M: (y: M) M (x: x)) (h: 2 2 (z, t: h ((x: z) z t)))) (f, x: f (f x))"
-lambda "(w: w (v0: (v1: (v0 (v2: (v1 (v0 v2)))))) w) (x: x x)"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v0 (v2: (v1 (v0 v2))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v3: (v1 (v1 (v0 v3)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v3: (v2 (v2 (v1 v3)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: ((v1 (v0 (v0 v2))) v1))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v0 (v3: (v1 (v0 v3)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v0 (v3: (v2 (v0 v3)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v1 (v3: (v2 (v1 v3)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v2: (v1 ((v0 (v0 v2)) v1)))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v0 (v2: (v1 (v3: (v0 v2)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v0 (v0 (v2: (v1 (v0 v2)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v1: (v1 (v0 (v2: (v1 (v0 v2)))))))))"
-lambda "(x: x x) ((x: x x) ((x: x x) (v0: (v0 (v1: (v0 (v2: (v1 (v0 v2)))))))))"
-lambda "(x: x x x x x x) (g, j, y: g (f, x: j f (y f x)))"
-lambda "(v1: v1 v1 v1 v1) (g, j, y: g (f, x: j f (y f x)))"
-lambda "(I: (2: (M: 2 M 2 I I) (f, x: 2 f (h, u: x h (h u)))) (f, x: f (f x))) (x: x)"
-lambda "(2: (M: M M) (h: 2 2 (z, t: h (z z t)))) (f, x: f (f x))"
-lambda "(v0: ((v1: (v1 v1)) (v1: (v0 (v2: v1)))))"
-
-exit
diff --git a/compile.js b/compile.js
deleted file mode 100644
index 843c4d7..0000000
--- a/compile.js
+++ /dev/null
@@ -1,638 +0,0 @@
-/* parser generated by jison 0.4.18 */
-/*
-  Returns a Parser object of the following structure:
-
-  Parser: {
-    yy: {}
-  }
-
-  Parser.prototype: {
-    yy: {},
-    trace: function(),
-    symbols_: {associative list: name ==> number},
-    terminals_: {associative list: number ==> name},
-    productions_: [...],
-    performAction: function anonymous(yytext, yyleng, yylineno, yy, yystate, $$, _$),
-    table: [...],
-    defaultActions: {...},
-    parseError: function(str, hash),
-    parse: function(input),
-
-    lexer: {
-        EOF: 1,
-        parseError: function(str, hash),
-        setInput: function(input),
-        input: function(),
-        unput: function(str),
-        more: function(),
-        less: function(n),
-        pastInput: function(),
-        upcomingInput: function(),
-        showPosition: function(),
-        test_match: function(regex_match_array, rule_index),
-        next: function(),
-        lex: function(),
-        begin: function(condition),
-        popState: function(),
-        _currentRules: function(),
-        topState: function(),
-        pushState: function(condition),
-
-        options: {
-            ranges: boolean           (optional: true ==> token location info will include a .range[] member)
-            flex: boolean             (optional: true ==> flex-like lexing behaviour where the rules are tested exhaustively to find the longest match)
-            backtrack_lexer: boolean  (optional: true ==> lexer regexes are tested in order and for each matching regex the action code is invoked; the lexer terminates the scan when a token is returned by the action code)
-        },
-
-        performAction: function(yy, yy_, $avoiding_name_collisions, YY_START),
-        rules: [...],
-        conditions: {associative list: name ==> set},
-    }
-  }
-
-
-  token location info (@$, _$, etc.): {
-    first_line: n,
-    last_line: n,
-    first_column: n,
-    last_column: n,
-    range: [start_number, end_number]       (where the numbers are indexes into the input string, regular zero-based)
-  }
-
-
-  the parseError function receives a 'hash' object with these members for lexer and parser errors: {
-    text:        (matched text)
-    token:       (the produced terminal token, if any)
-    line:        (yylineno)
-  }
-  while parser (grammar) errors will also provide these members, i.e. parser errors deliver a superset of attributes: {
-    loc:         (yylloc)
-    expected:    (string describing the set of expected tokens)
-    recoverable: (boolean: TRUE when the parser has a error recovery rule available for this particular error)
-  }
-*/
-var compile = (function(){
-var o=function(k,v,o,l){for(o=o||{},l=k.length;l--;o[k[l]]=v);return o},$V0=[7,15],$V1=[1,8],$V2=[2,11],$V3=[1,11],$V4=[1,12],$V5=[6,9,16],$V6=[6,7,9,15,16],$V7=[1,16];
-var parser = {trace: function trace() { },
-yy: {},
-symbols_: {"error":2,"text":3,"defs":4,"term":5,"EOF":6,"NAME":7,"=":8,";":9,"appl":10,"abst":11,",":12,":":13,"atom":14,"(":15,")":16,"$accept":0,"$end":1},
-terminals_: {2:"error",6:"EOF",7:"NAME",8:"=",9:";",12:",",13:":",15:"(",16:")"},
-productions_: [0,[3,3],[4,0],[4,5],[5,1],[5,1],[11,3],[11,3],[10,1],[10,2],[14,3],[14,1]],
-performAction: function anonymous(yytext, yyleng, yylineno, yy, yystate /* action[1] */, $$ /* vstack */, _$ /* lstack */) {
-/* this == yyval */
-
-var $0 = $$.length - 1;
-switch (yystate) {
-case 1:
-return {macros: $$[$0-2], term: $$[$0-1]};
-break;
-case 2:
-this.$ = [];
-break;
-case 3:
-$$[$0-4].unshift({id: $$[$0-3], def: $$[$0-1]}); this.$ = $$[$0-4];
-break;
-case 6: case 7:
-this.$ = {node: "abst", bound: $$[$0-2], body: $$[$0]};
-break;
-case 9:
-this.$ = {node: "appl", left: $$[$0-1], right: $$[$0]};
-break;
-case 10:
-this.$ = $$[$0-1];
-break;
-case 11:
-this.$ = {node: "atom", name: yytext};
-break;
-}
-},
-table: [o($V0,[2,2],{3:1,4:2}),{1:[3]},{5:3,7:[1,4],10:5,11:6,14:7,15:$V1},{6:[1,9]},o([6,7,15],$V2,{8:[1,10],12:$V3,13:$V4}),o($V5,[2,4],{14:13,7:[1,14],15:$V1}),o($V5,[2,5]),o($V6,[2,8]),{5:15,7:$V7,10:5,11:6,14:7,15:$V1},{1:[2,1]},{5:17,7:$V7,10:5,11:6,14:7,15:$V1},{7:[1,19],11:18},{5:20,7:$V7,10:5,11:6,14:7,15:$V1},o($V6,[2,9]),o($V6,$V2),{16:[1,21]},o($V6,$V2,{12:$V3,13:$V4}),{9:[1,22]},o($V5,[2,6]),{12:$V3,13:$V4},o($V5,[2,7]),o($V6,[2,10]),o($V0,[2,3])],
-defaultActions: {9:[2,1]},
-parseError: function parseError(str, hash) {
-    if (hash.recoverable) {
-        this.trace(str);
-    } else {
-        var error = new Error(str);
-        error.hash = hash;
-        throw error;
-    }
-},
-parse: function parse(input) {
-    var self = this, stack = [0], tstack = [], vstack = [null], lstack = [], table = this.table, yytext = '', yylineno = 0, yyleng = 0, recovering = 0, TERROR = 2, EOF = 1;
-    var args = lstack.slice.call(arguments, 1);
-    var lexer = Object.create(this.lexer);
-    var sharedState = { yy: {} };
-    for (var k in this.yy) {
-        if (Object.prototype.hasOwnProperty.call(this.yy, k)) {
-            sharedState.yy[k] = this.yy[k];
-        }
-    }
-    lexer.setInput(input, sharedState.yy);
-    sharedState.yy.lexer = lexer;
-    sharedState.yy.parser = this;
-    if (typeof lexer.yylloc == 'undefined') {
-        lexer.yylloc = {};
-    }
-    var yyloc = lexer.yylloc;
-    lstack.push(yyloc);
-    var ranges = lexer.options && lexer.options.ranges;
-    if (typeof sharedState.yy.parseError === 'function') {
-        this.parseError = sharedState.yy.parseError;
-    } else {
-        this.parseError = Object.getPrototypeOf(this).parseError;
-    }
-    function popStack(n) {
-        stack.length = stack.length - 2 * n;
-        vstack.length = vstack.length - n;
-        lstack.length = lstack.length - n;
-    }
-    _token_stack:
-        var lex = function () {
-            var token;
-            token = lexer.lex() || EOF;
-            if (typeof token !== 'number') {
-                token = self.symbols_[token] || token;
-            }
-            return token;
-        };
-    var symbol, preErrorSymbol, state, action, a, r, yyval = {}, p, len, newState, expected;
-    while (true) {
-        state = stack[stack.length - 1];
-        if (this.defaultActions[state]) {
-            action = this.defaultActions[state];
-        } else {
-            if (symbol === null || typeof symbol == 'undefined') {
-                symbol = lex();
-            }
-            action = table[state] && table[state][symbol];
-        }
-                    if (typeof action === 'undefined' || !action.length || !action[0]) {
-                var errStr = '';
-                expected = [];
-                for (p in table[state]) {
-                    if (this.terminals_[p] && p > TERROR) {
-                        expected.push('\'' + this.terminals_[p] + '\'');
-                    }
-                }
-                if (lexer.showPosition) {
-                    errStr = 'Parse error on line ' + (yylineno + 1) + ':\n' + lexer.showPosition() + '\nExpecting ' + expected.join(', ') + ', got \'' + (this.terminals_[symbol] || symbol) + '\'';
-                } else {
-                    errStr = 'Parse error on line ' + (yylineno + 1) + ': Unexpected ' + (symbol == EOF ? 'end of input' : '\'' + (this.terminals_[symbol] || symbol) + '\'');
-                }
-                this.parseError(errStr, {
-                    text: lexer.match,
-                    token: this.terminals_[symbol] || symbol,
-                    line: lexer.yylineno,
-                    loc: yyloc,
-                    expected: expected
-                });
-            }
-        if (action[0] instanceof Array && action.length > 1) {
-            throw new Error('Parse Error: multiple actions possible at state: ' + state + ', token: ' + symbol);
-        }
-        switch (action[0]) {
-        case 1:
-            stack.push(symbol);
-            vstack.push(lexer.yytext);
-            lstack.push(lexer.yylloc);
-            stack.push(action[1]);
-            symbol = null;
-            if (!preErrorSymbol) {
-                yyleng = lexer.yyleng;
-                yytext = lexer.yytext;
-                yylineno = lexer.yylineno;
-                yyloc = lexer.yylloc;
-                if (recovering > 0) {
-                    recovering--;
-                }
-            } else {
-                symbol = preErrorSymbol;
-                preErrorSymbol = null;
-            }
-            break;
-        case 2:
-            len = this.productions_[action[1]][1];
-            yyval.$ = vstack[vstack.length - len];
-            yyval._$ = {
-                first_line: lstack[lstack.length - (len || 1)].first_line,
-                last_line: lstack[lstack.length - 1].last_line,
-                first_column: lstack[lstack.length - (len || 1)].first_column,
-                last_column: lstack[lstack.length - 1].last_column
-            };
-            if (ranges) {
-                yyval._$.range = [
-                    lstack[lstack.length - (len || 1)].range[0],
-                    lstack[lstack.length - 1].range[1]
-                ];
-            }
-            r = this.performAction.apply(yyval, [
-                yytext,
-                yyleng,
-                yylineno,
-                sharedState.yy,
-                action[1],
-                vstack,
-                lstack
-            ].concat(args));
-            if (typeof r !== 'undefined') {
-                return r;
-            }
-            if (len) {
-                stack = stack.slice(0, -1 * len * 2);
-                vstack = vstack.slice(0, -1 * len);
-                lstack = lstack.slice(0, -1 * len);
-            }
-            stack.push(this.productions_[action[1]][0]);
-            vstack.push(yyval.$);
-            lstack.push(yyval._$);
-            newState = table[stack[stack.length - 2]][stack[stack.length - 1]];
-            stack.push(newState);
-            break;
-        case 3:
-            return true;
-        }
-    }
-    return true;
-}};
-/* generated by jison-lex 0.3.4 */
-var lexer = (function(){
-var lexer = ({
-
-EOF:1,
-
-parseError:function parseError(str, hash) {
-        if (this.yy.parser) {
-            this.yy.parser.parseError(str, hash);
-        } else {
-            throw new Error(str);
-        }
-    },
-
-// resets the lexer, sets new input
-setInput:function (input, yy) {
-        this.yy = yy || this.yy || {};
-        this._input = input;
-        this._more = this._backtrack = this.done = false;
-        this.yylineno = this.yyleng = 0;
-        this.yytext = this.matched = this.match = '';
-        this.conditionStack = ['INITIAL'];
-        this.yylloc = {
-            first_line: 1,
-            first_column: 0,
-            last_line: 1,
-            last_column: 0
-        };
-        if (this.options.ranges) {
-            this.yylloc.range = [0,0];
-        }
-        this.offset = 0;
-        return this;
-    },
-
-// consumes and returns one char from the input
-input:function () {
-        var ch = this._input[0];
-        this.yytext += ch;
-        this.yyleng++;
-        this.offset++;
-        this.match += ch;
-        this.matched += ch;
-        var lines = ch.match(/(?:\r\n?|\n).*/g);
-        if (lines) {
-            this.yylineno++;
-            this.yylloc.last_line++;
-        } else {
-            this.yylloc.last_column++;
-        }
-        if (this.options.ranges) {
-            this.yylloc.range[1]++;
-        }
-
-        this._input = this._input.slice(1);
-        return ch;
-    },
-
-// unshifts one char (or a string) into the input
-unput:function (ch) {
-        var len = ch.length;
-        var lines = ch.split(/(?:\r\n?|\n)/g);
-
-        this._input = ch + this._input;
-        this.yytext = this.yytext.substr(0, this.yytext.length - len);
-        //this.yyleng -= len;
-        this.offset -= len;
-        var oldLines = this.match.split(/(?:\r\n?|\n)/g);
-        this.match = this.match.substr(0, this.match.length - 1);
-        this.matched = this.matched.substr(0, this.matched.length - 1);
-
-        if (lines.length - 1) {
-            this.yylineno -= lines.length - 1;
-        }
-        var r = this.yylloc.range;
-
-        this.yylloc = {
-            first_line: this.yylloc.first_line,
-            last_line: this.yylineno + 1,
-            first_column: this.yylloc.first_column,
-            last_column: lines ?
-                (lines.length === oldLines.length ? this.yylloc.first_column : 0)
-                 + oldLines[oldLines.length - lines.length].length - lines[0].length :
-              this.yylloc.first_column - len
-        };
-
-        if (this.options.ranges) {
-            this.yylloc.range = [r[0], r[0] + this.yyleng - len];
-        }
-        this.yyleng = this.yytext.length;
-        return this;
-    },
-
-// When called from action, caches matched text and appends it on next action
-more:function () {
-        this._more = true;
-        return this;
-    },
-
-// When called from action, signals the lexer that this rule fails to match the input, so the next matching rule (regex) should be tested instead.
-reject:function () {
-        if (this.options.backtrack_lexer) {
-            this._backtrack = true;
-        } else {
-            return this.parseError('Lexical error on line ' + (this.yylineno + 1) + '. You can only invoke reject() in the lexer when the lexer is of the backtracking persuasion (options.backtrack_lexer = true).\n' + this.showPosition(), {
-                text: "",
-                token: null,
-                line: this.yylineno
-            });
-
-        }
-        return this;
-    },
-
-// retain first n characters of the match
-less:function (n) {
-        this.unput(this.match.slice(n));
-    },
-
-// displays already matched input, i.e. for error messages
-pastInput:function () {
-        var past = this.matched.substr(0, this.matched.length - this.match.length);
-        return (past.length > 20 ? '...':'') + past.substr(-20).replace(/\n/g, "");
-    },
-
-// displays upcoming input, i.e. for error messages
-upcomingInput:function () {
-        var next = this.match;
-        if (next.length < 20) {
-            next += this._input.substr(0, 20-next.length);
-        }
-        return (next.substr(0,20) + (next.length > 20 ? '...' : '')).replace(/\n/g, "");
-    },
-
-// displays the character position where the lexing error occurred, i.e. for error messages
-showPosition:function () {
-        var pre = this.pastInput();
-        var c = new Array(pre.length + 1).join("-");
-        return pre + this.upcomingInput() + "\n" + c + "^";
-    },
-
-// test the lexed token: return FALSE when not a match, otherwise return token
-test_match:function (match, indexed_rule) {
-        var token,
-            lines,
-            backup;
-
-        if (this.options.backtrack_lexer) {
-            // save context
-            backup = {
-                yylineno: this.yylineno,
-                yylloc: {
-                    first_line: this.yylloc.first_line,
-                    last_line: this.last_line,
-                    first_column: this.yylloc.first_column,
-                    last_column: this.yylloc.last_column
-                },
-                yytext: this.yytext,
-                match: this.match,
-                matches: this.matches,
-                matched: this.matched,
-                yyleng: this.yyleng,
-                offset: this.offset,
-                _more: this._more,
-                _input: this._input,
-                yy: this.yy,
-                conditionStack: this.conditionStack.slice(0),
-                done: this.done
-            };
-            if (this.options.ranges) {
-                backup.yylloc.range = this.yylloc.range.slice(0);
-            }
-        }
-
-        lines = match[0].match(/(?:\r\n?|\n).*/g);
-        if (lines) {
-            this.yylineno += lines.length;
-        }
-        this.yylloc = {
-            first_line: this.yylloc.last_line,
-            last_line: this.yylineno + 1,
-            first_column: this.yylloc.last_column,
-            last_column: lines ?
-                         lines[lines.length - 1].length - lines[lines.length - 1].match(/\r?\n?/)[0].length :
-                         this.yylloc.last_column + match[0].length
-        };
-        this.yytext += match[0];
-        this.match += match[0];
-        this.matches = match;
-        this.yyleng = this.yytext.length;
-        if (this.options.ranges) {
-            this.yylloc.range = [this.offset, this.offset += this.yyleng];
-        }
-        this._more = false;
-        this._backtrack = false;
-        this._input = this._input.slice(match[0].length);
-        this.matched += match[0];
-        token = this.performAction.call(this, this.yy, this, indexed_rule, this.conditionStack[this.conditionStack.length - 1]);
-        if (this.done && this._input) {
-            this.done = false;
-        }
-        if (token) {
-            return token;
-        } else if (this._backtrack) {
-            // recover context
-            for (var k in backup) {
-                this[k] = backup[k];
-            }
-            return false; // rule action called reject() implying the next rule should be tested instead.
-        }
-        return false;
-    },
-
-// return next match in input
-next:function () {
-        if (this.done) {
-            return this.EOF;
-        }
-        if (!this._input) {
-            this.done = true;
-        }
-
-        var token,
-            match,
-            tempMatch,
-            index;
-        if (!this._more) {
-            this.yytext = '';
-            this.match = '';
-        }
-        var rules = this._currentRules();
-        for (var i = 0; i < rules.length; i++) {
-            tempMatch = this._input.match(this.rules[rules[i]]);
-            if (tempMatch && (!match || tempMatch[0].length > match[0].length)) {
-                match = tempMatch;
-                index = i;
-                if (this.options.backtrack_lexer) {
-                    token = this.test_match(tempMatch, rules[i]);
-                    if (token !== false) {
-                        return token;
-                    } else if (this._backtrack) {
-                        match = false;
-                        continue; // rule action called reject() implying a rule MISmatch.
-                    } else {
-                        // else: this is a lexer rule which consumes input without producing a token (e.g. whitespace)
-                        return false;
-                    }
-                } else if (!this.options.flex) {
-                    break;
-                }
-            }
-        }
-        if (match) {
-            token = this.test_match(match, rules[index]);
-            if (token !== false) {
-                return token;
-            }
-            // else: this is a lexer rule which consumes input without producing a token (e.g. whitespace)
-            return false;
-        }
-        if (this._input === "") {
-            return this.EOF;
-        } else {
-            return this.parseError('Lexical error on line ' + (this.yylineno + 1) + '. Unrecognized text.\n' + this.showPosition(), {
-                text: "",
-                token: null,
-                line: this.yylineno
-            });
-        }
-    },
-
-// return next match that has a token
-lex:function lex() {
-        var r = this.next();
-        if (r) {
-            return r;
-        } else {
-            return this.lex();
-        }
-    },
-
-// activates a new lexer condition state (pushes the new lexer condition state onto the condition stack)
-begin:function begin(condition) {
-        this.conditionStack.push(condition);
-    },
-
-// pop the previously active lexer condition state off the condition stack
-popState:function popState() {
-        var n = this.conditionStack.length - 1;
-        if (n > 0) {
-            return this.conditionStack.pop();
-        } else {
-            return this.conditionStack[0];
-        }
-    },
-
-// produce the lexer rule set which is active for the currently active lexer condition state
-_currentRules:function _currentRules() {
-        if (this.conditionStack.length && this.conditionStack[this.conditionStack.length - 1]) {
-            return this.conditions[this.conditionStack[this.conditionStack.length - 1]].rules;
-        } else {
-            return this.conditions["INITIAL"].rules;
-        }
-    },
-
-// return the currently active lexer condition state; when an index argument is provided it produces the N-th previous condition state, if available
-topState:function topState(n) {
-        n = this.conditionStack.length - 1 - Math.abs(n || 0);
-        if (n >= 0) {
-            return this.conditionStack[n];
-        } else {
-            return "INITIAL";
-        }
-    },
-
-// alias for begin(condition)
-pushState:function pushState(condition) {
-        this.begin(condition);
-    },
-
-// return the number of states currently on the stack
-stateStackSize:function stateStackSize() {
-        return this.conditionStack.length;
-    },
-options: {},
-performAction: function anonymous(yy,yy_,$avoiding_name_collisions,YY_START) {
-var YYSTATE=YY_START;
-switch($avoiding_name_collisions) {
-case 0:/* skip comment */
-break;
-case 1:/* skip comment */
-break;
-case 2:/* skip whitespace */
-break;
-case 3:return "NAME";
-break;
-case 4:return "=";
-break;
-case 5:return ";";
-break;
-case 6:return ",";
-break;
-case 7:return ":";
-break;
-case 8:return "(";
-break;
-case 9:return ")";
-break;
-case 10:return "EOF";
-break;
-}
-},
-rules: [/^(?:\{[^}]*\})/,/^(?:#.*)/,/^(?:\s+)/,/^(?:[^{}#=;,:()\s]+)/,/^(?:=)/,/^(?:;)/,/^(?:,)/,/^(?::)/,/^(?:\()/,/^(?:\))/,/^(?:$)/],
-conditions: {"INITIAL":{"rules":[0,1,2,3,4,5,6,7,8,9,10],"inclusive":true}}
-});
-return lexer;
-})();
-parser.lexer = lexer;
-function Parser () {
-  this.yy = {};
-}
-Parser.prototype = parser;parser.Parser = Parser;
-return new Parser;
-})();
-
-
-if (typeof require !== 'undefined' && typeof exports !== 'undefined') {
-exports.parser = compile;
-exports.Parser = compile.Parser;
-exports.parse = function () { return compile.parse.apply(compile, arguments); };
-exports.main = function commonjsMain(args) {
-    if (!args[1]) {
-        console.log('Usage: '+args[0]+' FILE');
-        process.exit(1);
-    }
-    var source = require('fs').readFileSync(require('path').normalize(args[1]), "utf8");
-    return exports.parser.parse(source);
-};
-if (typeof module !== 'undefined' && require.main === module) {
-  exports.main(process.argv.slice(1));
-}
-}
\ No newline at end of file
diff --git a/compute.js b/compute.js
new file mode 100644
index 0000000..e8952da
--- /dev/null
+++ b/compute.js
@@ -0,0 +1,33 @@
+"use strict";
+
+const exhaust = require("./exhaust");
+const mlc = require("@alexo/lambda");
+const fs = require("fs");
+
+const argv = process.argv;
+const max = parseInt(argv.pop());
+const min = parseInt(argv.pop());
+const ctx = argv.pop();
+const limit = parseInt(argv.pop());
+const algo = argv.pop();
+
+for (const term of exhaust(ctx, min, max)) {
+	let result;
+
+	try {
+		const output = mlc(term, algo, limit);
+		const total = output.total;
+		const beta = output.beta;
+		const stats = `${total}/${beta}`;
+		let nf = output.nf;
+
+		if (!nf)
+			nf = "?";
+
+		result = `${stats}\t${nf}`;
+	} catch (error) {
+		result = `N/A\t${error}`;
+	}
+
+	fs.writeSync(1, `${term}\t${result}\n`);
+}
diff --git a/debug.js b/debug.js
deleted file mode 100644
index 1fa46d1..0000000
--- a/debug.js
+++ /dev/null
@@ -1,78 +0,0 @@
-"use strict";
-
-const mlc = require(".");
-
-const argv = process.argv;
-const max = parseInt(argv.pop());
-const min = parseInt(argv.pop());
-const ctx = argv.pop();
-const lim = parseInt(argv.pop());
-
-function* sub(len, nv)
-{
-	if (len) {
-		--len;
-
-		for (const t of sub(len, nv + 1))
-			yield `(v${nv}: ${t})`;
-
-		for (let l = 0; l <= len; l++)
-			for (const t of sub(len - l, nv))
-				for (const u of sub(l, nv))
-					yield `(${t} ${u})`;
-	} else {
-		for (let i = 0; i < nv; i++)
-			yield `v${i}`;
-	}
-}
-
-function* wrap(ctx, len)
-{
-	for (const m of sub(len, 0))
-		yield ctx.replace("M", m);
-}
-
-function* exhaust(ctx, min, max)
-{
-	for (let len = min; len <= max; len++)
-		yield* wrap(ctx, len);
-}
-
-function compute(term, algo)
-{
-	const abd = [];
-	const cb = {
-		a: () => abd.push("a"),
-		b: () => abd.push("b"),
-		d: () => abd.push("d")
-	};
-	let result;
-
-	try {
-		result = mlc(term, algo, lim, cb);
-		result.abd = abd.join("");
-	} catch (error) {
-		result = {};
-	}
-
-	return result;
-}
-
-function diff(term)
-{
-	const abstract = compute(term, "abstract");
-	const optimal = compute(term, "optimal");
-
-	if (!optimal.nf)
-		return;
-
-	if (abstract.nf != optimal.nf)
-		return true;
-
-	if (abstract.abd != optimal.abd)
-		return true;
-}
-
-for (const term of exhaust(ctx, min, max))
-	if (diff(term))
-		console.info(term);
diff --git a/diff.awk b/diff.awk
new file mode 100644
index 0000000..5eca268
--- /dev/null
+++ b/diff.awk
@@ -0,0 +1,42 @@
+function beta(s)
+{
+	return substr(s, index(s, "/"));
+}
+
+function detect(b1, b2, nf1, nf2)
+{
+	if (("N/A" == b1) && ("N/A" == b2))
+		return "BERR";
+
+	if ("N/A" == b1)
+		return "LERR";
+
+	if ("N/A" == b2)
+		return "RERR";
+
+	if (("?" == nf1) && ("?" == nf2))
+		return;
+
+	if ("?" == nf1)
+		return "LLIM";
+
+	if ("?" == nf2)
+		return "RLIM";
+
+	if (nf1 != nf2)
+		return "NENF";
+
+	if (beta(b1) != beta(b2))
+		return "BETA";
+}
+
+BEGIN {
+	FS = "\t";
+	OFS = "\t";
+}
+
+{
+	status = detect($2, $5, $3, $6);
+	if (status)
+		print status, $1, $2, $5, $3, $6;
+}
diff --git a/encoding/abstract/index.js b/encoding/abstract/index.js
deleted file mode 100644
index 32e4693..0000000
--- a/encoding/abstract/index.js
+++ /dev/null
@@ -1,81 +0,0 @@
-"use strict";
-
-const fs = require("fs");
-const path = require("path");
-
-const template = fs.readFileSync(path.join(__dirname, "template.txt"), "utf8");
-
-let mkwire, mktwins, getfv;
-
-function psi(shared, list)
-{
-	shared.forEach((twins, atom) => {
-		const left = twins.left;
-		const right = twins.right;
-		const agent = `\\fanin_{this.uniq()}`;
-		const tree = `${agent}(${right}, ${left})`;
-
-		list.push(`${atom} = ${tree}`);
-	});
-}
-
-function gamma(obj, root, list)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		if (obj.free) {
-			const name = `this.mkid("${obj.name}")`;
-			const agent = `\\atom_{${name}}`;
-
-			list.push(`${root} = ${agent}`);
-		} else {
-			const name = obj.name;
-
-			list.push(`${root} = ${name}`);
-		}
-	} else if ("abst" == node) {
-		const id = obj.bound;
-		const body = obj.body;
-		const fv = getfv(body);
-		const wire = mkwire();
-		const agent = fv.has(id) ? id : "\\erase";
-		const tree = `\\lambda(${agent}, ${wire})`;
-
-		list.push(`${root} = ${tree}`);
-
-		gamma(body, wire, list);
-	} else if ("appl" == node) {
-		const wleft = mkwire();
-		const wright = mkwire();
-		const left = obj.left;
-		const right = obj.right;
-		const shared = mktwins(left, right);
-		const agent = `\\apply(${wright}, ${root})`;
-
-		list.push(`${wleft} = ${agent}`);
-
-		gamma(left, wleft, list);
-		gamma(right, wright, list);
-
-		psi(shared, list);
-	}
-}
-
-function encode(generic, term)
-{
-	const inconfig = [
-		"\\read_{this.mkhole()}(!print) = root"
-	];
-
-	mkwire = generic.mkwire;
-	mktwins = generic.mktwins;
-	getfv = generic.getfv;
-
-	gamma(term, "root", inconfig);
-
-	inconfig.inet = template;
-	return inconfig;
-}
-
-module.exports = encode;
diff --git a/encoding/abstract/template.txt b/encoding/abstract/template.txt
deleted file mode 100644
index 7d09a96..0000000
--- a/encoding/abstract/template.txt
+++ /dev/null
@@ -1,93 +0,0 @@
-\apply[a, b] {
-	/* Apply beta reduction. */
-	this.debug.b();
-} \lambda[a, b];
-
-\apply[\fanin_{i}(a, b), \fanout_{i}(c, d)] {
-	/* Duplicate application. */
-	this.debug.o();
-} \fanout_{i}[\apply(a, c), \apply(b, d)];
-
-\fanin_{i}[\lambda(a, b), \lambda(c, d)] {
-	/* Duplicate abstraction. */
-	this.debug.o();
-} \lambda[\fanout_{i}(a, c), \fanin_{i}(b, d)];
-
-\fanin_{i}[\fanout_{this.phi(j, i)}(a, b), \fanout_{j}(c, d)] {
-	/* Duplicate different fans. */
-	if (!this.match(i, j))
-		this.debug.d();
-	else
-		return false;
-} \fanout_{j}[\fanin_{this.phi(i, j)}(a, c), \fanin_{i}(b, d)];
-
-\fanin_{i}[a, b] {
-	/* Annihilate matching fans. */
-	if (this.match(i, j))
-		this.debug.a();
-	else
-		return false;
-} \fanout_{j}[a, b];
-
-\read_{C}[\fanout_{i}(a, b)] {
-	/* Duplicate context. */
-	this.debug.o();
-} \fanout_{i}[\read_{C}(a), \read_{this.clone(C)}(b)];
-
-\print {
-	/* Output results of read-back. */
-	this.nf = M;
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[a] {
-	/* Read back abstraction. */
-	this.debug.o();
-} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
-
-\apply[\read_{this.appl(M)}(a), a] {
-	/* Read back application. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\atom_{this.atom(C, M)}] {
-	/* Read back an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\fanin_{i}[\atom_{M}, \atom_{M}] {
-	/* Duplicate an atom. */
-	this.debug.o();
-} \atom_{M};
-
-$$
-
-INCONFIG
-
-$$
-
-READBACK
-
-const map = new Map();
-let nonce = 0;
-
-function decide(i, j)
-{
-	const key = `${i},${j}`;
-
-	if (map.has(key))
-		return;
-
-	map.set(key, ++nonce);
-	map.set(`${j},${i}`, j);
-}
-
-this.uniq = () => ++nonce;
-this.phi = (i, j) => map.get(`${i},${j}`);
-this.match = (i, j) => {
-	if (i == j)
-		return true;
-
-	decide(i, j);
-	return false;
-};
diff --git a/encoding/closed/index.js b/encoding/closed/index.js
deleted file mode 100644
index 8a95330..0000000
--- a/encoding/closed/index.js
+++ /dev/null
@@ -1,105 +0,0 @@
-"use strict";
-
-const fs = require("fs");
-const path = require("path");
-
-const template = fs.readFileSync(path.join(__dirname, "template.txt"), "utf8");
-
-let mkwire, mktwins, getfv, rename;
-
-function psi(shared, list)
-{
-	shared.forEach((twins, atom) => {
-		const left = twins.left;
-		const right = twins.right;
-		const wire = mkwire();
-		const agent = `\\share(${atom}, ${wire})`;
-		const amb = `\\amb(${right}, ${agent}, ${wire})`;
-
-		list.push(`${left} = ${amb}`);
-	});
-}
-
-function rho(fv, root, end, list)
-{
-	fv.forEach((ref, atom) => {
-		const next = mkwire();
-		const agent = `\\bind(${next}, ${ref}, ${root})`;
-
-		list.push(`${atom} = ${agent}`);
-
-		root = next;
-	});
-
-	list.push(`${root} = ${end}`);
-}
-
-function gamma(obj, root, list)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		if (obj.free) {
-			const name = `this.mkid("${obj.name}")`;
-			const agent = `\\atom_{${name}}`;
-
-			list.push(`${root} = ${agent}`);
-		} else {
-			const name = obj.name;
-
-			list.push(`${root} = ${name}`);
-		}
-	} else if ("abst" == node) {
-		const id = obj.bound;
-		const body = obj.body;
-		const fv = getfv(body);
-		const wire = mkwire();
-		const agent = fv.has(id) ? id : "\\erase";
-		const tree = `\\lambda(${agent}, ${wire})`;
-
-		fv.delete(id);
-
-		fv.forEach((proper, atom, map) => {
-			map.set(atom, mkwire());
-		});
-
-		rename(body, fv);
-
-		rho(fv, root, tree, list);
-
-		gamma(body, wire, list);
-	} else if ("appl" == node) {
-		const wleft = mkwire();
-		const wright = mkwire();
-		const left = obj.left;
-		const right = obj.right;
-		const shared = mktwins(left, right);
-		const agent = `\\outapp(${wleft}, ${wright})`;
-
-		list.push(`${root} = ${agent}`);
-
-		gamma(left, wleft, list);
-		gamma(right, wright, list);
-
-		psi(shared, list);
-	}
-}
-
-function encode(generic, term)
-{
-	const inconfig = [
-		"\\read_{this.mkhole()}(!print) = root"
-	];
-
-	mkwire = generic.mkwire;
-	mktwins = generic.mktwins;
-	getfv = generic.getfv;
-	rename = generic.rename;
-
-	gamma(term, "root", inconfig);
-
-	inconfig.inet = template;
-	return inconfig;
-}
-
-module.exports = encode;
diff --git a/encoding/closed/template.txt b/encoding/closed/template.txt
deleted file mode 100644
index ce1df7f..0000000
--- a/encoding/closed/template.txt
+++ /dev/null
@@ -1,183 +0,0 @@
-\read_{C}[a] {
-	/* Unshare variable. */
-	this.debug.o();
-} \share[\copy(b, \read_{C}(a)), b];
-
-\copy[a, b] {
-	/* Unshare variable. */
-	this.debug.o();
-} \share[\copy(c, \copy(a, b)), c];
-
-\copy[a, b] {
-	/* Initiate application. */
-	this.debug.o();
-} \outapp[\apply(c, \copy(a, b)), c];
-
-\dup[a, b] {
-	/* Unshare variable. */
-	this.debug.o();
-} \share[\copy(c, \dup(a, b)), c];
-
-\dup[a, b] {
-	/* Initiate application. */
-	this.debug.o();
-} \outapp[\apply(c, \dup(a, b)), c];
-
-\apply[a, b] {
-	/* Unshare variable. */
-	this.debug.o();
-} \share[\copy(c, \apply(a, b)), c];
-
-\apply[a, b] {
-	/* Initiate application. */
-	this.debug.o();
-} \outapp[\apply(c, \apply(a, b)), c];
-
-\bind[a, \outapp(b, c), d] {
-	/* Inject application. */
-	this.debug.o();
-} \outapp[\bind(e, b, d), \bind(a, c, e)];
-
-\erase {
-	/* Erase sharing. */
-	this.debug.o();
-} \share[a, a];
-
-\erase {
-	/* Erase application. */
-	this.debug.o();
-} \outapp[\erase, \erase];
-
-\bind[a, \amb(b, \share(c, d), d), e] {
-	/* Inject sharing. */
-	this.debug.o();
-} \share[\bind(a, c, e), b];
-
-\read_{C}[a] {
-	/* Initiate application. */
-	this.debug.o();
-} \outapp[\apply(b, \read_{C}(a)), b];
-
-\print {
-	/* Output results of read-back. */
-	this.nf = M;
-	this.debug.o();
-} \atom_{M};
-
-\bind[a, \erase, a] {
-	/* Erase FV. */
-	this.debug.o();
-} \erase;
-
-\bind[a, \atom_{M}, a] {
-	/* Bind an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\bind[a, \lambda(b, c), a] {
-	/* Bind a closed abstraction. */
-	this.debug.o();
-} \lambda[b, c];
-
-\bind[\dup(a, b), \dup(c, d), \dup(e, f)] {
-	/* Duplicate FV. */
-	this.debug.o();
-} \dup[\bind(a, c, e), \bind(b, d, f)];
-
-\read_{C}[\dup(a, b)] {
-	/* Duplicate context. */
-	this.debug.o();
-} \dup[\read_{C}(a), \read_{this.clone(C)}(b)];
-
-\dup[a, b] {
-	/* Duplicate sharing. */
-	this.debug.o();
-} \copy[\dup(\amb(c, \share(a, d), d), \amb(e, \share(b, f), f)), \dup(c, e)];
-
-\read_{C}[a] {
-	/* Read back abstraction. */
-	this.debug.o();
-} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
-
-\apply[\read_{this.appl(M)}(a), a] {
-	/* Read back application. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\atom_{this.atom(C, M)}] {
-	/* Read back an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\copy[\atom_{M}, \atom_{M}] {
-	/* Copy an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\dup[\atom_{M}, \atom_{M}] {
-	/* Duplicate an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\apply[a, b] {
-	/* Apply a closed term. */
-	this.debug.b();
-} \lambda[a, b];
-
-\copy[\lambda(a, b), \lambda(c, d)] {
-	/* Initiate copy of a closed term. */
-	this.debug.o();
-} \lambda[\dup(a, c), \dup(b, d)];
-
-\apply[\dup(a, b), \dup(\outapp(c, a), \outapp(d, b))] {
-	/* Duplicate application. */
-	this.debug.o();
-} \dup[c, d];
-
-\dup[\lambda(a, b), \lambda(c, d)] {
-	/* Duplicate abstraction. */
-	this.debug.o();
-} \lambda[\dup(a, c), \dup(b, d)];
-
-\dup[a, b] {
-	/* Finish duplication. */
-	this.debug.o();
-} \dup[a, b];
-
-\erase {
-	/* Erase an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\erase {
-	/* Erase application. */
-	this.debug.o();
-} \apply[\erase, \erase];
-
-\erase {
-	/* Erase abstraction. */
-	this.debug.o();
-} \lambda[\erase, \erase];
-
-\erase {
-	/* Erase copy initiator. */
-	this.debug.o();
-} \copy[\erase, \erase];
-
-\erase {
-	/* Erase duplicator. */
-	this.debug.o();
-} \dup[\erase, \erase];
-
-\erase {
-	/* Finish erasing. */
-	this.debug.o();
-} \erase;
-
-$$
-
-INCONFIG
-
-$$
-
-READBACK
diff --git a/encoding/generic.js b/encoding/generic.js
deleted file mode 100644
index 176f00e..0000000
--- a/encoding/generic.js
+++ /dev/null
@@ -1,197 +0,0 @@
-"use strict";
-
-const fs = require("fs");
-const path = require("path");
-
-const readback = fs.readFileSync(path.join(__dirname, "readback.txt"), "utf8");
-let lastwire;
-
-function getcap(left, right)
-{
-	const cap = new Map();
-
-	left = getfv(left);
-	right = getfv(right);
-
-	left.forEach((proper, atom) => {
-		if (right.has(atom))
-			cap.set(atom, proper);
-	});
-
-	return cap;
-}
-
-function merge(left, right)
-{
-	left = Array.from(left);
-	right = Array.from(right);
-	return new Map(left.concat(right));
-}
-
-function getfv(obj)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		const fv = new Map();
-
-		if (!obj.free)
-			fv.set(obj.name, obj.proper);
-
-		return fv;
-	}
-
-	if ("abst" == node) {
-		const fv = getfv(obj.body);
-
-		fv.delete(obj.bound);
-
-		return fv;
-	}
-
-	if ("appl" == node) {
-		const left = getfv(obj.left);
-		const right = getfv(obj.right);
-
-		return merge(left, right);
-	}
-}
-
-function mkwire()
-{
-	++lastwire;
-	return "w" + lastwire.toFixed(0);
-}
-
-function rename(obj, map)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		const name = obj.name;
-
-		if (map.has(name))
-			obj.name = map.get(name);
-	} else if ("abst" == node) {
-		const body = obj.body;
-
-		rename(body, map);
-	} else if ("appl" == node) {
-		rename(obj.left, map);
-		rename(obj.right, map);
-	}
-}
-
-function mktwins(left, right)
-{
-	const lmap = new Map();
-	const rmap = new Map();
-	const smap = new Map();
-
-	getcap(left, right).forEach((proper, atom) => {
-		const wleft = mkwire();
-		const wright = mkwire();
-
-		lmap.set(atom, wleft);
-		rmap.set(atom, wright);
-		smap.set(atom, {
-			proper: proper,
-			left: wleft,
-			right: wright
-		});
-	});
-
-	rename(left, lmap);
-	rename(right, rmap);
-	return smap;
-}
-
-function alpha(obj, bv, lvl)
-{
-	const node = obj.node;
-	const aobj = {
-		node: node
-	};
-
-	if ("atom" == node) {
-		const name = obj.name;
-		const id = bv.get(name);
-
-		if (id) {
-			const proper = id.name;
-
-			aobj.name = proper;
-			aobj.proper = proper;
-			aobj.index = lvl - id.lvl;
-		} else {
-			aobj.name = name;
-			aobj.free = true;
-		}
-	} else if ("abst" == node) {
-		const id = obj.bound;
-		const old = bv.get(id);
-		const wire = mkwire();
-
-		bv.set(id, {
-			name: wire,
-			lvl: ++lvl
-		});
-
-		aobj.bound = wire;
-		aobj.body = alpha(obj.body, bv, lvl);
-
-		if (old)
-			bv.set(id, old);
-		else
-			bv.delete(id);
-	} else if ("appl" == node) {
-		aobj.left = alpha(obj.left, bv, lvl);
-		aobj.right = alpha(obj.right, bv, lvl);
-	}
-
-	return aobj;
-}
-
-function expand(dict)
-{
-	const orig = dict.term;
-	const term = dict.macros.reduce((acc, macro) => {
-		const fv = acc.fv;
-		const id = macro.id;
-		const def = macro.def;
-
-		if (!fv.has(id))
-			return acc;
-
-		fv.delete(id);
-
-		getfv(def).forEach((proper, atom) => {
-			fv.set(atom, proper);
-		});
-
-		acc.term = {
-			node: "appl",
-			left: {
-				node: "abst",
-				bound: id,
-				body: acc.term
-			},
-			right: def
-		};
-		return acc;
-	}, {
-		term: orig,
-		fv: getfv(orig)
-	}).term;
-
-	dict.expanded = term;
-	lastwire = 0;
-	return alpha(term, new Map(), 0);
-}
-
-exports.expand = expand;
-exports.mkwire = mkwire;
-exports.mktwins = mktwins;
-exports.getfv = getfv;
-exports.rename = rename;
-exports.readback = readback;
diff --git a/encoding/index.js b/encoding/index.js
deleted file mode 100644
index d44097e..0000000
--- a/encoding/index.js
+++ /dev/null
@@ -1,28 +0,0 @@
-"use strict";
-
-const generic = require("./generic");
-const abstract = require("./abstract");
-const closed = require("./closed");
-const optimal = require("./optimal");
-const standard = require("./standard");
-
-const map = new Map();
-const expand = generic.expand;
-const readback = generic.readback;
-const encode = algo => term => {
-	const expanded = expand(term);
-	const eqns = algo(generic, expanded);
-	const conf = eqns.join(";\n") + ";";
-	let inet = eqns.inet;
-
-	inet = inet.replace("INCONFIG", conf);
-	inet = inet.replace("READBACK\n", readback);
-	return inet;
-};
-
-map.set("abstract", encode(abstract));
-map.set("closed", encode(closed));
-map.set("optimal", encode(optimal));
-map.set("standard", encode(standard));
-
-module.exports = map;
diff --git a/encoding/optimal/index.js b/encoding/optimal/index.js
deleted file mode 100644
index c2effbf..0000000
--- a/encoding/optimal/index.js
+++ /dev/null
@@ -1,89 +0,0 @@
-"use strict";
-
-const fs = require("fs");
-const path = require("path");
-
-const template = fs.readFileSync(path.join(__dirname, "template.txt"), "utf8");
-
-let mkwire, mktwins, getfv;
-
-function psi(shared, list)
-{
-	shared.forEach((twins, atom) => {
-		const left = twins.left;
-		const right = twins.right;
-		const agent = `\\fan_{0}`;
-		const tree = `${agent}(${right}, ${left})`;
-
-		list.push(`${atom} = ${tree}`);
-	});
-}
-
-function mkscope(n, s)
-{
-	for (let i = 0; i < n; i++)
-		s = `\\scope_{0}(${s})`;
-
-	return s;
-}
-
-function gamma(obj, root, list)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		if (obj.free) {
-			const name = `this.mkid("${obj.name}")`;
-			const agent = `\\atom_{${name}}`;
-
-			list.push(`${root} = ${agent}`);
-		} else {
-			const agent = mkscope(obj.index, root);
-
-			list.push(`${obj.name} = ${agent}`);
-		}
-	} else if ("abst" == node) {
-		const id = obj.bound;
-		const body = obj.body;
-		const fv = getfv(body);
-		const wire = mkwire();
-		const agent = fv.has(id) ? id : "\\erase";
-		const tree = `\\lambda(${agent}, ${wire})`;
-
-		list.push(`${root} = ${tree}`);
-
-		gamma(body, wire, list);
-	} else if ("appl" == node) {
-		const wleft = mkwire();
-		const wright = mkwire();
-		const left = obj.left;
-		const right = obj.right;
-		const shared = mktwins(left, right);
-		const agent = `\\apply(${wright}, ${root})`;
-
-		list.push(`${wleft} = ${agent}`);
-
-		gamma(left, wleft, list);
-		gamma(right, wright, list);
-
-		psi(shared, list);
-	}
-}
-
-function encode(generic, term)
-{
-	const inconfig = [
-		"\\read_{this.mkhole()}(!print) = root"
-	];
-
-	mkwire = generic.mkwire;
-	mktwins = generic.mktwins;
-	getfv = generic.getfv;
-
-	gamma(term, "root", inconfig);
-
-	inconfig.inet = template;
-	return inconfig;
-}
-
-module.exports = encode;
diff --git a/encoding/optimal/template.txt b/encoding/optimal/template.txt
deleted file mode 100644
index a4f0c39..0000000
--- a/encoding/optimal/template.txt
+++ /dev/null
@@ -1,126 +0,0 @@
-\fan_{i}[\scope_{j}(a), \scope_{j}(b)] {
-	/* Duplicate higher delimiter. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \scope_{j}[\fan_{i}(a, b)];
-
-\scope_{i}[\fan_{j + 1}(a, b)] {
-	/* Level up higher or matching fan. */
-	if (i <= j)
-		this.debug.o();
-	else
-		return false;
-} \fan_{j}[\scope_{i}(a), \scope_{i}(b)];
-
-\scope_{i}[\scope_{j + 1}(a)] {
-	/* Level up higher delimiter. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \scope_{j}[\scope_{i}(a)];
-
-\print {
-	/* Ignore delimiter. */
-	this.debug.o();
-} \scope_{i}[!print];
-
-\read_{C}[\scope_{i}(a)] {
-	/* Pass through context. */
-	this.debug.o();
-} \scope_{i}[\read_{C}(a)];
-
-\scope_{i}[a] {
-	/* Annihilate matching delimiters. */
-	if (i == j)
-		this.debug.o();
-	else
-		return false;
-} \scope_{j}[a];
-
-\scope_{i}[\apply(a, b)] {
-	/* Pass through application. */
-	this.debug.o();
-} \apply[\scope_{i}(a), \scope_{i}(b)];
-
-\scope_{i}[\lambda(a, b)] {
-	/* Level up delimiter. */
-	this.debug.o();
-} \lambda[\scope_{i + 1}(a), \scope_{i + 1}(b)];
-
-\scope_{i}[\atom_{M}] {
-	/* Return an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\fan_{i}(a, b)] {
-	/* Duplicate context. */
-	this.debug.o();
-} \fan_{i}[\read_{C}(a), \read_{this.clone(C)}(b)];
-
-\print {
-	/* Output results of read-back. */
-	this.nf = M;
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\scope_{0}(a)] {
-	/* Read back abstraction. */
-	this.debug.o();
-} \lambda[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
-
-\apply[\read_{this.appl(M)}(a), a] {
-	/* Read back application. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\atom_{this.atom(C, M)}] {
-	/* Read back an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\fan_{i}[\atom_{M}, \atom_{M}] {
-	/* Duplicate an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\apply[\scope_{0}(a), \scope_{0}(b)] {
-	/* Apply beta reduction. */
-	this.debug.b();
-} \lambda[a, b];
-
-\fan_{i}[\apply(a, b), \apply(c, d)] {
-	/* Duplicate application. */
-	this.debug.o();
-} \apply[\fan_{i}(a, c), \fan_{i}(b, d)];
-
-\fan_{i}[\lambda(a, b), \lambda(c, d)] {
-	/* Level up fan. */
-	this.debug.o();
-} \lambda[\fan_{i + 1}(a, c), \fan_{i + 1}(b, d)];
-
-\fan_{i}[a, b] {
-	/* Annihilate matching fans. */
-	if (i == j)
-		this.debug.a();
-	else
-		return false;
-} \fan_{j}[a, b];
-
-\fan_{i}[\fan_{j}(a, b), \fan_{j}(c, d)] {
-	/* Duplicate higher fan. */
-	if (i < j)
-		this.debug.d();
-	else
-		return false;
-} \fan_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
-
-$$
-
-INCONFIG
-
-$$
-
-READBACK
diff --git a/encoding/readback.txt b/encoding/readback.txt
deleted file mode 100644
index 6b4aaed..0000000
--- a/encoding/readback.txt
+++ /dev/null
@@ -1,226 +0,0 @@
-const gfv = new Set();
-let id = 0;
-
-function mkvar(fresh)
-{
-	if (fresh)
-		++id;
-
-	return `v${id}`;
-}
-
-function mkid(name)
-{
-	const fv = new Set();
-	const obj = {
-		node: "atom",
-		fv: fv
-	};
-
-	if (name) {
-		obj.name = name;
-		gfv.add(name);
-		return obj;
-	}
-
-	do {
-		name = mkvar(true);
-	} while (gfv.has(name));
-
-	obj.name = name;
-	fv.add(name);
-	return obj;
-}
-
-function mkhole()
-{
-	const obj = {};
-
-	obj.fv = new Set();
-	obj.bv = new Set();
-	obj.hole = obj;
-	return obj;
-}
-
-function subst(hole, obj)
-{
-	const parent = hole.parent;
-	const body = obj.body;
-	const left = obj.left;
-	const right = obj.right;
-
-	if (parent)
-		obj.parent = hole.parent;
-	else
-		delete obj.parent;
-
-	Object.assign(hole, obj);
-
-	if (body)
-		body.parent = hole;
-	if (left)
-		left.parent = hole;
-	if (right)
-		right.parent = hole;
-}
-
-function eta(obj)
-{
-	let parent, left, right, name;
-
-	if ("appl" != obj.node)
-		return;
-
-	parent = obj.parent;
-	if (!parent)
-		return;
-	if ("abst" != parent.node)
-		return;
-
-	right = obj.right;
-	if ("atom" != right.node)
-		return;
-
-	name = parent.bound;
-	if (name != right.name)
-		return;
-
-	left = obj.left;
-	if (left.fv.has(name))
-		return;
-
-	subst(parent, left);
-
-	eta(parent);
-}
-
-function atom(context, obj, name)
-{
-	const ofv = obj.fv;
-	const cfv = context.fv;
-	const bv = context.bv;
-	const chole = context.hole;
-	const ohole = obj.hole;
-
-	if (name)
-		bv.add(name);
-
-	ofv.forEach(x => {
-		if (!bv.has(x))
-			cfv.add(x);
-	});
-
-	subst(chole, obj);
-
-	if (ohole) {
-		delete chole.hole;
-		context.hole = ohole;
-	} else {
-		delete context.hole;
-		eta(chole);
-	}
-
-	return context;
-}
-
-function abst(context)
-{
-	const hole = mkhole();
-	const name = mkvar();
-	const obj = {
-		node: "abst",
-		bound: name,
-		body: hole,
-		fv: new Set(),
-		hole: hole
-	};
-
-	hole.parent = obj;
-	return atom(context, obj, name);
-}
-
-function appl(left)
-{
-	const context = mkhole();
-	const hole = mkhole();
-	const obj = {
-		node: "appl",
-		left: left,
-		right: hole,
-		fv: new Set(left.fv),
-		hole: hole
-	};
-
-	left.parent = obj;
-	hole.parent = obj;
-	return atom(context, obj);
-}
-
-function clone(obj, root, hole, parent)
-{
-	const copy = {};
-
-	if (!obj)
-		return;
-
-	if (!root) {
-		root = copy;
-		hole = obj.hole;
-	}
-
-	copy.node = obj.node;
-	copy.bound = obj.bound;
-	copy.name = obj.name;
-	copy.parent = parent;
-	copy.body = clone(obj.body, root, hole, copy);
-	copy.left = clone(obj.left, root, hole, copy);
-	copy.right = clone(obj.right, root, hole, copy);
-
-	copy.fv = new Set(obj.fv);
-	copy.bv = new Set(obj.bv);
-
-	if (obj === hole)
-		root.hole = copy;
-
-	return copy;
-}
-
-this.clone = clone;
-this.mkid = mkid;
-this.mkvar = mkvar;
-this.mkhole = mkhole;
-this.abst = abst;
-this.appl = appl;
-this.atom = atom;
-
-function noop()
-{
-}
-
-this.beta = 0;
-this.total = 0;
-this.cb = Object.assign({
-	a: noop,
-	b: noop,
-	d: noop,
-	o: noop
-}, this.cb);
-this.debug = {
-	a: () => {
-		++this.total;
-		this.cb.a();
-	},
-	b: () => {
-		++this.beta;
-		++this.total;
-		this.cb.b();
-	},
-	d: () => {
-		++this.total;
-		this.cb.d();
-	},
-	o: () => {
-		++this.total;
-		this.cb.o();
-	}
-};
diff --git a/encoding/standard/index.js b/encoding/standard/index.js
deleted file mode 100644
index 048e566..0000000
--- a/encoding/standard/index.js
+++ /dev/null
@@ -1,100 +0,0 @@
-"use strict";
-
-const fs = require("fs");
-const path = require("path");
-
-const template = fs.readFileSync(path.join(__dirname, "template.txt"), "utf8");
-
-let mkwire, mktwins, getfv, rename;
-
-function box(fv, list, lvl)
-{
-	fv.forEach((ref, atom) => {
-		const agent = `\\bra_{${lvl}}(${ref})`;
-
-		list.push(`${atom} = ${agent}`);
-	});
-}
-
-function psi(shared, list, lvl)
-{
-	shared.forEach((twins, atom) => {
-		const left = twins.left;
-		const right = twins.right;
-		const agent = `\\fan_{${lvl}}`;
-		const tree = `${agent}(${right}, ${left})`;
-
-		list.push(`${atom} = ${tree}`);
-	});
-}
-
-function gamma(obj, root, list, lvl)
-{
-	const node = obj.node;
-
-	if ("atom" == node) {
-		if (obj.free) {
-			const name = `this.mkid("${obj.name}")`;
-			const agent = `\\atom_{${name}}`;
-
-			list.push(`${root} = ${agent}`);
-		} else {
-			const agent = `\\cro_{${lvl}}(${root})`;
-
-			list.push(`${obj.name} = ${agent}`);
-		}
-	} else if ("abst" == node) {
-		const id = obj.bound;
-		const body = obj.body;
-		const fv = getfv(body);
-		const wire = mkwire();
-		const agent = fv.has(id) ? id : "\\erase";
-		const tree = `\\lam_{${lvl}}(${agent}, ${wire})`;
-
-		list.push(`${root} = ${tree}`);
-
-		gamma(body, wire, list, lvl);
-	} else if ("appl" == node) {
-		const wleft = mkwire();
-		const wright = mkwire();
-		const left = obj.left;
-		const right = obj.right;
-		const shared = mktwins(left, right);
-		const agent = `\\app_{${lvl}}`;
-		const tree = `${agent}(${wright}, ${root})`;
-		const fv = getfv(right);
-
-		fv.forEach((proper, atom, map) => {
-			map.set(atom, mkwire());
-		});
-
-		rename(right, fv);
-
-		list.push(`${wleft} = ${tree}`);
-
-		gamma(left, wleft, list, lvl);
-		gamma(right, wright, list, lvl + 1);
-
-		box(fv, list, lvl);
-		psi(shared, list, lvl);
-	}
-}
-
-function encode(generic, term)
-{
-	const inconfig = [
-		"\\read_{this.mkhole()}(!print) = root"
-	];
-
-	mkwire = generic.mkwire;
-	mktwins = generic.mktwins;
-	getfv = generic.getfv;
-	rename = generic.rename;
-
-	gamma(term, "root", inconfig, 0);
-
-	inconfig.inet = template;
-	return inconfig;
-}
-
-module.exports = encode;
diff --git a/encoding/standard/template.txt b/encoding/standard/template.txt
deleted file mode 100644
index b7c6d55..0000000
--- a/encoding/standard/template.txt
+++ /dev/null
@@ -1,220 +0,0 @@
-\cro_{i}[\fan_{j - 1}(a, b)] {
-	/* Level down higher fan. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \fan_{j}[\cro_{i}(a), \cro_{i}(b)];
-
-\fan_{i}[\cro_{j}(a), \cro_{j}(b)] {
-	/* Duplicate higher croissant. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \cro_{j}[\fan_{i}(a, b)];
-
-\fan_{i}[\bra_{j}(a), \bra_{j}(b)] {
-	/* Duplicate higher bracket. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \bra_{j}[\fan_{i}(a, b)];
-
-\bra_{i}[\fan_{j + 1}(a, b)] {
-	/* Level up higher fan. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \fan_{j}[\bra_{i}(a), \bra_{i}(b)];
-
-\bra_{i}[\bra_{j + 1}(a)] {
-	/* Level up higher bracket. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \bra_{j}[\bra_{i}(a)];
-
-\cro_{i}[\cro_{j - 1}(a)] {
-	/* Level down higher bracket. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \cro_{j}[\cro_{i}(a)];
-
-\cro_{i}[\bra_{j - 1}(a)] {
-	/* Level down higher bracket. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \bra_{j}[\cro_{i}(a)];
-
-\bra_{i}[\cro_{j + 1}(a)] {
-	/* Level up higher croissant. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \cro_{j}[\bra_{i}(a)];
-
-\print {
-	/* Ignore bracket. */
-	this.debug.o();
-} \bra_{i}[\print];
-
-\read_{C}[\bra_{i}(a)] {
-	/* Pass through context. */
-	this.debug.o();
-} \bra_{i}[\read_{C}(a)];
-
-\cro_{i}[a] {
-	/* Annihilate matching croissants. */
-	if (i == j)
-		this.debug.o();
-	else
-		return false;
-} \cro_{j}[a];
-
-\bra_{i}[a] {
-	/* Annihilate matching brackets. */
-	if (i == j)
-		this.debug.o();
-	else
-		return false;
-} \bra_{j}[a];
-
-\bra_{i}[\app_{j + 1}(a, b)] {
-	/* Level up higher application. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \app_{j}[\bra_{i}(a), \bra_{i}(b)];
-
-\bra_{i}[\lam_{j + 1}(a, b)] {
-	/* Level up higher abstraction. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \lam_{j}[\bra_{i}(a), \bra_{i}(b)];
-
-\print {
-	/* Ignore croissant. */
-	this.debug.o();
-} \cro_{i}[\print];
-
-\read_{C}[\cro_{i}(a)] {
-	/* Pass through context. */
-	this.debug.o();
-} \cro_{i}[\read_{C}(a)];
-
-\cro_{i}[\app_{j - 1}(a, b)] {
-	/* Level down higher application. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \app_{j}[\cro_{i}(a), \cro_{i}(b)];
-
-\cro_{i}[\lam_{j - 1}(a, b)] {
-	/* Level down higher abstraction. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \lam_{j}[\cro_{i}(a), \cro_{i}(b)];
-
-\cro_{i}[\atom_{M}] {
-	/* Return an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\bra_{i}[\atom_{M}] {
-	/* Return an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\fan_{i}(a, b)] {
-	/* Duplicate context. */
-	this.debug.o();
-} \fan_{i}[\read_{C}(a), \read_{this.clone(C)}(b)];
-
-\print {
-	/* Output results of read-back. */
-	this.nf = M;
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[a] {
-	/* Read back abstraction. */
-	this.debug.o();
-} \lam_{i}[\atom_{this.mkid()}, \read_{this.abst(C)}(a)];
-
-\app_{i}[\read_{this.appl(M)}(a), a] {
-	/* Read back application. */
-	this.debug.o();
-} \atom_{M};
-
-\read_{C}[\atom_{this.atom(C, M)}] {
-	/* Read back an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\fan_{i}[\atom_{M}, \atom_{M}] {
-	/* Duplicate an atom. */
-	this.debug.o();
-} \atom_{M};
-
-\app_{i}[a, b] {
-	/* Annihilate matching abstraction and application. */
-	if (i != j)
-		return false;
-
-	this.debug.b();
-} \lam_{j}[a, b];
-
-\fan_{i}[\app_{j}(a, b), \app_{j}(c, d)] {
-	/* Duplicate higher application. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \app_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
-
-\fan_{i}[\lam_{j}(a, b), \lam_{j}(c, d)] {
-	/* Duplicate higher abstraction. */
-	if (i < j)
-		this.debug.o();
-	else
-		return false;
-} \lam_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
-
-\fan_{i}[a, b] {
-	/* Annihilate matching fans. */
-	if (i == j)
-		this.debug.a();
-	else
-		return false;
-} \fan_{j}[a, b];
-
-\fan_{i}[\fan_{j}(a, b), \fan_{j}(c, d)] {
-	/* Duplicate higher fan. */
-	if (i < j)
-		this.debug.d();
-	else
-		return false;
-} \fan_{j}[\fan_{i}(a, c), \fan_{i}(b, d)];
-
-$$
-
-INCONFIG
-
-$$
-
-READBACK
diff --git a/exhaust.js b/exhaust.js
new file mode 100644
index 0000000..4576ccd
--- /dev/null
+++ b/exhaust.js
@@ -0,0 +1,33 @@
+"use strict";
+
+function* sub(len, nv)
+{
+	if (len) {
+		--len;
+
+		for (const t of sub(len, nv + 1))
+			yield `(v${nv}: ${t})`;
+
+		for (let l = 0; l <= len; l++)
+			for (const t of sub(len - l, nv))
+				for (const u of sub(l, nv))
+					yield `(${t} ${u})`;
+	} else {
+		for (let i = 0; i < nv; i++)
+			yield `v${i}`;
+	}
+}
+
+function* wrap(ctx, len)
+{
+	for (const m of sub(len, 0))
+		yield ctx.replace("M", m);
+}
+
+function* exhaust(ctx, min, max)
+{
+	for (let len = min; len <= max; len++)
+		yield* wrap(ctx, len);
+}
+
+module.exports = exhaust;
diff --git a/generate.js b/generate.js
new file mode 100644
index 0000000..0058578
--- /dev/null
+++ b/generate.js
@@ -0,0 +1,12 @@
+"use strict";
+
+const exhaust = require("./exhaust");
+const fs = require("fs");
+
+const argv = process.argv;
+const max = parseInt(argv.pop());
+const min = parseInt(argv.pop());
+const ctx = argv.pop();
+
+for (const term of exhaust(ctx, min, max))
+	fs.writeSync(1, `${term}\n`);
diff --git a/grammar.jison b/grammar.jison
deleted file mode 100644
index da01267..0000000
--- a/grammar.jison
+++ /dev/null
@@ -1,41 +0,0 @@
-%lex
-
-%%
-
-"{"[^}]*"}" /* skip comment */
-"#".* /* skip comment */
-\s+ /* skip whitespace */
-
-[^{}#=;,:()\s]+ return "NAME";
-
-"=" return "=";
-";" return ";";
-"," return ",";
-":" return ":";
-"(" return "(";
-")" return ")";
-<<EOF>> return "EOF";
-
-/lex
-
-%token NAME
-
-%%
-
-text : defs term EOF {return {macros: $1, term: $2};}
-     ;
-defs : /* empty */ {$$ = [];}
-     | defs NAME '=' term ';' {$1.unshift({id: $2, def: $4}); $$ = $1;}
-     ;
-term : appl
-     | abst
-     ;
-abst : NAME ',' abst {$$ = {node: "abst", bound: $1, body: $3};}
-     | NAME ':' term {$$ = {node: "abst", bound: $1, body: $3};}
-     ;
-appl :      atom
-     | appl atom {$$ = {node: "appl", left: $1, right: $2};}
-     ;
-atom : '(' term ')' {$$ = $2;}
-     |     NAME     {$$ = {node: "atom", name: yytext};}
-     ;
diff --git a/helper.txt b/helper.txt
deleted file mode 100644
index 3349554..0000000
--- a/helper.txt
+++ /dev/null
@@ -1,62 +0,0 @@
-# Common combinators
-I = x: x;
-K = x, y: x;
-S = x, y, z: x z (y z);
-Y = (a: a a) (a, f: f (a a f));
-
-# Booleans
-T = K;
-F = K I;
-Not = p, a, b: p b a;
-And = p, q: p q F;
-Or = p, q: p T q;
-Xor = p, q: p Not I q;
-
-# Pairs/lists
-[] = K T;
-[]? = l: l (h, t: F);
-Cons = h, t, x: x h t;
-Head = l: l T;
-Tail = l: l F;
-
-# Church arithmetic
-+1 = n, f, x: f (n f x);
-+ = m, n, f, x: m f (n f x);
-* = m, n, f: m (n f);
-^ = m, n: n m;
--1 = n, f, x: n (g, h: h (g f)) (K x) I;
-- = m, n: n -1 m;
-0? = n: n (K F) T;
-
-# Church numerals
-0 = f, x: x;
-1 = f, x: f x;
-2 = +1 1;
-3 = +1 2;
-4 = ^ 2 2;
-5 = + 2 3;
-6 = * 2 3;
-7 = +1 6;
-8 = ^ 2 3;
-9 = ^ 3 2;
-10 = * 2 5;
-16 = ^ 2 4;
-20 = * 2 10;
-30 = * 3 10;
-32 = ^ 2 5;
-64 = ^ 2 6;
-100 = ^ 10 2;
-128 = ^ 2 7;
-256 = ^ 2 8;
-512 = ^ 2 9;
-1k = ^ 10 3;
-1ki = ^ 2 10;
-1m = ^ 10 6;
-1mi = ^ 2 20;
-1g = ^ 10 9;
-1gi = ^ 2 30;
-
-# Recursive functions
-FactY = Y (f, n: (0? n) 1 (* (f (-1 n)) n));
-Fact = n: n (f, i: * (f (+1 i)) i) (K 1) 1;
-Fibo = n: n (f, a, b: f (+ a b) a) F 1 0;
diff --git a/index.js b/index.js
deleted file mode 100644
index 42112f2..0000000
--- a/index.js
+++ /dev/null
@@ -1,122 +0,0 @@
-"use strict";
-
-const encoding = require("./encoding");
-const compile = require("./compile");
-const inet = require("inet-lib");
-
-const parser = new compile.Parser();
-const defalgo = "abstract";
-let expanded;
-
-function obj2mlc(obj)
-{
-	const node = obj.node;
-
-	if ("atom" == node)
-		return obj.name;
-
-	if ("abst" == node) {
-		const body = obj.body;
-		let sep;
-
-		if ("abst" == body.node)
-			sep = ", ";
-		else
-			sep = ": ";
-
-		return obj.bound + sep + obj2mlc(body);
-	}
-
-	if ("appl" == node) {
-		const left = obj.left;
-		const right = obj.right;
-		const rnode = right.node;
-		let lmlc = obj2mlc(left);
-		let rmlc = obj2mlc(right);
-
-		if ("abst" == left.node)
-			lmlc = "(" + lmlc + ")";
-
-		if (("abst" == rnode) || ("appl" == rnode))
-			rmlc = "(" + rmlc + ")";
-
-		return lmlc + " " + rmlc;
-	}
-
-	return "[ ]";
-}
-
-function mlc2in(mlc, algo, cb)
-{
-	const encode = encoding.get(algo ? algo : defalgo);
-	let insrc;
-
-	if (!encode)
-		throw `${algo}: Unknown algorithm`;
-
-	mlc = parser.parse(mlc);
-	insrc = encode(mlc);
-	expanded = mlc.expanded;
-	inet.inenv = {
-		cb: cb
-	};
-
-	return insrc;
-}
-
-function format(data)
-{
-	if (Array.isArray(data))
-		return data.toString();
-	else if ("object" == typeof data)
-		return obj2mlc(data);
-	else if ("number" == typeof data)
-		return data.toString();
-	else
-		return data;
-}
-
-function prepare(mlc, algo)
-{
-	const src = mlc2in(mlc, algo);
-
-	inet.prepare(src, format);
-}
-
-function debug()
-{
-	return inet.debug();
-}
-
-function debug0()
-{
-	return inet.debug0();
-}
-
-function debug1()
-{
-	return inet.debug1();
-}
-
-function run(mlc, algo, max, cb)
-{
-	const src = mlc2in(mlc, algo, cb);
-	const output = inet(src, max);
-
-	output.term = obj2mlc(expanded);
-
-	if (output.nf)
-		output.nf = obj2mlc(output.nf);
-
-	return output;
-}
-
-run.defalgo = defalgo;
-run.algos = Array.from(encoding.keys());
-run.prepare = prepare;
-run.debug = debug;
-run.debug0 = debug0;
-run.debug1 = debug1;
-run.mlc2in = mlc2in;
-
-module.exports = run;
diff --git a/lambda.js b/lambda.js
deleted file mode 100755
index 42f15cf..0000000
--- a/lambda.js
+++ /dev/null
@@ -1,127 +0,0 @@
-#!/usr/bin/env node
-
-"use strict";
-
-const lambda = require(".");
-const yargs = require("yargs");
-const fs = require("fs");
-const path = require("path");
-
-const helper = path.join(__dirname, "helper.txt");
-
-const opts = {
-	algo: {
-		alias: "a",
-		desc: "Select algorithm",
-		string: true
-	},
-	debug: {
-		alias: "d",
-		desc: "Evaluate step by step",
-		boolean: true
-	},
-	exec: {
-		alias: "e",
-		desc: "Process m4(1) macros",
-		boolean: true
-	},
-	file: {
-		alias: "f",
-		desc: "Read term from file",
-		boolean: true
-	},
-	inet: {
-		alias: "i",
-		desc: "Show interaction net",
-		boolean: true
-	},
-	limit: {
-		alias: "l",
-		desc: "Limit interactions",
-		number: true
-	},
-	macros: {
-		alias: "m",
-		desc: "Read macros from file",
-		string: true
-	},
-	perf: {
-		alias: "p",
-		desc: "Print benchmarks",
-		boolean: true
-	},
-	stats: {
-		alias: "s",
-		desc: "Save statistics to file",
-		string: true
-	},
-	term: {
-		alias: "t",
-		desc: "Output expanded term",
-		boolean: true
-	}
-};
-
-const argv = yargs
-	.usage("Usage: $0 [options] (<term> | -f <file>)")
-	.options(opts)
-	.demandCommand(1, 1)
-	.help()
-	.alias("help", "h")
-	.version()
-	.alias("version", "v")
-	.strict()
-	.wrap(50)
-	.argv;
-
-const macros = argv.macros ? argv.macros : helper;
-const comb = fs.readFileSync(macros, "utf8");
-
-let input = argv._[0];
-
-if (argv.file)
-	input = fs.readFileSync(input, "utf8");
-
-input = comb.concat(input);
-
-if (argv.exec) {
-	const exec = require("child_process").execSync;
-
-	input = exec("m4", {
-		encoding: "utf8",
-		input: input
-	});
-}
-
-if (argv.debug) {
-	let eqn;
-
-	lambda.prepare(input, argv.algo);
-
-	while (eqn = lambda.debug1())
-		console.info(eqn);
-} else if (argv.inet) {
-	const inet = lambda.mlc2in(input, argv.algo);
-
-	process.stdout.write(inet);
-} else {
-	const output = lambda(input, argv.algo, argv.limit);
-	const stats = JSON.stringify(output.stats, null, "\t");
-	const total = output.total;
-	const beta = output.beta;
-	const redtime = output.redtime;
-
-	if (argv.term)
-		console.warn(output.term);
-
-	if (argv.perf)
-		console.warn(`${total}(${beta}), ${redtime} ms`);
-
-	if (argv.stats)
-		fs.writeFileSync(argv.stats, stats + "\n");
-
-	if (output.nf)
-		console.info(output.nf);
-	else
-		process.exit(1);
-}
diff --git a/line.js b/line.js
new file mode 100644
index 0000000..9576a07
--- /dev/null
+++ b/line.js
@@ -0,0 +1,33 @@
+"use strict";
+
+const readline = require("readline");
+const mlc = require("@alexo/lambda");
+const fs = require("fs");
+
+const rl = readline.createInterface({
+	input: process.stdin
+});
+const argv = process.argv;
+const limit = parseInt(argv.pop());
+const algo = argv.pop();
+
+rl.on("line", term => {
+	let result;
+
+	try {
+		const output = mlc(term, algo, limit);
+		const total = output.total;
+		const beta = output.beta;
+		const stats = `${total}/${beta}`;
+		let nf = output.nf;
+
+		if (!nf)
+			nf = "?";
+
+		result = `${stats}\t${nf}`;
+	} catch (error) {
+		result = `N/A\t${error}`;
+	}
+
+	fs.writeSync(1, `${term}\t${result}\n`);
+});
diff --git a/package.json b/package.json
index 94100b3..d2572cc 100644
--- a/package.json
+++ b/package.json
@@ -1,26 +1,6 @@
 {
-	"description": "Macro Lambda Calculus",
-	"author": "Anton Salikhmetov",
-	"repository": "codedot/lambda",
-	"name": "@alexo/lambda",
-	"bin": "./lambda.js",
-	"version": "0.5.2",
-	"keywords": [
-		"lambda-calculus",
-		"pure",
-		"untyped",
-		"interaction-nets",
-		"interaction-calculus",
-		"optimal-reduction",
-		"abstract-algorithm",
-		"closed-reduction",
-		"lambdascope",
-		"api",
-		"cli"
-	],
-	"license": "MIT",
 	"dependencies": {
-		"inet-lib": "0.2.7",
-		"yargs": "6.6.0"
-	}
+		"@alexo/lambda": "0.5.0"
+	},
+	"private": true
 }
diff --git a/samples/1021.mlc b/samples/1021.mlc
deleted file mode 100644
index beec119..0000000
--- a/samples/1021.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-10 2 1
-# v1: v1
diff --git a/samples/1022i.mlc b/samples/1022i.mlc
deleted file mode 100644
index 0ccfdd6..0000000
--- a/samples/1022i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-10 2 2 I
-# v1: v1
diff --git a/samples/22210i.mlc b/samples/22210i.mlc
deleted file mode 100644
index b9490ee..0000000
--- a/samples/22210i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-2 2 2 10 I
-# v1: v1
diff --git a/samples/2222101.mlc b/samples/2222101.mlc
deleted file mode 100644
index 1bde624..0000000
--- a/samples/2222101.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-2 2 2 2 10 1
-# v1: v1
diff --git a/samples/3222i.mlc b/samples/3222i.mlc
deleted file mode 100644
index 6a9986e..0000000
--- a/samples/3222i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-3 2 2 2 I
-# v1: v1
diff --git a/samples/33-fact4.mlc b/samples/33-fact4.mlc
deleted file mode 100644
index 530187b..0000000
--- a/samples/33-fact4.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-- (^ 3 3) (Fact 4)
-# v1, v2: v1 (v1 (v1 v2))
diff --git a/samples/35-fact5.mlc b/samples/35-fact5.mlc
deleted file mode 100644
index 4227e20..0000000
--- a/samples/35-fact5.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-- (^ 5 3) (Fact 5)
-# v1, v2: v1 (v1 (v1 (v1 (v1 v2))))
diff --git a/samples/counter.mlc b/samples/counter.mlc
deleted file mode 100644
index cdd8f24..0000000
--- a/samples/counter.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-(f: f (f (x: x))) (i: (f: f (x: x) (f (x: x))) (x: (h, u: h (h u)) (y: x (i y))))
-# v1: v1
diff --git a/samples/fact100i.mlc b/samples/fact100i.mlc
deleted file mode 100644
index 0829919..0000000
--- a/samples/fact100i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-Fact 100 I
-# v1: v1
diff --git a/samples/fact1knt.mlc b/samples/fact1knt.mlc
deleted file mode 100644
index b3ba886..0000000
--- a/samples/fact1knt.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-Fact 1k Not T
-# v1, v2: v1
diff --git a/samples/facty6nt.mlc b/samples/facty6nt.mlc
deleted file mode 100644
index 2c0dbeb..0000000
--- a/samples/facty6nt.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-FactY 6 Not T
-# v1, v2: v1
diff --git a/samples/facty9i.mlc b/samples/facty9i.mlc
deleted file mode 100644
index 6d62eb0..0000000
--- a/samples/facty9i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-FactY 9 I
-# v1: v1
diff --git a/samples/fibo16nt.mlc b/samples/fibo16nt.mlc
deleted file mode 100644
index 0212707..0000000
--- a/samples/fibo16nt.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-Fibo 16 Not T
-# v1, v2: v2
diff --git a/samples/fibo20i.mlc b/samples/fibo20i.mlc
deleted file mode 100644
index 182455e..0000000
--- a/samples/fibo20i.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-Fibo 20 I
-# v1: v1
diff --git a/samples/w2eta.mlc b/samples/w2eta.mlc
deleted file mode 100644
index 22f9cb2..0000000
--- a/samples/w2eta.mlc
+++ /dev/null
@@ -1,2 +0,0 @@
-(x: x x) (x, y: (z: z (z y)) (w: x w))
-# v1, v2: v1 (v1 (v1 (v1 v2)))
diff --git a/stats.awk b/stats.awk
new file mode 100644
index 0000000..8ed6882
--- /dev/null
+++ b/stats.awk
@@ -0,0 +1,28 @@
+BEGIN {
+	FS = "\t";
+	OFS = "\t";
+
+	total = 0;
+
+	fail = 0;
+	hard = 0;
+	good = 0;
+}
+
+{
+	++total;
+
+	if ("N/A" == $2)
+		++fail;
+	else if ("?" == $3)
+		++hard;
+	else
+		++good;
+
+	if (!(total % 10000))
+		print total, good, hard, fail;
+}
+
+END {
+	print total, good, hard, fail;
+}
diff --git a/test.sh b/test.sh
deleted file mode 100644
index b22e3c0..0000000
--- a/test.sh
+++ /dev/null
@@ -1,51 +0,0 @@
-TERMF="%-9s"
-CELLF="%15s"
-SED="s/(\([0-9]*\)),.*$/\/\1/"
-OUT=`mktemp`
-ERR=`mktemp`
-
-run()
-{
-	node lambda -f $1 -a $2 -p >|$OUT 2>|$ERR
-
-	if [ $? -eq 0 -a "$(cat $OUT)" = "$3" ]; then
-		printf $CELLF "$(sed "$SED" $ERR)"
-	else
-		printf $CELLF "N/A"
-	fi
-}
-
-compare()
-{
-	term=$1
-	file=samples/$term.mlc
-	nf="$(sed -n 's/^# *//p' $file)"
-	shift 1
-
-	printf $TERMF $term
-
-	for algo; do
-		run $file $algo "$nf"
-	done
-
-	printf "\n"
-}
-
-printf "$TERMF$CELLF$CELLF$CELLF$CELLF\n" SAMPLE \
-	ABSTRACT CLOSED OPTIMAL STANDARD
-
-compare counter  abstract closed optimal standard
-compare w2eta    abstract closed optimal standard
-compare 1021     abstract closed optimal standard
-compare 22210i   abstract closed optimal STANDARD
-compare 3222i    abstract closed optimal STANDARD
-compare 1022i    abstract closed OPTIMAL STANDARD
-compare 2222101  abstract CLOSED OPTIMAL STANDARD
-compare facty6nt abstract closed optimal standard
-compare facty9i  abstract closed OPTIMAL STANDARD
-compare 33-fact4 abstract closed optimal standard
-compare fibo16nt abstract closed optimal standard
-compare fact100i abstract closed OPTIMAL STANDARD
-compare 35-fact5 abstract closed optimal STANDARD
-compare fibo20i  abstract closed optimal standard
-compare fact1knt abstract CLOSED OPTIMAL STANDARD