Relation Transition Systems (RTSs) have recently been proposed as a
foundation for reasoning effectively about program equivalence in
higher-order imperative languages like ML.  RTSs fruitfully synthesize
the coinductive style of bisimulation-based methods with the treatment
of local state in recent work on step-indexed Kripke logical relations
(SKLRs).  Like SKLRs, RTSs are designed to have the potential to scale
to inter-language reasoning; but unlike SKLRs, RTS proofs are also
transitively composable, which is of critical importance for
applications such as multi-stage verified compilation.

In a POPL'12 paper, we presented the first RTS model for an ML-like
core language, Fmuref, supporting higher-order functions, recursive
types, abstract types, and general mutable references, and we proved
soundness of the model w.r.t. contextual equivalence.  In addition, we
briefly sketched the proof that RTSs are transitively composable, but
our proof only covered a restricted fragment of the language/model
omitting abstract types and mutable state.  Here, we present the
transitivity proof for the full RTS model of the full Fmuref language.
The proof is highly intricate and requires a number of technical
innovations.  We have mechanized all our results in Coq.