let rec mk_expt n a = 
  if n = 0 then                     (* [a^0 = 1] *)
    mk_one
  else if n = 1 then                (* [a^1 = a] *)
    a
  else 
    match a with
      | App(Pp(Expt(m)), [x]) ->    (* [x^m^n = x^(m * n)] *)
          mk_expt (m * n) x
      | App(Pp(Mult), []) ->        (* [1^n = 1] *)
          mk_one
      | App(Pp(Mult), [x]) -> 
          mk_app (expt n) [x]
      | App(Pp(Mult), xl) ->        (* [(x1*...*xk)^n = x1^n*...*...xk^n] *)
          mk_multl (mapl (mk_expt n) xl)
      | _ ->
          mk_app (expt n) [a]
      
and mk_multl al =
  List.fold_left mk_mult mk_one al

and mk_mult a b =
  match a with
    | App(Pp(Expt(n)), [x]) ->
        mk_mult_with_expt x n b
    | App(Pp(Mult), []) ->
        b
    | App(Pp(Mult), xl) ->
        mk_mult_with_pp xl b
    | _ ->
        mk_mult_with_expt a 1 b

and mk_mult_with_expt x n b =
  match b with
    | App(Pp(Expt(m)), [y]) 
        when Term.eq x y ->  (* [x^n * x*m = x^(n + m)] *)
        mk_expt (n + m) x
    | App(Pp(Mult), []) ->   (* [x^n * 1 = x^n] *)
        mk_expt n x
    | App(Pp(Mult), yl) -> (* [x^n * (y1 * ... * yk) = (y1*...x^n...*yk)] *)
        insert x n yl
    | _ ->
        insert x n [b]

and mk_mult_with_pp xl b =
  match b with
    | App(Pp(Expt(m)), [y]) -> (* [(x1*...*xk) * y^m = (x1*...y^m*...*xk)] *)
        insert y m xl
    | App(Pp(Mult), yl) ->
        merge yl xl 
    | _ ->
        insert b 1 xl

and cmp1 (x, n) (y, m) =
  let res = Term.cmp x y in
    if res = 0 then Pervasives.compare n m else res

and destruct a =
  match a with
    | App(Pp(Expt(n)), [x]) -> (x, n)
    | _ -> (a, 1)


and insert x n bl =
  merge [mk_expt n x] bl

and insert1 x = insert x 1

and merge al bl =
  let compare a b = cmp1 (destruct a) (destruct b) in
  let rec loop acc al bl = 
    match al, bl with
      | [], [] -> acc
      | _, [] -> acc @ al   (* needs to be sorted. *)
      | [], _ -> acc @ bl
      | a :: al', b :: bl' ->
          let (x, n) = destruct a 
          and (y, m) = destruct b in
          let cmp = Term.cmp x y in
            if cmp = 0 then
              if n + m = 0 then
                loop acc al'  bl'
              else 
                loop (mk_expt (n + m) x :: acc) al' bl'
            else if cmp < 0 then
              loop (a :: acc)  al' bl
            else 
              loop (b :: acc) al bl'
  in
  match loop [] al bl with
    | [] -> mk_one
    | [c] -> c
    | cl -> mk_app mult (List.sort compare cl)