YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (15ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

i#(.(x, y)) → i#(x)i#(.(x, y)) → i#(y)
.#(.(x, y), z) → .#(y, z)i#(.(x, y)) → .#(i(y), i(x))
.#(.(x, y), z) → .#(x, .(y, z))

Rewrite Rules

.(1, x) → x.(x, 1) → x
.(i(x), x) → 1.(x, i(x)) → 1
i(1) → 1i(i(x)) → x
.(i(y), .(y, z)) → z.(y, .(i(y), z)) → z
.(.(x, y), z) → .(x, .(y, z))i(.(x, y)) → .(i(y), i(x))

Original Signature

Termination of terms over the following signature is verified: 1, ., i

Strategy

The following SCCs where found

.#(.(x, y), z) → .#(y, z).#(.(x, y), z) → .#(x, .(y, z))
i#(.(x, y)) → i#(x)i#(.(x, y)) → i#(y)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

.#(.(x, y), z) → .#(y, z).#(.(x, y), z) → .#(x, .(y, z))

Rewrite Rules

.(1, x) → x.(x, 1) → x
.(i(x), x) → 1.(x, i(x)) → 1
i(1) → 1i(i(x)) → x
.(i(y), .(y, z)) → z.(y, .(i(y), z)) → z
.(.(x, y), z) → .(x, .(y, z))i(.(x, y)) → .(i(y), i(x))

Original Signature

Termination of terms over the following signature is verified: 1, ., i

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

.#(.(x, y), z) → .#(y, z).#(.(x, y), z) → .#(x, .(y, z))

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

i#(.(x, y)) → i#(x)i#(.(x, y)) → i#(y)

Rewrite Rules

.(1, x) → x.(x, 1) → x
.(i(x), x) → 1.(x, i(x)) → 1
i(1) → 1i(i(x)) → x
.(i(y), .(y, z)) → z.(y, .(i(y), z)) → z
.(.(x, y), z) → .(x, .(y, z))i(.(x, y)) → .(i(y), i(x))

Original Signature

Termination of terms over the following signature is verified: 1, ., i

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

i#(.(x, y)) → i#(x)i#(.(x, y)) → i#(y)