Certification Problem

Input (TPDB TRS_Standard/Secret_05_TRS/cime2)

The rewrite relation of the following TRS is considered.

circ(cons(a,s),t) → cons(msubst(a,t),circ(s,t)) (1)
circ(cons(lift,s),cons(a,t)) → cons(a,circ(s,t)) (2)
circ(cons(lift,s),cons(lift,t)) → cons(lift,circ(s,t)) (3)
circ(circ(s,t),u) → circ(s,circ(t,u)) (4)
circ(s,id) → s (5)
circ(id,s) → s (6)
circ(cons(lift,s),circ(cons(lift,t),u)) → circ(cons(lift,circ(s,t)),u) (7)
subst(a,id) → a (8)
msubst(a,id) → a (9)
msubst(msubst(a,s),t) → msubst(a,circ(s,t)) (10)

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.
circ#(cons(a,s),t) → msubst#(a,t) (11)
circ#(cons(a,s),t) → circ#(s,t) (12)
circ#(cons(lift,s),cons(a,t)) → circ#(s,t) (13)
circ#(cons(lift,s),cons(lift,t)) → circ#(s,t) (14)
circ#(circ(s,t),u) → circ#(s,circ(t,u)) (15)
circ#(circ(s,t),u) → circ#(t,u) (16)
circ#(cons(lift,s),circ(cons(lift,t),u)) → circ#(cons(lift,circ(s,t)),u) (17)
circ#(cons(lift,s),circ(cons(lift,t),u)) → circ#(s,t) (18)
msubst#(msubst(a,s),t) → msubst#(a,circ(s,t)) (19)
msubst#(msubst(a,s),t) → circ#(s,t) (20)

1.1 Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals
[circ#(x1, x2)] = 1 · x1 + 1 · x1 · x2
[cons(x1, x2)] = 1 + 1 · x2 + 1 · x1
[msubst#(x1, x2)] = 1 · x1 + 1 · x1 · x2
[lift] = 0
[circ(x1, x2)] = 1 · x2 + 1 · x1 + 1 · x1 · x2
[msubst(x1, x2)] = 1 · x2 + 1 · x1 + 1 · x1 · x2
[id] = 1
together with the usable rules
circ(cons(a,s),t) → cons(msubst(a,t),circ(s,t)) (1)
circ(cons(lift,s),cons(a,t)) → cons(a,circ(s,t)) (2)
circ(cons(lift,s),cons(lift,t)) → cons(lift,circ(s,t)) (3)
circ(circ(s,t),u) → circ(s,circ(t,u)) (4)
circ(s,id) → s (5)
circ(id,s) → s (6)
circ(cons(lift,s),circ(cons(lift,t),u)) → circ(cons(lift,circ(s,t)),u) (7)
msubst(msubst(a,s),t) → msubst(a,circ(s,t)) (10)
msubst(a,id) → a (9)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
circ#(cons(a,s),t) → msubst#(a,t) (11)
circ#(cons(a,s),t) → circ#(s,t) (12)
circ#(cons(lift,s),cons(a,t)) → circ#(s,t) (13)
circ#(cons(lift,s),cons(lift,t)) → circ#(s,t) (14)
circ#(cons(lift,s),circ(cons(lift,t),u)) → circ#(cons(lift,circ(s,t)),u) (17)
circ#(cons(lift,s),circ(cons(lift,t),u)) → circ#(s,t) (18)
could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.