Certification Problem

Input (TPDB TRS_Standard/Secret_05_TRS/cime1)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(11)
te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	te^#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))	(12)
sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))	→	sortSu^#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))	(13)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(14)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	te^#(msubst(te(a),sortSu(t)))	(15)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(16)
sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))	→	sortSu^#(circ(sortSu(t),sortSu(u)))	(17)
te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(18)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t)))))	(19)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(20)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u)))	(21)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t)))))	→	sortSu^#(cons(te(a),sortSu(circ(sortSu(s),sortSu(t)))))	(22)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t)))))	→	sortSu^#(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t)))))	(23)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t)))))	(24)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))	→	sortSu^#(circ(sortSu(t),sortSu(u)))	(17)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(16)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u)))	(21)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	te^#(msubst(te(a),sortSu(t)))	(15)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(14)
sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))	→	sortSu^#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))	(13)
te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	te^#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))	(12)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(20)
te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(18)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(11)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[sortSu(x₁)]	=	x₁ + 2
[sop(x₁)]	=	x₁ + 1
[te^#(x₁)]	=	x₁ + 41379
[sortSu^#(x₁)]	=	x₁ + 0
[lift]	=	1
[msubst(x₁, x₂)]	=	x₁ + x₂ + 2
[subst(x₁, x₂)]	=	x₁ + 0
[te(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 41379, x₂ + 82759, 0)
[id]	=	14661
[circ(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

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

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

sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))	→	sortSu^#(circ(sortSu(t),sortSu(u)))	(17)
sortSu^#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(16)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(cons(sop(lift),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u)))	(21)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(sop(lift),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(14)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift),sortSu(t))),sortSu(u)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(20)
te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(18)
sortSu^#(circ(sortSu(cons(sop(lift),sortSu(s))),sortSu(cons(te(a),sortSu(t)))))	→	sortSu^#(circ(sortSu(s),sortSu(t)))	(11)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))

→

sortSu^#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))

(13)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(sortSu)	=	1
π(te^#)	=	1
π(sortSu^#)	=	1
π(msubst)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(sop)	=	4	status(sop)	=	[1]	list-extension(sop)	=	Lex
prec(lift)	=	4	status(lift)	=	[]	list-extension(lift)	=	Lex
prec(subst)	=	0	status(subst)	=	[1, 2]	list-extension(subst)	=	Lex
prec(te)	=	2	status(te)	=	[]	list-extension(te)	=	Lex
prec(cons)	=	4	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(id)	=	0	status(id)	=	[]	list-extension(id)	=	Lex
prec(circ)	=	1	status(circ)	=	[1, 2]	list-extension(circ)	=	Lex

and the following Max-polynomial interpretation

[sop(x₁)]	=	x₁ + 0
[lift]	=	0
[subst(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[te(x₁)]	=	0
[cons(x₁, x₂)]	=	max(0)
[id]	=	0
[circ(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

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

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

sortSu^#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u)))

→

sortSu^#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))

(13)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))

→

te^#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))

(12)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[sortSu(x₁)]	=	x₁ + 1
[sop(x₁)]	=	1
[te^#(x₁)]	=	x₁ + 2
[sortSu^#(x₁)]	=	0
[lift]	=	1
[msubst(x₁, x₂)]	=	x₁ + 0
[subst(x₁, x₂)]	=	x₁ + 0
[te(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	2
[id]	=	31122
[circ(x₁, x₂)]	=	1

together with the usable rules

te(subst(te(a),sortSu(id)))	→	te(a)	(8)
te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))	→	te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))	(10)
te(msubst(te(a),sortSu(id)))	→	te(a)	(9)

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

te^#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t)))

→

te^#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))

(12)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.