Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z28)

The rewrite relation of the following TRS is considered.

f(f(0,x),1) → f(g(f(x,x)),x) (1)
f(g(x),y) → g(f(x,y)) (2)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(f(0,x),1) → f#(g(f(x,x)),x) (3)
f#(f(0,x),1) → f#(x,x) (4)
f#(g(x),y) → f#(x,y) (5)

1.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[f#(x1, x2)] =
0
+
0
· x1 +
-∞
· x2
[f(x1, x2)] =
1
+
0
· x1 +
1
· x2
[0] =
0
[1] =
0
[g(x1)] =
-∞
+
0
· x1
the pair
f#(f(0,x),1) → f#(x,x) (4)
could be deleted.

1.1.1.1 Forward Instantiation Processor

We instantiate the pair to the following set of pairs
f#(g(f(0,y_0)),1) → f#(f(0,y_0),1) (6)
f#(g(g(y_0)),x1) → f#(g(y_0),x1) (7)

1.1.1.1.1 Narrowing Processor

We consider all narrowings of the pair below position ε to get the following set of pairs
f#(f(0,g(x0)),1) → f#(g(g(f(x0,g(x0)))),g(x0)) (8)

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(1) = 1 weight(1) = 1
prec(g) = 0 weight(g) = 1
in combination with the following argument filter

π(f#) = 2
π(1) = []
π(g) = []

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair
f#(f(0,g(x0)),1) → f#(g(g(f(x0,g(x0)))),g(x0)) (8)
could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.