title: Is the following a legit successor function for lambda calculus ? (Church Numeral)
body: <p>I have read from the books that, the successor for Church Numerals is of the form:
  (\lambda n f x. f (n f x) )</p>
  
  <p>Last night I came up with this:
  (\lambda a b c. (a b) (b c) )</p>
  
  <p>I believe it also performs the functionality of a successor function. However I am not 100% positive my reductions are correct. Can someone examine it and tell me?</p>
  
  <p>The following is my reduction: let a church numeral be (\lambda f x. f^n x), where f^n x is actually a short version of (f(f(f(f...(x)))..  It represents the number n. The expected result should be n+1, that is (\lambda f x. f^{n+1} x)</p>
  
  <p>(\lambda a b c. (a b) (b c) )(\lambda f x. f^n x)</p>
  
  <p>= (\lambda b c. ( (\lambda f x. f^n x) b) (b c) )  // a replaced</p>
  
  <p>= (\lambda b c. ( (\lambda x. b^n x) (b c) )       // f replaced</p>
  
  <p>= (\lambda b c. ( (\lambda x. b^n x) (b c) ) // not 100% sure, can I replace x with (b c)?</p>
  
  <p>= (\lambda b c. ( b^n (b c) )  </p>
  
  <p>= (\lambda b c. ( b^(n+1) c )  </p>
  
  <p>Is this reduction correct, especially from step 3 to 4?
  Thanks!</p>