let rec mk_sub n i j a =
  assert (0 <= i && j < n && n >= 0);
  if i = 0 && j = n - 1 then 
    a 
  else if j < i then
    mk_eps()
  else 
    try
      (match d_interp a with
         | Sym.Const(b), [] -> 
             mk_const (Bitv.sub b i (j - i + 1))
         | Sym.Sub(m,k,l), [x] ->
             mk_sub m (k + i) (k + j) x
         | Sym.Conc(n,m), [x; y] ->
             if j < n then
               mk_sub n i j x
             else if n <= i then
               mk_sub m (i - n) (j - n) y
             else 
               (assert(i < n && n <= j);
                let t = mk_sub n i (n - 1) x in
                let u = mk_sub m 0 (j - n) y in
                  mk_conc (n - i) (j - n + 1) t u)
         | _ ->
             failwith "Bv.mk_sub: ill-formed expression")
    with
        Not_found -> 
          Term.App.mk_app (Sym.Bv.mk_sub n i j) [a]
        
and mk_conc n m a b =
  assert (0 <= n && 0 <= m);
  match n = 0, m = 0 with
    | true, true -> mk_eps()
    | true, false -> b
    | false, true -> a
    | false, false ->
        (try
           merge n m a b
         with
             Not_found -> Term.App.mk_app (Sym.Bv.mk_conc n m) [a; b])

and merge n m a b =
  match to_option d_interp a, to_option d_interp b with
    | _, Some(Sym.Conc(m1,m2), [b1;b2]) -> 
        mk_conc (n + m1) m2 (mk_conc n m1 a b1) b2
    | Some(Sym.Const(c),[]), Some(Sym.Const(d),[]) -> 
        mk_const (Bitv.append c d)
    | Some(Sym.Sub(n,i,j),[x]), Some(Sym.Sub(m,j',k), [y])
        when j' = j + 1 && Term.eq x y ->
        assert(n = m);
          mk_sub n i k x
    | Some(Sym.Conc(m1, m2), [b1; b2]), Some(Sym.Const(d), []) ->
        let c = d_const b2 in
        let n = Bitv.length d in
          mk_conc m1 (m2 + n) b1 (mk_const (Bitv.append c d))
    | _ -> 
        raise Not_found
 
and mk_conc3 n m k a b c =
  mk_conc n (m + k) a (mk_conc m k b c)

and cut n i a =
  (mk_sub n 0 (i - 1) a, mk_sub n i (n - 1) a)