YES

The TRS could be proven terminating. The proof took 610 ms.

The following DP Processors were used


Problem 1 was processed with processor BackwardInstantiation (2ms).
 | – Problem 2 was processed with processor BackwardInstantiation (1ms).
 |    | – Problem 5 was processed with processor Propagation (2ms).
 | – Problem 3 was processed with processor BackwardsNarrowing (1ms).
 |    | – Problem 4 was processed with processor BackwardInstantiation (1ms).

Problem 1: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

g#(0, 1, x)f#(x, x, x)f#(x, y, z)g#(x, y, z)

Rewrite Rules

f(x, y, z)g(x, y, z)g(0, 1, x)f(x, x, x)
abac

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, b, c, a

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(x, y, z) → g#(x, y, z) on dependency pair chains it holds that: Thus, f#(x, y, z) → g#(x, y, z) is replaced by instances determined through the above matching. These instances are:
f#(_x, _x, _x) → g#(_x, _x, _x)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

g#(0, 1, x)f#(x, x, x)f#(_x, _x, _x)g#(_x, _x, _x)

Rewrite Rules

f(x, y, z)g(x, y, z)g(0, 1, x)f(x, x, x)
abac

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, b, c, a

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(_x, _x, _x) → g#(_x, _x, _x) on dependency pair chains it holds that: Thus, f#(_x, _x, _x) → g#(_x, _x, _x) is replaced by instances determined through the above matching. These instances are:
f#(x, x, x) → g#(x, x, x)

Problem 5: Propagation



Dependency Pair Problem

Dependency Pairs

g#(0, 1, x)f#(x, x, x)f#(x, x, x)g#(x, x, x)

Rewrite Rules

f(x, y, z)g(x, y, z)g(0, 1, x)f(x, x, x)
abac

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, b, c, a

Strategy


The dependency pairs g#(0, 1, x) → f#(x, x, x) and f#(x, x, x) → g#(x, x, x) are consolidated into the rule g#(0, 1, x) → g#(x, x, x) .

This is possible as

The dependency pairs g#(0, 1, x) → f#(x, x, x) and f#(x, x, x) → g#(x, x, x) are consolidated into the rule g#(0, 1, x) → g#(x, x, x) .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
g#(0, 1, x) → f#(x, x, x)g#(0, 1, x) → g#(x, x, x)
f#(x, x, x) → g#(x, x, x) 

Problem 3: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

g#(0, 1, x)f#(x, x, x)f#(_x, _x, _x)g#(_x, _x, _x)

Rewrite Rules

f(x, y, z)g(x, y, z)g(0, 1, x)f(x, x, x)
abac

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, b, c, a

Strategy


The left-hand side of the rule g#(0, 1, x) → f#(x, x, x) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
Thus, the rule g#(0, 1, x) → f#(x, x, x) is deleted.

Problem 4: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x, _x, _x)g#(_x, _x, _x)

Rewrite Rules

f(x, y, z)g(x, y, z)g(0, 1, x)f(x, x, x)
abac

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, b, c, a

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(_x, _x, _x) → g#(_x, _x, _x) on dependency pair chains it holds that: Thus, f#(_x, _x, _x) → g#(_x, _x, _x) is replaced by instances determined through the above matching. These instances are: