Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/167742)

The rewrite relation of the following TRS is considered.

There are 110 ruless (increase limit for explicit display).

Prove or disprove termination.

Yes.

Using the flat contexts

{0(☐), 1(☐), 2(☐)}

We obtain the transformed TRS

There are 218 ruless (increase limit for explicit display).

Root-labeling is applied.

We obtain the labeled TRS

There are 654 ruless (increase limit for explicit display).

Using the linear polynomial interpretation over the naturals

all of the following rules can be deleted.

There are 649 ruless (increase limit for explicit display).

Using the linear polynomial interpretation over the naturals

all of the following rules can be deleted.

0₀(0₁(1₀(0₁(1₁(1₁(1₂(2₀(0₁(1₀(0₀(0₀(0₀(0₂(2₁(1₂(2₀(0₂(2₁(1₀(0₂(2₁(1₂(2₁(1₀(0₁(1₁(1₀(0₁(x1)))))))))))))))))))))))))))))	→	0₁(1₁(1₀(0₁(1₀(0₁(1₀(0₀(0₀(0₀(0₀(0₁(1₂(2₂(2₁(1₀(0₁(1₂(2₁(1₂(2₂(2₀(0₁(1₀(0₀(0₁(1₂(2₁(1₁(x1)))))))))))))))))))))))))))))	(422)
1₂(2₀(0₂(2₁(1₁(1₀(0₂(2₂(2₂(2₂(2₂(2₀(0₁(1₂(2₀(0₁(1₁(1₀(0₀(0₁(1₀(0₁(1₂(2₂(2₁(1₂(2₂(2₀(0₁(x1)))))))))))))))))))))))))))))	→	1₀(0₂(2₀(0₂(2₂(2₀(0₀(0₁(1₁(1₁(1₁(1₂(2₁(1₂(2₂(2₂(2₁(1₀(0₀(0₀(0₀(0₁(1₂(2₀(0₁(1₂(2₁(1₀(0₁(1₁(1₁(x1)))))))))))))))))))))))))))))))	(914)

Using the linear polynomial interpretation over the naturals

all of the following rules can be deleted.

There are no rules in the TRS. Hence, it is terminating.