Simplified λ-evaluations

Lambda calculus is the theoretical core of functional languages; it is built on evaluating λ-expressions.

A λ-expression takes one of three forms:

1. a single constant, for example t;
2. a function definition Lv.E, where the letter L stands for λ, v is a variable (for example x) that may occur in the body E, and E is itself a λ-expression;
3. an application of a function to an argument, written (f)x, where the function f and the argument x are both λ-expressions.

An occurrence of a variable v in an expression E is bound when it lies inside the body of some sub-expression Lv.… of E. Occurrences that are not bound are unbound.

Evaluating a λ-expression produces another λ-expression, following these rules:

1. A constant evaluates to itself.
2. A function definition evaluates to itself.
3. To evaluate an application (f)x, first evaluate the function f.
   • If f evaluates to a function definition Lv.E, then the argument x is not evaluated; instead every unbound occurrence of v inside the body E is replaced by x (substitution), and the value of the application is the evaluation of the resulting body.
   • Otherwise the argument x is evaluated, and the application evaluates to (f')x', where f' and x' are the evaluated function and argument.

Variables and constants are single lowercase letters (a–z). Some evaluations never terminate, so your program must perform at most 1000 function applications (substitutions) per expression. During evaluation the current λ-expression never exceeds 10000 characters.

Worked examples follow (text after ; is a comment).

1.
  (Lx.x)y                        ; x <- y
  y

2.
  ((Lx.Ly.(x)y)Lz.z)Lq.q         ; x <- Lz.z
  (Ly.(Lz.z)y)Lq.q               ; y <- Lq.q
  (Lz.z)Lq.q                     ; z <- Lq.q
  Lq.q

The scope of the variable bound by a λ covers only the body of that λ-expression; the same name may appear elsewhere, for example:

3.
  ((Lx.x)(Ly.y)Lx.x)x
  ((Ly.y)Lx.x)x
  (Lx.x)x
  x

A body may contain unbound variables, i.e. constants:

4.
  (((Lx.Ly.q)Lz.t)r)u      ; x <- Lz.t
  ((Ly.q)r)u               ; y <- r
  (q)u

This evaluation is simplified compared with real λ-calculus: after substitution, occurrences in the argument that were previously unbound may become bound. Real λ-calculus prevents this by renaming variables, but in this problem you do not need to handle it.

5.
  ((Ly.Lx.y)x)w            ; y <- x
  (Lx.x)w
  w

Write a program that reads a set of expressions and prints the evaluation of each.

The input is a set of λ-expressions, one per line. The final line is always the single constant z. You may assume every expression is well-formed.

For each input expression, in the same order (including the final line), print the result of evaluating it on its own line. If evaluating an expression would require more than 1000 function applications, print the single word unterminated for that line instead.