YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

p(0(x0))	→	s(s(0(s(s(p(x0))))))
p(s(0(x0)))	→	0(x0)
p(s(s(x0)))	→	s(p(s(x0)))
f(s(x0))	→	g(q(i(x0)))
g(x0)	→	f(p(p(x0)))
q(i(x0))	→	q(s(x0))
q(s(x0))	→	s(s(x0))
i(x0)	→	s(x0)

Proof

1 String Reversal

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

0(p(x0))	→	p(s(s(0(s(s(x0))))))
0(s(p(x0)))	→	0(x0)
s(s(p(x0)))	→	s(p(s(x0)))
s(f(x0))	→	i(q(g(x0)))
g(x0)	→	p(p(f(x0)))
i(q(x0))	→	s(q(x0))
s(q(x0))	→	s(s(x0))
i(x0)	→	s(x0)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

0^#(p(x0))	→	s^#(x0)
0^#(p(x0))	→	s^#(s(x0))
0^#(p(x0))	→	0^#(s(s(x0)))
0^#(p(x0))	→	s^#(0(s(s(x0))))
0^#(p(x0))	→	s^#(s(0(s(s(x0)))))
0^#(s(p(x0)))	→	0^#(x0)
s^#(s(p(x0)))	→	s^#(x0)
s^#(s(p(x0)))	→	s^#(p(s(x0)))
s^#(f(x0))	→	g^#(x0)
s^#(f(x0))	→	i^#(q(g(x0)))
i^#(q(x0))	→	s^#(q(x0))
s^#(q(x0))	→	s^#(x0)
s^#(q(x0))	→	s^#(s(x0))
i^#(x0)	→	s^#(x0)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pairs

0^#(s(p(x0)))	→	0^#(x0)
0^#(p(x0))	→	0^#(s(s(x0)))

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the naturals

[i(x₁)]

1	0	0	0
0	0	0	0
0	0	0	1
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[p(x₁)]

1	0	1	1
0	0	0	0
0	0	0	0
0	1	0	0

· x₁ +

0	0	0	0
1	0	0	0
0	0	0	0
0	0	0	0

[f(x₁)]

0	1	0	0
0	0	0	0
0	0	0	0
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[q(x₁)]

1	0	0	0
0	0	0	0
0	0	0	0
0	0	1	0

· x₁ +

0	0	0	0
1	0	0	0
0	0	0	0
0	0	0	0

[0^#(x₁)]

1	1	1
0	0	0
0	0	0
0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

[g(x₁)]

0	1	0	0
1	0	1	0
0	0	0	0
0	0	0	1

· x₁ +

0	0	0	0
1	0	0	0
0	0	0	0
1	0	0	0

[s(x₁)]

1	0	0	0
0	0	0	0
0	0	0	1
0	0	0	0

· x₁ +

0	0	0	0
0	0	0	0
0	0	0	0
0	0	0	0

together with the usable rules

s(s(p(x0)))	→	s(p(s(x0)))
s(f(x0))	→	i(q(g(x0)))
s(q(x0))	→	s(s(x0))
i(q(x0))	→	s(q(x0))
i(x0)	→	s(x0)
g(x0)	→	p(p(f(x0)))

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

0^#(s(p(x0)))

→

0^#(x0)

remains.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pairs

i^#(q(x0))	→	s^#(q(x0))
s^#(q(x0))	→	s^#(s(x0))
s^#(s(p(x0)))	→	s^#(x0)
s^#(q(x0))	→	s^#(x0)
s^#(f(x0))	→	i^#(q(g(x0)))
i^#(x0)	→	s^#(x0)

1.1.1.2 Reduction Pair Processor with Usable Rules

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

[i(x₁)]	=	5 · x₁ + 12
[s^#(x₁)]	=	-14 · x₁ + 0
[p(x₁)]	=	-5 · x₁ + 2
[f(x₁)]	=	-∞ · x₁ + 15
[q(x₁)]	=	5 · x₁ + 11
[i^#(x₁)]	=	-14 · x₁ + 0
[g(x₁)]	=	-∞ · x₁ + 5
[s(x₁)]	=	5 · x₁ + 8

together with the usable rules

s(s(p(x0)))	→	s(p(s(x0)))
s(f(x0))	→	i(q(g(x0)))
s(q(x0))	→	s(s(x0))
i(q(x0))	→	s(q(x0))
i(x0)	→	s(x0)
g(x0)	→	p(p(f(x0)))

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

i^#(q(x0))	→	s^#(q(x0))
s^#(q(x0))	→	s^#(s(x0))
s^#(s(p(x0)))	→	s^#(x0)
s^#(q(x0))	→	s^#(x0)
i^#(x0)	→	s^#(x0)

remain.

1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

s^#(s(p(x0)))

→

s^#(x0)

1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the arctic semiring over the integers

[s^#(x₁)]

0	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞

· x₁ +

-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞

[p(x₁)]

0	1	-∞
-∞	0	0
0	0	0
0	0	-∞

· x₁ +

0	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞
-∞	-∞	-∞	-∞

[s(x₁)]

1	0	1
-∞	0	-∞
-∞	-∞	-∞
-∞	0	0

· x₁ +

-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞
-∞	-∞	-∞

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), all pairs could be removed.

1.1.1.2.1.1.1 P is empty

There are no pairs anymore.