YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(x0))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x0)))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

1(2(1(0(x0))))	→	2(1(0(2(1(0(1(1(2(1(x0))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

1^#(2(1(0(x0))))	→	1^#(x0)
1^#(2(1(0(x0))))	→	1^#(2(1(x0)))
1^#(2(1(0(x0))))	→	1^#(1(2(1(x0))))
1^#(2(1(0(x0))))	→	1^#(0(1(1(2(1(x0))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(1(1(2(1(x0)))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1^#(2(1(0(x0))))	→	1^#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pairs

1^#(2(1(0(x0))))	→	1^#(2(1(x0)))
1^#(2(1(0(x0))))	→	1^#(1(2(1(x0))))
1^#(2(1(0(x0))))	→	1^#(x0)

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[2(x₁)]	=	-12 · x₁ + 0
[1^#(x₁)]	=	0 · x₁ + 0
[1(x₁)]	=	0 · x₁ + 0
[0(x₁)]	=	12 · x₁ + 15

together with the usable rules

1(2(1(0(x0))))	→	2(1(0(2(1(0(1(1(2(1(x0))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(2(1(0(x0))))	→	2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(w.r.t. the implicit argument filter of the reduction pair), the pair

1^#(2(1(0(x0))))

→

1^#(x0)

remains.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.