let rec atom (s, a) =
    Trace.call "rule" "Abst" a Atom.pp;
    let (s', a') = match a with
      | Atom.True -> (s, Atom.True)  
      | Atom.False -> (s, Atom.False)
      | Atom.Equal(x, y) -> equal s (x, y)
      | Atom.Diseq(x, y) -> diseq s (x, y)
      | Atom.In(x, d) -> cnstrnt s (x, d)
    in
      Trace.exit "rule" "Abst" a' Atom.pp;
      (s', a')

  and equal s (a, b) =
    match a, b with
      | Var _, Var _ -> 
          (s, Atom.mk_equal (a, b))
      | Var _, App(f, _) ->
          let i = Th.of_sym f in
          let (s', y') = term i (s, b) in
            let e' = Atom.mk_equal (a, y') in
              (s', e')
      | App(f, _), Var _ ->
          let i = Th.of_sym f in
          let (s', x') = term i (s, a) in
          let e' = Atom.mk_equal (b, x') in
            (s', e')
      | App(f, _), App(g, _) -> 
          let i = Th.of_sym f and j = Th.of_sym g in
          let (i', j') = 
            if Th.eq i j then (i, i) 
            else if Th.is_fully_interp i && not(Th.is_fully_interp j) then (i, u)
            else if not(Th.is_fully_interp i) && Th.is_fully_interp j then (u, j)
            else (u, u)
          in
          let (s', x') = term i' (s, a) in
          let (s'', y') = term j' (s', b) in
          let e' = Atom.mk_equal (x', y') in
            (s'', e')

  and diseq s (a, b) =
    let (s', x') = term Th.u (s, a) in
    let (s'', y') = term Th.u (s', b) in
    let d' = Atom.mk_diseq (x', y') in
      (s'', d')

  and cnstrnt s (a, i) =
    let (s', x') = term Th.la (s, a) in
    let l' = Atom.mk_in  (x', i) in
      (s', l')

  and term i (s, a) =
    match a with
      | Var _ -> 
          (s, a)
      | App(f, al) ->
          let j = Th.of_sym f in
          let (s', al') = args j (s, al) in
          let a' = if Term.eql al al' then a else sigma s f al' in
            if not(Th.is_fully_interp i) || i <> j then
              try
                let x' = inv j s' a' in
                  (s', v s' x')
              with 
                  Not_found -> name j (s', a')
            else 
              (s', a')
            
  and args i (s, al) =
    match al with
      | [] -> 
          (s, [])
      | b :: bl ->
          let (s', bl') = args i (s, bl) in
          let (s'', b') = term i (s', b) in
            if Term.eq b b' && bl == bl' then
              (s'', al)
            else 
              (s'', b' :: bl')