Problem implementing NOR. Variable capture bug.

[15joeybloom]

I was going through the tutorial and had trouble implementing NOR. My trouble is because there is a bug in the evaluation of this expression:

1. (λc.λd.λa.λb.(λf.λb.cf(dfb))ba)(λa.λb.a)(λa.λb.a)
2. (λd.λa.λb.(λf.λb.(λa.λb.a)f(dfb))ba)(λa.λb.a)
3. λa.λb.(λf.λb.(λa.λb.a)f((λa.λb.a)fb))ba
4. λa.λb.(λε₁.(λa.λε₁.a)b((λa.λε₁.a)bε₁))a
5. λa.λb.(λε₁.λε₂.a)b((λε₁.λε₂.a)ba)
6. λa.λb.(λε₂.a)((λε₁.λε₂.a)ba)
7. λa.λb.a

The bug is in the reduction of step 4 to step 5. The correct reduction should be:

4. λa.λb.(λε₁.(λa.λε₁.a)b((λa.λε₁.a)bε₁))a
5. λa.λb.(λa.λε₁.a)b((λa.λε₁.a)ba)
6. λa.λb.(λε₁.b)((λa.λε₁.a)ba)
7. λa.λb.b

[evinism]

Has a variable capture bug really been hiding in here this whole time? Excuse my language but holy hell that's insane. Thank you for finding this.

[evinism]

Test for failing case added in #93