How do you reduce this lambda calculus expression?

Question

How do you reduce this lambda calculus expression? I am trying to reduce NOT FALSE to TRUE with lambda calculus with the given definitions:

NOT = (λb.λx.λy.b y x)
FALSE = (λx.λy.y)
TRUE = (λx.λy.x)

Answer 1

  NOT FALSE
= { expand definitions }
  (λb.λx.λy.b y x) (λx.λy.y)
= { beta-reduce, alpha-rename to avoid capture }
  λx.λy.(λa.λb.b) y x 
= { beta-reduce inside lambda, twice }
  λx.λy.x
= { definition of TRUE }
  TRUE