Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/Ex25_Luc06_C)

The rewrite relation of the following TRS is considered.

active(f(f(X)))	→	mark(c(f(g(f(X)))))	(1)
active(c(X))	→	mark(d(X))	(2)
active(h(X))	→	mark(c(d(X)))	(3)
active(f(X))	→	f(active(X))	(4)
active(h(X))	→	h(active(X))	(5)
f(mark(X))	→	mark(f(X))	(6)
h(mark(X))	→	mark(h(X))	(7)
proper(f(X))	→	f(proper(X))	(8)
proper(c(X))	→	c(proper(X))	(9)
proper(g(X))	→	g(proper(X))	(10)
proper(d(X))	→	d(proper(X))	(11)
proper(h(X))	→	h(proper(X))	(12)
f(ok(X))	→	ok(f(X))	(13)
c(ok(X))	→	ok(c(X))	(14)
g(ok(X))	→	ok(g(X))	(15)
d(ok(X))	→	ok(d(X))	(16)
h(ok(X))	→	ok(h(X))	(17)
top(mark(X))	→	top(proper(X))	(18)
top(ok(X))	→	top(active(X))	(19)

The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

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

f(f(active(X)))	→	f(g(f(c(mark(X)))))	(20)
c(active(X))	→	d(mark(X))	(21)
h(active(X))	→	d(c(mark(X)))	(22)
f(active(X))	→	active(f(X))	(23)
h(active(X))	→	active(h(X))	(24)
mark(f(X))	→	f(mark(X))	(25)
mark(h(X))	→	h(mark(X))	(26)
f(proper(X))	→	proper(f(X))	(27)
c(proper(X))	→	proper(c(X))	(28)
g(proper(X))	→	proper(g(X))	(29)
d(proper(X))	→	proper(d(X))	(30)
h(proper(X))	→	proper(h(X))	(31)
ok(f(X))	→	f(ok(X))	(32)
ok(c(X))	→	c(ok(X))	(33)
ok(g(X))	→	g(ok(X))	(34)
ok(d(X))	→	d(ok(X))	(35)
ok(h(X))	→	h(ok(X))	(36)
mark(top(X))	→	proper(top(X))	(37)
ok(top(X))	→	active(top(X))	(38)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[f(x₁)]	=	1 · x₁
[active(x₁)]	=	1 · x₁ + 2
[g(x₁)]	=	1 · x₁
[c(x₁)]	=	1 · x₁
[mark(x₁)]	=	1 · x₁ + 1
[d(x₁)]	=	1 · x₁
[h(x₁)]	=	1 · x₁
[proper(x₁)]	=	1 · x₁
[ok(x₁)]	=	1 · x₁ + 3
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

f(f(active(X)))	→	f(g(f(c(mark(X)))))	(20)
c(active(X))	→	d(mark(X))	(21)
h(active(X))	→	d(c(mark(X)))	(22)
mark(top(X))	→	proper(top(X))	(37)
ok(top(X))	→	active(top(X))	(38)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(active(X))	→	f^#(X)	(39)
h^#(active(X))	→	h^#(X)	(40)
mark^#(f(X))	→	f^#(mark(X))	(41)
mark^#(f(X))	→	mark^#(X)	(42)
mark^#(h(X))	→	h^#(mark(X))	(43)
mark^#(h(X))	→	mark^#(X)	(44)
f^#(proper(X))	→	f^#(X)	(45)
c^#(proper(X))	→	c^#(X)	(46)
g^#(proper(X))	→	g^#(X)	(47)
d^#(proper(X))	→	d^#(X)	(48)
h^#(proper(X))	→	h^#(X)	(49)
ok^#(f(X))	→	f^#(ok(X))	(50)
ok^#(f(X))	→	ok^#(X)	(51)
ok^#(c(X))	→	c^#(ok(X))	(52)
ok^#(c(X))	→	ok^#(X)	(53)
ok^#(g(X))	→	g^#(ok(X))	(54)
ok^#(g(X))	→	ok^#(X)	(55)
ok^#(d(X))	→	d^#(ok(X))	(56)
ok^#(d(X))	→	ok^#(X)	(57)
ok^#(h(X))	→	h^#(ok(X))	(58)
ok^#(h(X))	→	ok^#(X)	(59)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

mark^#(h(X)) → mark^#(X) (44)

mark^#(f(X)) → mark^#(X) (42)

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

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

mark^#(h(X)) → mark^#(X) (44)

1 > 1

mark^#(f(X)) → mark^#(X) (42)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair

ok^#(c(X)) → ok^#(X) (53)

ok^#(f(X)) → ok^#(X) (51)

ok^#(g(X)) → ok^#(X) (55)

ok^#(d(X)) → ok^#(X) (57)

ok^#(h(X)) → ok^#(X) (59)

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

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

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

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

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.2.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

ok^#(c(X)) → ok^#(X) (53)

1 > 1

ok^#(f(X)) → ok^#(X) (51)

1 > 1

ok^#(g(X)) → ok^#(X) (55)

1 > 1

ok^#(d(X)) → ok^#(X) (57)

1 > 1

ok^#(h(X)) → ok^#(X) (59)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair

f^#(proper(X)) → f^#(X) (45)

f^#(active(X)) → f^#(X) (39)

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

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.3.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

f^#(proper(X)) → f^#(X) (45)

1 > 1

f^#(active(X)) → f^#(X) (39)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair

h^#(proper(X)) → h^#(X) (49)

h^#(active(X)) → h^#(X) (40)

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

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.4.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

h^#(proper(X)) → h^#(X) (49)

1 > 1

h^#(active(X)) → h^#(X) (40)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 5^th component contains the pair
c^#(proper(X)) → c^#(X) (46)

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.5.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

c^#(proper(X)) → c^#(X) (46)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 6^th component contains the pair
g^#(proper(X)) → g^#(X) (47)

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.6.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

g^#(proper(X)) → g^#(X) (47)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 7^th component contains the pair
d^#(proper(X)) → d^#(X) (48)

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

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

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

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.1.1.7.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

d^#(proper(X)) → d^#(X) (48)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.

Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/Ex25_Luc06_C)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

1.1 Rule Removal

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.1.1 Size-Change Termination

1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.2.1 Size-Change Termination

1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.3.1 Size-Change Termination

1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.4.1 Size-Change Termination

1.1.1.1.5 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.5.1 Size-Change Termination

1.1.1.1.6 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.6.1 Size-Change Termination

1.1.1.1.7 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.7.1 Size-Change Termination