Beta reduction

Here is a term in the lambda calculus: v((λx.yλt.t)z)(tλz.y). Beta reduce this term until you can't reduce it any farther, and input the result:

How to enter a term:
  • Use single lowercase letters, such as f, g, x, y, z, for variables.
  • For applications, write terms next to each other; so for example x y is x applied to y.
  • For abstractions, you can use \ as your lambda, so for example \x.x is the function that returns its input unmodified. Or, if you prefer, you can to copy a lambda to your clipboard, and then write λx.x instead. Binchicken doesn't care whether you use \ or λ; it's your call!
  • Finally, if you run into bugs or difficulties, please let me know! Screenshots are very much appreciated.