Certification Problem

Input (TPDB TRS_Standard/CiME_04/lse)

The rewrite relation of the following TRS is considered.

Term_sub(Case(m,xi,n),s)	→	Frozen(m,Sum_sub(xi,s),n,s)	(1)
Frozen(m,Sum_constant(Left),n,s)	→	Term_sub(m,s)	(2)
Frozen(m,Sum_constant(Right),n,s)	→	Term_sub(n,s)	(3)
Frozen(m,Sum_term_var(xi),n,s)	→	Case(Term_sub(m,s),xi,Term_sub(n,s))	(4)
Term_sub(Term_app(m,n),s)	→	Term_app(Term_sub(m,s),Term_sub(n,s))	(5)
Term_sub(Term_pair(m,n),s)	→	Term_pair(Term_sub(m,s),Term_sub(n,s))	(6)
Term_sub(Term_inl(m),s)	→	Term_inl(Term_sub(m,s))	(7)
Term_sub(Term_inr(m),s)	→	Term_inr(Term_sub(m,s))	(8)
Term_sub(Term_var(x),Id)	→	Term_var(x)	(9)
Term_sub(Term_var(x),Cons_usual(y,m,s))	→	m	(10)
Term_sub(Term_var(x),Cons_usual(y,m,s))	→	Term_sub(Term_var(x),s)	(11)
Term_sub(Term_var(x),Cons_sum(xi,k,s))	→	Term_sub(Term_var(x),s)	(12)
Term_sub(Term_sub(m,s),t)	→	Term_sub(m,Concat(s,t))	(13)
Sum_sub(xi,Id)	→	Sum_term_var(xi)	(14)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_constant(k)	(15)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_sub(xi,s)	(16)
Sum_sub(xi,Cons_usual(y,m,s))	→	Sum_sub(xi,s)	(17)
Concat(Concat(s,t),u)	→	Concat(s,Concat(t,u))	(18)
Concat(Cons_usual(x,m,s),t)	→	Cons_usual(x,Term_sub(m,t),Concat(s,t))	(19)
Concat(Cons_sum(xi,k,s),t)	→	Cons_sum(xi,k,Concat(s,t))	(20)
Concat(Id,s)	→	s	(21)

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.

Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(m,s)	(22)
Term_sub^#(Term_var(x),Cons_usual(y,m,s))	→	Term_sub^#(Term_var(x),s)	(23)
Concat^#(Cons_usual(x,m,s),t)	→	Term_sub^#(m,t)	(24)
Term_sub^#(Term_inl(m),s)	→	Term_sub^#(m,s)	(25)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(n,s)	(26)
Concat^#(Concat(s,t),u)	→	Concat^#(t,u)	(27)
Sum_sub^#(xi,Cons_usual(y,m,s))	→	Sum_sub^#(xi,s)	(28)
Concat^#(Cons_usual(x,m,s),t)	→	Concat^#(s,t)	(29)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(m,s)	(30)
Term_sub^#(Term_var(x),Cons_sum(xi,k,s))	→	Term_sub^#(Term_var(x),s)	(31)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(m,s)	(32)
Term_sub^#(Term_sub(m,s),t)	→	Concat^#(s,t)	(33)
Concat^#(Concat(s,t),u)	→	Concat^#(s,Concat(t,u))	(34)
Term_sub^#(Case(m,xi,n),s)	→	Frozen^#(m,Sum_sub(xi,s),n,s)	(35)
Term_sub^#(Term_inr(m),s)	→	Term_sub^#(m,s)	(36)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(n,s)	(37)
Frozen^#(m,Sum_constant(Right),n,s)	→	Term_sub^#(n,s)	(38)
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(n,s)	(39)
Frozen^#(m,Sum_constant(Left),n,s)	→	Term_sub^#(m,s)	(40)
Concat^#(Cons_sum(xi,k,s),t)	→	Concat^#(s,t)	(41)
Sum_sub^#(xi,Cons_sum(psi,k,s))	→	Sum_sub^#(xi,s)	(42)
Term_sub^#(Term_sub(m,s),t)	→	Term_sub^#(m,Concat(s,t))	(43)
Term_sub^#(Case(m,xi,n),s)	→	Sum_sub^#(xi,s)	(44)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

Term_sub^#(Term_sub(m,s),t)	→	Term_sub^#(m,Concat(s,t))	(43)
Concat^#(Cons_usual(x,m,s),t)	→	Concat^#(s,t)	(29)
Concat^#(Cons_sum(xi,k,s),t)	→	Concat^#(s,t)	(41)
Frozen^#(m,Sum_constant(Left),n,s)	→	Term_sub^#(m,s)	(40)
Concat^#(Concat(s,t),u)	→	Concat^#(t,u)	(27)
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(n,s)	(39)
Frozen^#(m,Sum_constant(Right),n,s)	→	Term_sub^#(n,s)	(38)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(n,s)	(37)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(n,s)	(26)
Term_sub^#(Term_inl(m),s)	→	Term_sub^#(m,s)	(25)
Concat^#(Cons_usual(x,m,s),t)	→	Term_sub^#(m,t)	(24)
Term_sub^#(Term_inr(m),s)	→	Term_sub^#(m,s)	(36)
Term_sub^#(Case(m,xi,n),s)	→	Frozen^#(m,Sum_sub(xi,s),n,s)	(35)
Concat^#(Concat(s,t),u)	→	Concat^#(s,Concat(t,u))	(34)
Term_sub^#(Term_sub(m,s),t)	→	Concat^#(s,t)	(33)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(m,s)	(32)
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(m,s)	(22)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(m,s)	(30)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[Cons_sum(x₁, x₂, x₃)]	=	x₃ + 1
[Left]	=	1
[Sum_term_var(x₁)]	=	1
[Concat^#(x₁, x₂)]	=	x₁ + 0
[Case(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 2
[Term_inr(x₁)]	=	x₁ + 8856
[Sum_sub^#(x₁, x₂)]	=	0
[Sum_constant(x₁)]	=	1
[Sum_sub(x₁, x₂)]	=	1
[Right]	=	1
[Cons_usual(x₁, x₂, x₃)]	=	x₂ + x₃ + 11798
[Term_var(x₁)]	=	9508
[Id]	=	32286
[Term_sub(x₁, x₂)]	=	x₁ + x₂ + 1
[Frozen(x₁,...,x₄)]	=	0
[Frozen^#(x₁,...,x₄)]	=	x₁ + x₂ + x₃ + 0
[Term_app(x₁, x₂)]	=	x₁ + x₂ + 10451
[Term_inl(x₁)]	=	x₁ + 30613
[Term_pair(x₁, x₂)]	=	x₁ + x₂ + 5854
[Term_sub^#(x₁, x₂)]	=	x₁ + 0
[Concat(x₁, x₂)]	=	x₁ + x₂ + 28102

together with the usable rules

Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_constant(k)	(15)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_sub(xi,s)	(16)
Sum_sub(xi,Cons_usual(y,m,s))	→	Sum_sub(xi,s)	(17)
Sum_sub(xi,Id)	→	Sum_term_var(xi)	(14)

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

Term_sub^#(Term_sub(m,s),t)	→	Term_sub^#(m,Concat(s,t))	(43)
Concat^#(Cons_usual(x,m,s),t)	→	Concat^#(s,t)	(29)
Concat^#(Cons_sum(xi,k,s),t)	→	Concat^#(s,t)	(41)
Frozen^#(m,Sum_constant(Left),n,s)	→	Term_sub^#(m,s)	(40)
Concat^#(Concat(s,t),u)	→	Concat^#(t,u)	(27)
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(n,s)	(39)
Frozen^#(m,Sum_constant(Right),n,s)	→	Term_sub^#(n,s)	(38)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(n,s)	(37)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(n,s)	(26)
Term_sub^#(Term_inl(m),s)	→	Term_sub^#(m,s)	(25)
Concat^#(Cons_usual(x,m,s),t)	→	Term_sub^#(m,t)	(24)
Term_sub^#(Term_inr(m),s)	→	Term_sub^#(m,s)	(36)
Term_sub^#(Case(m,xi,n),s)	→	Frozen^#(m,Sum_sub(xi,s),n,s)	(35)
Concat^#(Concat(s,t),u)	→	Concat^#(s,Concat(t,u))	(34)
Term_sub^#(Term_sub(m,s),t)	→	Concat^#(s,t)	(33)
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(m,s)	(32)
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(m,s)	(22)
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(m,s)	(30)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

Term_sub^#(Term_var(x),Cons_usual(y,m,s))	→	Term_sub^#(Term_var(x),s)	(23)
Term_sub^#(Term_var(x),Cons_sum(xi,k,s))	→	Term_sub^#(Term_var(x),s)	(31)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[Cons_sum(x₁, x₂, x₃)]	=	x₃ + 1
[Left]	=	1
[Sum_term_var(x₁)]	=	1
[Concat^#(x₁, x₂)]	=	0
[Case(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 13297
[Term_inr(x₁)]	=	x₁ + 31205
[Sum_sub^#(x₁, x₂)]	=	0
[Sum_constant(x₁)]	=	1
[Sum_sub(x₁, x₂)]	=	1
[Right]	=	1
[Cons_usual(x₁, x₂, x₃)]	=	x₃ + 11798
[Term_var(x₁)]	=	46441
[Id]	=	1
[Term_sub(x₁, x₂)]	=	x₁ + x₂ + 2
[Frozen(x₁,...,x₄)]	=	x₂ + 0
[Frozen^#(x₁,...,x₄)]	=	x₂ + 0
[Term_app(x₁, x₂)]	=	x₂ + 22105
[Term_inl(x₁)]	=	x₁ + 1
[Term_pair(x₁, x₂)]	=	x₁ + x₂ + 30490
[Term_sub^#(x₁, x₂)]	=	x₂ + 0
[Concat(x₁, x₂)]	=	x₁ + x₂ + 3

together with the usable rules

Concat(Concat(s,t),u)	→	Concat(s,Concat(t,u))	(18)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_constant(k)	(15)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_sub(xi,s)	(16)
Concat(Id,s)	→	s	(21)
Concat(Cons_usual(x,m,s),t)	→	Cons_usual(x,Term_sub(m,t),Concat(s,t))	(19)
Sum_sub(xi,Cons_usual(y,m,s))	→	Sum_sub(xi,s)	(17)
Concat(Cons_sum(xi,k,s),t)	→	Cons_sum(xi,k,Concat(s,t))	(20)
Sum_sub(xi,Id)	→	Sum_term_var(xi)	(14)

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

Term_sub^#(Term_var(x),Cons_usual(y,m,s))	→	Term_sub^#(Term_var(x),s)	(23)
Term_sub^#(Term_var(x),Cons_sum(xi,k,s))	→	Term_sub^#(Term_var(x),s)	(31)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

Sum_sub^#(xi,Cons_sum(psi,k,s))	→	Sum_sub^#(xi,s)	(42)
Sum_sub^#(xi,Cons_usual(y,m,s))	→	Sum_sub^#(xi,s)	(28)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[Cons_sum(x₁, x₂, x₃)]	=	x₃ + 1
[Left]	=	1
[Sum_term_var(x₁)]	=	1
[Concat^#(x₁, x₂)]	=	0
[Case(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 48178
[Term_inr(x₁)]	=	x₁ + 31205
[Sum_sub^#(x₁, x₂)]	=	x₂ + 0
[Sum_constant(x₁)]	=	1
[Sum_sub(x₁, x₂)]	=	1
[Right]	=	1
[Cons_usual(x₁, x₂, x₃)]	=	x₃ + 11798
[Term_var(x₁)]	=	1
[Id]	=	1
[Term_sub(x₁, x₂)]	=	x₁ + x₂ + 2
[Frozen(x₁,...,x₄)]	=	x₂ + 0
[Frozen^#(x₁,...,x₄)]	=	x₂ + 0
[Term_app(x₁, x₂)]	=	x₂ + 1
[Term_inl(x₁)]	=	x₁ + 1
[Term_pair(x₁, x₂)]	=	x₁ + x₂ + 15208
[Term_sub^#(x₁, x₂)]	=	x₂ + 0
[Concat(x₁, x₂)]	=	x₁ + x₂ + 3

together with the usable rules

Concat(Concat(s,t),u)	→	Concat(s,Concat(t,u))	(18)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_constant(k)	(15)
Sum_sub(xi,Cons_sum(psi,k,s))	→	Sum_sub(xi,s)	(16)
Concat(Id,s)	→	s	(21)
Concat(Cons_usual(x,m,s),t)	→	Cons_usual(x,Term_sub(m,t),Concat(s,t))	(19)
Sum_sub(xi,Cons_usual(y,m,s))	→	Sum_sub(xi,s)	(17)
Concat(Cons_sum(xi,k,s),t)	→	Cons_sum(xi,k,Concat(s,t))	(20)
Sum_sub(xi,Id)	→	Sum_term_var(xi)	(14)

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

Sum_sub^#(xi,Cons_sum(psi,k,s))	→	Sum_sub^#(xi,s)	(42)
Sum_sub^#(xi,Cons_usual(y,m,s))	→	Sum_sub^#(xi,s)	(28)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.