BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TN-95-17
       ENTRY:: March 13, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Ntyft/ntyxt Rules Reduce to Ntree Rules
        TYPE:: Technical Note
      AUTHOR:: Glabbeek, R.J. van
        DATE:: February 1995
       PAGES:: 16
    ABSTRACT:: Groote and Vaandrager introduced the tyft/tyxt format for
               Transition System Specifications (TSSs), and established that
               for each TSS in this format that is well-founded, the
               bisimulation equivalence it induces is a congruence. In this
               paper, we construct for each TSS in tyft/tyxt format an
               equivalent TSS that consists of tree rules only. As a
               corollary we can give an affirmative answer to an open
               question, namely whether the well-foundedness condition in
               the congruence theorem for tyft/tyxt can be dropped. These
               results extend to tyft/tyxt with negative premises and
               predicates.
       NOTES:: [Adminitrivia V1/Prg/19950313]
         END:: STAN//CS-TN-95-17