YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

C(C(x0))	→	c(c(x0))
c(c(c(c(x0))))	→	x0
b(b(b(b(x0))))	→	B(B(x0))
B(B(B(B(x0))))	→	b(b(x0))
c(c(B(B(c(c(b(b(c(c(x0))))))))))	→	B(B(c(c(b(b(c(c(B(B(c(c(b(b(x0))))))))))))))
b(b(B(B(x0))))	→	x0
B(B(b(b(x0))))	→	x0
c(c(C(C(x0))))	→	x0
C(C(c(c(x0))))	→	x0

Proof

1 Rule Removal

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

[c(x₁)]	=	0 · x₁ + -∞
[B(x₁)]	=	0 · x₁ + -∞
[C(x₁)]	=	4 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞

the rules

c(c(c(c(x0))))	→	x0
b(b(b(b(x0))))	→	B(B(x0))
B(B(B(B(x0))))	→	b(b(x0))
c(c(B(B(c(c(b(b(c(c(x0))))))))))	→	B(B(c(c(b(b(c(c(B(B(c(c(b(b(x0))))))))))))))
b(b(B(B(x0))))	→	x0
B(B(b(b(x0))))	→	x0

remain.

1.1 Rule Removal

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

[c(x₁)]	=	1 · x₁ + -∞
[B(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	0 · x₁ + -∞

the rules

b(b(b(b(x0))))	→	B(B(x0))
B(B(B(B(x0))))	→	b(b(x0))
c(c(B(B(c(c(b(b(c(c(x0))))))))))	→	B(B(c(c(b(b(c(c(B(B(c(c(b(b(x0))))))))))))))
b(b(B(B(x0))))	→	x0
B(B(b(b(x0))))	→	x0

remain.

1.1.1 String Reversal

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

b(b(b(b(x0))))	→	B(B(x0))
B(B(B(B(x0))))	→	b(b(x0))
c(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b(b(c(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))))
B(B(b(b(x0))))	→	x0
b(b(B(B(x0))))	→	x0

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(b(b(b(x0))))	→	B^#(x0)
b^#(b(b(b(x0))))	→	B^#(B(x0))
B^#(B(B(B(x0))))	→	b^#(x0)
B^#(B(B(B(x0))))	→	b^#(b(x0))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	B^#(x0)
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	B^#(B(x0))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(B(B(x0)))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(B(B(x0))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b^#(c(c(B(B(x0)))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b^#(b(c(c(B(B(x0))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(b(b(c(c(B(B(x0)))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(b(b(c(c(B(B(x0))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	B^#(c(c(b(b(c(c(B(B(x0)))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	B^#(B(c(c(b(b(c(c(B(B(x0))))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(B(B(c(c(b(b(c(c(B(B(x0)))))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b^#(c(c(B(B(c(c(b(b(c(c(B(B(x0)))))))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b^#(b(c(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))))

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pairs

c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(B(B(c(c(b(b(c(c(B(B(x0)))))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(B(B(x0)))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(B(B(x0))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(b(b(c(c(B(B(x0)))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(b(b(c(c(B(B(x0))))))))
c^#(c(b(b(c(c(B(B(c(c(x0))))))))))	→	c^#(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[c(x₁)]	=	1 · x₁ + 8
[B(x₁)]	=	0 · x₁ + 3
[c^#(x₁)]	=	0 · x₁ + 0
[b(x₁)]	=	0 · x₁ + 3

together with the usable rules

b(b(b(b(x0))))	→	B(B(x0))
B(B(B(B(x0))))	→	b(b(x0))
c(c(b(b(c(c(B(B(c(c(x0))))))))))	→	b(b(c(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))))
B(B(b(b(x0))))	→	x0
b(b(B(B(x0))))	→	x0

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

c^#(c(b(b(c(c(B(B(c(c(x0))))))))))

→

c^#(c(B(B(c(c(b(b(c(c(B(B(x0))))))))))))

remains.

1.1.1.1.1.1.1 Reduction Pair Processor

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

[c(x₁)]

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

· x₁ +

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

[B(x₁)]

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

· x₁ +

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

[c^#(x₁)]

1	0	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

[b(x₁)]

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

· x₁ +

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

all pairs could be removed.

1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pairs

B^#(B(B(B(x0))))	→	b^#(x0)
b^#(b(b(b(x0))))	→	B^#(x0)
B^#(B(B(B(x0))))	→	b^#(b(x0))
b^#(b(b(b(x0))))	→	B^#(B(x0))

1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

[b^#(x₁)]	=	2 · x₁ + -∞
[B(x₁)]	=	1 · x₁ + -∞
[B^#(x₁)]	=	0 · x₁ + -∞
[b(x₁)]	=	1 · x₁ + -∞

together with the usable rules

b(b(b(b(x0))))	→	B(B(x0))
b(b(B(B(x0))))	→	x0
B(B(B(B(x0))))	→	b(b(x0))
B(B(b(b(x0))))	→	x0

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

B^#(B(B(B(x0))))

→

b^#(b(x0))

remains.

1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.