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 AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

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

1.1.1 Size-Change Termination

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

Term_sub^#(Case(m,xi,n),s)	→	Frozen^#(m,Sum_sub(xi,s),n,s)	(22)

1	>	1
1	>	3
2	≥	4
Term_sub^#(Term_sub(m,s),t)	→	Concat^#(s,t)	(37)

1	>	1
2	≥	2
Concat^#(Cons_usual(x,m,s),t)	→	Term_sub^#(m,t)	(42)

1	>	1
2	≥	2
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(m,s)	(28)

1	>	1
2	≥	2
Term_sub^#(Term_app(m,n),s)	→	Term_sub^#(n,s)	(29)

1	>	1
2	≥	2
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(m,s)	(30)

1	>	1
2	≥	2
Term_sub^#(Term_pair(m,n),s)	→	Term_sub^#(n,s)	(31)

1	>	1
2	≥	2
Term_sub^#(Term_inl(m),s)	→	Term_sub^#(m,s)	(32)

1	>	1
2	≥	2
Term_sub^#(Term_inr(m),s)	→	Term_sub^#(m,s)	(33)

1	>	1
2	≥	2
Term_sub^#(Term_sub(m,s),t)	→	Term_sub^#(m,Concat(s,t))	(36)

1	>	1
Frozen^#(m,Sum_constant(Left),n,s)	→	Term_sub^#(m,s)	(24)

1	≥	1
4	≥	2
Frozen^#(m,Sum_constant(Right),n,s)	→	Term_sub^#(n,s)	(25)

3	≥	1
4	≥	2
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(m,s)	(26)

1	≥	1
4	≥	2
Frozen^#(m,Sum_term_var(xi),n,s)	→	Term_sub^#(n,s)	(27)

3	≥	1
4	≥	2
Concat^#(Concat(s,t),u)	→	Concat^#(s,Concat(t,u))	(40)

1	>	1
Concat^#(Concat(s,t),u)	→	Concat^#(t,u)	(41)

1	>	1
2	≥	2
Concat^#(Cons_usual(x,m,s),t)	→	Concat^#(s,t)	(43)

1	>	1
2	≥	2
Concat^#(Cons_sum(xi,k,s),t)	→	Concat^#(s,t)	(44)

1	>	1
2	≥	2

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

The 2^nd component contains the pair

Term_sub^#(Term_var(x),Cons_sum(xi,k,s)) → Term_sub^#(Term_var(x),s) (35)

Term_sub^#(Term_var(x),Cons_usual(y,m,s)) → Term_sub^#(Term_var(x),s) (34)

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

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

[Cons_sum(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[Cons_usual(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[Term_sub^#(x₁, x₂)] = 1 · 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.2.1 Size-Change Termination

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

Term_sub^#(Term_var(x),Cons_sum(xi,k,s)) → Term_sub^#(Term_var(x),s) (35)

1 ≥ 1

2 > 2

Term_sub^#(Term_var(x),Cons_usual(y,m,s)) → Term_sub^#(Term_var(x),s) (34)

1 ≥ 1

2 > 2

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

Sum_sub^#(xi,Cons_usual(y,m,s)) → Sum_sub^#(xi,s) (39)

Sum_sub^#(xi,Cons_sum(psi,k,s)) → Sum_sub^#(xi,s) (38)

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

[Cons_usual(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[Cons_sum(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[Sum_sub^#(x₁, x₂)] = 1 · 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.3.1 Size-Change Termination

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

Sum_sub^#(xi,Cons_usual(y,m,s)) → Sum_sub^#(xi,s) (39)

1 ≥ 1

2 > 2

Sum_sub^#(xi,Cons_sum(psi,k,s)) → Sum_sub^#(xi,s) (38)

1 ≥ 1

2 > 2

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

[Term_var(x₁)]	=	1 · x₁
[Cons_sum(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[Cons_usual(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[Term_sub^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

Certification Problem

Input (TPDB TRS_Standard/CiME_04/lse)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Size-Change Termination

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.2.1 Size-Change Termination

1.1.3 Monotonic Reduction Pair Processor with Usable Rules

1.1.3.1 Size-Change Termination