fun is_b_redex (APP (LAM (x, m), n)) = true
  | is_b_redex (_)                   = false;

fun has_b_redex (APP (m, n)) = if is_b_redex (APP (m,n)) then true
                               else has_b_redex m orelse has_b_redex n
  | has_b_redex (LAM (x, m)) = has_b_redex m
  | has_b_redex (ID x)       = false;

(*Created two pattern matching functions to avoid having to write
  two different patterns for an application that is a redex, and one
  that may or may not contain a redex.*)
fun bdy (LAM (x, m)) = m;
fun var (LAM (x, m)) = x;

fun lb_reduce (APP (m, n)) = if is_b_redex (APP (m,n)) then subs n (var m) (bdy m)
                             else if has_b_redex m then APP (lb_reduce m, n)
                             else if has_b_redex n then APP (n, lb_reduce m)
                                                   else APP(m, n)
  | lb_reduce (LAM (x, m)) = lb_reduce m
  | lb_reduce (ID x)       = (ID x);

fun rb_reduce (APP (m, n)) = if is_b_redex (APP (m,n)) then subs n (var m) (bdy m)
                             else if has_b_redex n then APP (n, rb_reduce m)
                             else if has_b_redex m then APP (rb_reduce m, n)
                                                   else APP(m, n)
  | rb_reduce (LAM (x, m)) = rb_reduce m
  | rb_reduce (ID x)       = (ID x);