static AST id = L("x", "x");

static AST y = L("f", A(L("x", A("f", A("x", "x"))), L("x", A("f", A("x", "x")))));

static AST tru = L("x", "y", "x");
static AST fal = L("x", "y", "y");

static AST zero = fal;
static AST iszero = L("n", A("n", L("x", fal), tru));
static AST succ = L("n", "f", "x", A("f", A("n", "f", "x")));
static AST pred = L("n", "f", "x", A("n", L("g", "h", A("h", A("g", "f"))), L("u", "x"), id));
static AST add = L("m", "n", A("m", succ, "n"));
static AST sub = L("m", "n", A("n", pred, "m"));
static AST mul = L("m", "n", A("m", A(add, "n"), zero));

static AST not = L("b", A("b", fal, tru));
static AST or = L("a", "b", A("a", "b", fal));
static AST and = L("a", "b", A("a", tru, "b"));

static AST leq = L("m", "n", A(iszero, A(sub, "m", "n")));
static AST lt = L("m", "n", A(not, A(leq, "n", "m")));
static AST eq = L("m", "n", A(A(leq, "m", "n"), A(leq, "n", "m"), fal));

static AST pair = L("x", "y", "z", A("z", "x", "y"));
static AST fst = L("p", A("p", tru));
static AST snd = L("p", A("p", fal));
static AST nil = L("x", tru);
static AST isnil = L("p", A("p", L("x", "y", fal)));

static AST div = A(y, L("div", "q", "m", "n",
    A(A(lt, "m", "n"),
        A(pair, "q", "m"),
        A("div", A(succ, "q"), A(sub, "m", "n"), "n"))),
    0);

static AST idiv = L("m", "n", A(fst, A(div, "m", "n")));
static AST mod = L("m", "n", A(snd, A(div, "m", "n")));

static AST ilog = A(y, L("ilog", "b", "n",
    A(A(lt, "n", "b"),
        0,
        A(succ, A("ilog", "b", A(idiv, "n", "b"))))));

static AST fact = A(y, L("fact", "n",
    A(A(eq, "n", 1),
        1,
        A(mul, "n", A("fact", A(pred, "n"))))));

static AST len = A(y, L("len", "l",
    A(A(isnil, "l"),
        zero,
        A(succ, A("len", A(snd, "l"))))));

static AST nth = A(y, L("nth", "l", "i",
    A(A(iszero, "i"),
        A(fst, "l"),
        A("nth", A(snd, "l"), A(pred, "i")))));

static AST tail = A(y, L("tail", "l",
    A(A(isnil, A(snd, "l")),
        A(fst, "l"),
        A("tail", A(snd, "l")))));

static AST append = A(y, L("append", "l", "e",
    A(A(isnil, "l"),
        A(pair, "e", nil),
        A(pair, A(fst, "l"), A("append", A(snd, "l"), "e")))));

static AST concat = A(y, L("concat", "l", "m",
    A(A(isnil, "l"),
        "m",
        A(pair, A(fst, "l"), A("concat", A(snd, "l"), "m")))));

static AST reverse = A(y, L("reverse", "l",
    A(A(isnil, "l"),
        "l",
        A(append, A("reverse", A(snd, "l")), A(fst, "l")))));

static AST map = A(y, L("map", "l", "f",
    A(A(isnil, "l"),
        nil,
        A(pair,
            A("f", A(fst, "l")),
            A("map", A(snd, "l"), "f")))));

static AST yp = L("l", A(y, L("self", A(map, "self", "l"))));

static AST stoi = L("l",
    A(y,
        L("stoi", "l",
            A(A(isnil, A(snd, "l")),
                A(sub, A(fst, "l"), '0'),
                A(add,
                    A(sub,
                        A(fst, "l"),
                        '0'),
                    A(mul,
                        A("stoi", A(snd, "l")),
                        10)))),
        A(reverse, "l")));

static AST itos = L("n",
    A(reverse, A(y, L("itos", "n", A(A(iszero, A(idiv, "n", 10)),
        A(pair, A(add, "n", '0'), nil),
        A(pair, A(add, A(mod, "n", 10), '0'), A("itos", A(idiv, "n", 10))))), "n")));

static AST cat = A(y, L("m", "i", "o",
    A("i", L("j", "c",
        A(A(eq, "c", ast_church_natural('\n')),
            "o",
            A("m", "j", A("o", "c")))))));

static AST read = L("i", "n", "f",
    A(L("p", A("f", A(fst, "p"), A(snd, "p"))), A(y, L("read_1", "i", "n",
        A(A(iszero, "n"),
            A(pair, "i", nil),
            A("i", L("j", "c",
                A(L("res", A(pair,
                    A(fst, "res"),
                    A(pair,
                        "c",
                        A(snd, "res")))), A("read_1", "j", A(pred, "n"))))))),
        "i", "n")));

static AST read_line = L("i", "f",
    let("p",
        A(y, L("read_line", "i",
            A("i", L("j", "c",
                A(A(eq, "c", '\n'),
                    A(pair, "j", nil),
                    let("res",
                        A("read_line", "j"),
                        A(pair,
                            A(fst, "res"),
                            A(pair,
                                "c",
                                A(snd, "res")))))))),
            "i"),
        A("f", A(fst, "p"), A(snd, "p"))));

static AST write = A(y, L("write", "o", "l",
    A(A(isnil, "l"),
        "o",
        A("write", A("o", A(fst, "l")), A(snd, "l")))));

var term = L("i", "o",
    A(read_line, "i", L("j", "s",
        A(read_line, "j", L("k", "t",
            A(write, "o",
                A(itos, A(add,
                    A(stoi, "s"),
                    A(stoi, "t")))))))));