Certification Problem

Input (TPDB SRS_Standard/Zantema_06/beans3)

The rewrite relation of the following TRS is considered.

b(a(a(x1)))	→	a(b(c(x1)))	(1)
c(a(x1))	→	a(c(x1))	(2)
b(c(a(x1)))	→	a(b(c(x1)))	(3)
c(b(x1))	→	d(x1)	(4)
a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
L(a(a(x1)))	→	L(a(b(c(x1))))	(7)
c(R(x1))	→	c(b(R(x1)))	(8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(a(a(x1)))	→	a^#(b(c(x1)))	(9)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(a(a(x1)))	→	c^#(x1)	(11)
c^#(a(x1))	→	a^#(c(x1))	(12)
c^#(a(x1))	→	c^#(x1)	(13)
b^#(c(a(x1)))	→	a^#(b(c(x1)))	(14)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	c^#(x1)	(16)
c^#(b(x1))	→	d^#(x1)	(17)
a^#(d(x1))	→	d^#(a(x1))	(18)
a^#(d(x1))	→	a^#(x1)	(19)
d^#(x1)	→	b^#(a(x1))	(20)
d^#(x1)	→	a^#(x1)	(21)
L^#(a(a(x1)))	→	L^#(a(b(c(x1))))	(22)
L^#(a(a(x1)))	→	a^#(b(c(x1)))	(23)
L^#(a(a(x1)))	→	b^#(c(x1))	(24)
L^#(a(a(x1)))	→	c^#(x1)	(25)
c^#(R(x1))	→	c^#(b(R(x1)))	(26)
c^#(R(x1))	→	b^#(R(x1))	(27)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

L^#(a(a(x1)))

→

L^#(a(b(c(x1))))

(22)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁
[a(x₁)]	=	1 · x₁
[b(x₁)]	=	1 · x₁
[d(x₁)]	=	1 · x₁
[R(x₁)]	=	1 · x₁
[L^#(x₁)]	=	1 · x₁

together with the usable rules

c(a(x1))	→	a(c(x1))	(2)
c(b(x1))	→	d(x1)	(4)
c(R(x1))	→	c(b(R(x1)))	(8)
a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
b(a(a(x1)))	→	a(b(c(x1)))	(1)
b(c(a(x1)))	→	a(b(c(x1)))	(3)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[L^#(x₁)]	=	-2 + x₁
[a(x₁)]	=	2 + x₁
[b(x₁)]	=	-2 + x₁
[c(x₁)]	=	2 + x₁
[d(x₁)]	=	x₁
[R(x₁)]	=	0

the pair

L^#(a(a(x1)))

→

L^#(a(b(c(x1))))

(22)

could be deleted.

1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

a^#(d(x1))	→	d^#(a(x1))	(18)
d^#(x1)	→	b^#(a(x1))	(20)
b^#(a(a(x1)))	→	a^#(b(c(x1)))	(9)
a^#(d(x1))	→	a^#(x1)	(19)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(a(a(x1)))	→	c^#(x1)	(11)
c^#(a(x1))	→	a^#(c(x1))	(12)
c^#(a(x1))	→	c^#(x1)	(13)
c^#(b(x1))	→	d^#(x1)	(17)
d^#(x1)	→	a^#(x1)	(21)
c^#(R(x1))	→	c^#(b(R(x1)))	(26)
b^#(c(a(x1)))	→	a^#(b(c(x1)))	(14)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	c^#(x1)	(16)

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁
[a(x₁)]	=	1 · x₁
[b(x₁)]	=	1 · x₁
[d(x₁)]	=	1 · x₁
[R(x₁)]	=	1 · x₁
[d^#(x₁)]	=	1 · x₁
[a^#(x₁)]	=	1 · x₁
[b^#(x₁)]	=	1 · x₁
[c^#(x₁)]	=	1 · x₁

together with the usable rules

c(a(x1))	→	a(c(x1))	(2)
c(b(x1))	→	d(x1)	(4)
c(R(x1))	→	c(b(R(x1)))	(8)
a(d(x1))	→	d(a(x1))	(5)
d(x1)	→	b(a(x1))	(6)
b(a(a(x1)))	→	a(b(c(x1)))	(1)
b(c(a(x1)))	→	a(b(c(x1)))	(3)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.2.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a^#(x₁)]	=	1 + 1 · x₁
[d(x₁)]	=	1 + 1 · x₁
[d^#(x₁)]	=	1 + 1 · x₁
[a(x₁)]	=	1 + 1 · x₁
[b^#(x₁)]	=	1 · x₁
[b(x₁)]	=	1 · x₁
[c(x₁)]	=	1 + 1 · x₁
[c^#(x₁)]	=	1 + 1 · x₁
[R(x₁)]	=	1 + 1 · x₁

the pairs

a^#(d(x1))	→	a^#(x1)	(19)
b^#(a(a(x1)))	→	b^#(c(x1))	(10)
b^#(a(a(x1)))	→	c^#(x1)	(11)
c^#(a(x1))	→	c^#(x1)	(13)
b^#(c(a(x1)))	→	b^#(c(x1))	(15)
b^#(c(a(x1)))	→	c^#(x1)	(16)

could be deleted.

1.1.2.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

d^#(x1) → b^#(a(x1)) (20)

b^#(a(a(x1))) → a^#(b(c(x1))) (9)

a^#(d(x1)) → d^#(a(x1)) (18)

d^#(x1) → a^#(x1) (21)

b^#(c(a(x1))) → a^#(b(c(x1))) (14)

1.1.2.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[d^#(x₁)] = 1 · x₁

[b^#(x₁)] = 0

[a(x₁)] = 1 · x₁

[a^#(x₁)] = 1 · x₁

[b(x₁)] = 0

[c(x₁)] = 0

[d(x₁)] = 1 + 1 · x₁

[R(x₁)] = 1 + 1 · x₁

together with the usable rules

d(x1) → b(a(x1)) (6)

b(a(a(x1))) → a(b(c(x1))) (1)

a(d(x1)) → d(a(x1)) (5)

b(c(a(x1))) → a(b(c(x1))) (3)

(w.r.t. the implicit argument filter of the reduction pair), the pair
a^#(d(x1)) → d^#(a(x1)) (18)
could be deleted.
1.1.2.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

Certification Problem

Input (TPDB SRS_Standard/Zantema_06/beans3)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1 Reduction Pair Processor

1.1.1.1.1 P is empty

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.2.1 Reduction Pair Processor

1.1.2.1.1 Dependency Graph Processor

1.1.2.1.1.1 Reduction Pair Processor with Usable Rules

1.1.2.1.1.1.1 Dependency Graph Processor