functor
  (C : sig type t val context : Transition.Make.t Syntax.context end) (Var : Var) ->
  sig
    type t
    type var = Transition.Var.t
    val equal : Transition.Make.t -> Transition.Make.t -> bool
    val compare : Transition.Make.t -> Transition.Make.t -> int
    val pp : Format.formatter -> Transition.Make.t -> unit
    val show : Transition.Make.t -> string
    val construct :
      C.t Syntax.formula ->
      (Transition.Make.var * C.t Syntax.term) list -> Transition.Make.t
    val assume : C.t Syntax.formula -> Transition.Make.t
    val assign : Transition.Make.var -> C.t Syntax.term -> Transition.Make.t
    val parallel_assign :
      (Transition.Make.var * C.t Syntax.term) list -> Transition.Make.t
    val havoc : Transition.Make.var list -> Transition.Make.t
    val mul : Transition.Make.t -> Transition.Make.t -> Transition.Make.t
    val add : Transition.Make.t -> Transition.Make.t -> Transition.Make.t
    val zero : Transition.Make.t
    val one : Transition.Make.t
    val widen : Transition.Make.t -> Transition.Make.t -> Transition.Make.t
    val exists :
      (Transition.Make.var -> bool) -> Transition.Make.t -> Transition.Make.t
    val is_zero : Transition.Make.t -> bool
    val is_one : Transition.Make.t -> bool
    val mem_transform : Transition.Make.var -> Transition.Make.t -> bool
    val get_transform :
      Transition.Make.var -> Transition.Make.t -> C.t Syntax.term
    val transform :
      Transition.Make.t -> (Transition.Make.var * C.t Syntax.term) BatEnum.t
    val guard : Transition.Make.t -> C.t Syntax.formula
    val interpolate :
      Transition.Make.t list ->
      C.t Syntax.formula ->
      [ `Invalid | `Unknown | `Valid of C.t Syntax.formula list ]
    val valid_triple :
      C.t Syntax.formula ->
      Transition.Make.t list ->
      C.t Syntax.formula -> [ `Invalid | `Unknown | `Valid ]
    val defines : Transition.Make.t -> Transition.Make.var list
    val uses : Transition.Make.t -> Transition.Make.var list
    val abstract_post :
      (C.t, 'abs) SrkApron.property ->
      Transition.Make.t -> (C.t, 'abs) SrkApron.property
    module Iter :
      functor (I : Iteration.Domain) ->
        sig
          type iter = C.t I.t
          val alpha : Transition.Make.t -> Transition.Make.Iter.iter
          val closure : Transition.Make.Iter.iter -> Transition.Make.t
          val star : Transition.Make.t -> Transition.Make.t
          val equal :
            Transition.Make.Iter.iter -> Transition.Make.Iter.iter -> bool
          val widen :
            Transition.Make.Iter.iter ->
            Transition.Make.Iter.iter -> Transition.Make.Iter.iter
          val join :
            Transition.Make.Iter.iter ->
            Transition.Make.Iter.iter -> Transition.Make.Iter.iter
          val pp : Format.formatter -> Transition.Make.Iter.iter -> unit
          val show : Transition.Make.Iter.iter -> string
        end
  end