We show that it is decidable for any extended ground term rewrite system R whether there is a ground term rewrite system S such that the congrunce ↔ ^*_R generated by R is equal to the congruence ↔ ^*_S generated by S. If the answer is yes, then we can effectively construct such a ground term rewrite system S. We characterize congruences generated by extended ground term rewrite systems.

We introduce the ground tree transducer game (gtt game) played by Alpha and Beta. We deduce from the possibility of embedding gtt games into abstract games that for any gtt game there is either a winning Alpha-strategy or a winning Beta-strategy. We present several examples for the game, and show that any abstract game can be simulated by some gtt game 𝒢, a set S 1 of Alpha-strategies for 𝒢, and a set S 2 of Beta-strategies for 𝒢. Among several decidability and undecidability results, we show the following. It is decidable, given gtt games 𝒢 1 and 𝒢 2 , whether 𝒢 1 and 𝒢 2 are equivalent. There is no algorithm to determine, given a gtt game 𝒢 and an Alpha-strategy π, whether π is a winning Alpha-strategy. There is no algorithm to determine, given a recursive set S of gtt games, whether or not there exists a game 𝒢 ∈,; S such that Alpha has a winning strategy for 𝒢.

A ground term equation system (gtes for short) E is simple if there is no gtes E′ equivalent to E consisting of less equations than E has. Moreover, a gtes E is minimal if for each equation e ∈ E, the congruence generated by E – {e} is a proper subset of the congruence generated by E. Given a reduced ground term rewriting system R, we describe all simple gtes' E and minimal gtes' F equivalent to R. We show that for a reduced ground term rewriting system R, it is decidable whether or not there exist infinitely many simple (minimal) gtes' equivalent to R. Finally, we show that for a reduced ground term rewriting system R, and a gtes E, it is decidable if there is a simple gtes F equivalent to R such that E ⊆ F.