let rec lookup s a = 
  match a with
    | Var _ ->
        v s a
    | App(f, _) ->
        let i = Th.of_sym f in
          try 
            let x = 
              if Th.eq i Th.pprod then
                inv_pprod s a 
              else 
                inv i s a
            in
              v s x
          with 
              Not_found -> a



(** Search for largest match on rhs. For example, if a is of the form x * y and there is an equality u = x^2 * y, then inv_pprod s a returns u * x if there is no larger rhs which matches a. *)



and inv_pprod s a =           
  let rec usea acc = 
    match a with
      | App(Pp(Mult), xl) ->
          (List.fold_left 
             (fun acc' x -> 
                let (x', _) = Pp.destruct x in
                  Set.union (use Th.pprod s x') acc')
             acc xl)
      | App(Pp(Expt(_)), [x]) -> 
          use Th.pprod s x
      | _ -> 
          acc
  in
  let lookup =
    Set.fold
      (fun x acc ->
         try
           let b = apply Th.pprod s x in
             (match acc with
               | None ->        (* [lcm = p * a = q * b = q * x] *)
                   let (p, q, lcm) = Pp.lcm (a, b) in
                     if Pp.is_one p then Some(q, x, b) else None
               | Some(_, _, b') when Pp.cmp b b' <= 0 ->
                   acc
               | _ ->
                   let (p, q, lcm) = Pp.lcm (a, b) in
                     if Pp.is_one p then Some(q, x, b) else acc)
         with
             Not_found -> acc)
      (usea Set.empty)
      None
  in
    match lookup with
      | Some(q, x, _) -> 
          let a' = Pp.mk_mult q (v s x) in
            inv_pprod s a'
      | None ->
          a