================================================================================
P9605   P.R. D'Argenio & C. Verhoef
        "A general conservative extension theorem in process algebras with
         inequalities"


We prove a general conservative extension theorem for transition system
based process theories with easy-to-check and reasonable conditions.
The core of this result is another general theorem which gives sufficient
conditions for a system of operational rules and an extension of it in
order to ensure conservativity, that is, provable transitions from an
original term in the extension are the same as in the original system.
As a simple corollary of the conservative extension theorem we prove a
completeness theorem.  We also prove a general theorem giving sufficient
conditions to reduce the question of ground confluence modulo some
equations for a large term rewriting system associated with an equational
process theory to a small term rewriting system under the condition that
the large system is a conservative extension of the small one.  We provide
many applications to show that our results are useful.  The applications
include (but are not limited to) various real and discrete time settings
in ACP, ATP, and CCS and the notions projection, renaming, state
operator, priority, recursion, the silent step, autonomous actions,
the empty process, divergence, etc.