let rec isolate y ((a, b) as e) =
  assert(Term.subterm y (mk_sub a b));
  if Term.is_var a then
    if Term.eq y a then
      if Term.subterm y b then
        isolate_in_unsolved y e
      else 
        e
    else 
      if Term.subterm y b then
        isolate_in_unsolved y e
      else 
        isolate_in_solved y e
  else 
    isolate_in_unsolved y e
  


(** Isolate y in a solved equality x = a. *)


and isolate_in_solved y (x, a) = 
  assert (Term.subterm y a && not(Term.subterm x a));    
  let (p, pre, q, y, post) = destructure y a in 
    assert(not(Q.is_zero q)); (* [p + pre + q * y + post = x]. *)
    let b = mk_multq (Q.inv q) (mk_sub x (mk_addq p (mk_addl (pre @ post)))) in
      (y, b)             

and isolate_in_unsolved x ((a, b) as e) =
  assert(Term.subterm x a || Term.subterm x b);
  let a_sub_b = mk_sub a b in
    assert(not(is_num a_sub_b));
    let (p, pre, q, x, post) = destructure x a_sub_b in
      assert(not(Q.is_zero q));    (* [p + pre + q*x + post = 0] *)
      let c = mk_multq (Q.minus (Q.inv q)) 
                (mk_addq p (mk_addl (pre @ post))) 
      in
        (x, c)
    
   


(** Decompose a into pre + q * y + post. *)


and destructure y a =
  let rec loop pre post =     (* [pre + post = 0]. *)
    match post with
      | [m] ->
          let q = coefficient_of_mono m
          and y' = variable_of_mono m in
            if Term.eq y y' then
              (pre, q, y, [])
            else 
              raise Not_found
      | m :: post' ->
          let q = coefficient_of_mono m
          and y' = variable_of_mono m in
            if Term.eq y y' then
              (pre, q, y, post')
            else 
              loop (m :: pre) post'
      | [] ->
          raise Not_found
  in      
  let p = constant_of a
  and ml = nonconstant_monomials_of a in
  let (pre, q, y, post) = loop [] ml in
    (p, pre, q, y, post)