The TRS could be proven non-terminating. The proof took 571 ms.

The following reduction sequence is a witness for non-termination:

+#(1, ___x) →* +#(1, ___x)

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor ForwardNarrowing (3ms).
 |    | – Problem 3 was processed with processor BackwardInstantiation (2ms).
 |    |    | – Problem 4 was processed with processor BackwardInstantiation (2ms).
 |    |    |    | – Problem 5 was processed with processor BackwardInstantiation (1ms).
 |    |    |    |    | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

+#(1, x)+#(+(0, 1), x)+#(1, x)+#(0, 1)

Rewrite Rules

+(1, x)+(+(0, 1), x)+(0, x)x

Original Signature

Termination of terms over the following signature is verified: 1, 0, +

Strategy


Parameters


The following SCCs where found

+#(1, x) → +#(+(0, 1), x)

Problem 2: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

+#(1, x)+#(+(0, 1), x)

Rewrite Rules

+(1, x)+(+(0, 1), x)+(0, x)x

Original Signature

Termination of terms over the following signature is verified: 1, 0, +

Strategy


Parameters


The right-hand side of the rule +#(1, x) → +#(+(0, 1), x) is 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
+#(1, x) 
Thus, the rule +#(1, x) → +#(+(0, 1), x) is replaced by the following rules:
+#(1, x) → +#(1, x)

Problem 3: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

+#(1, x)+#(1, x)

Rewrite Rules

+(1, x)+(+(0, 1), x)+(0, x)x

Original Signature

Termination of terms over the following signature is verified: 1, 0, +

Strategy


Instantiation

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

Problem 4: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

+#(1, _x)+#(1, _x)

Rewrite Rules

+(1, x)+(+(0, 1), x)+(0, x)x

Original Signature

Termination of terms over the following signature is verified: 1, 0, +

Strategy


Instantiation

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

Problem 5: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

+#(1, __x)+#(1, __x)

Rewrite Rules

+(1, x)+(+(0, 1), x)+(0, x)x

Original Signature

Termination of terms over the following signature is verified: 1, 0, +

Strategy


Instantiation

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