Certification Problem

Input (TPDB TRS_Standard/AG01/#3.53)

The rewrite relation of the following TRS is considered.

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)
quot(0,s(y))	→	0	(3)
quot(s(x),s(y))	→	s(quot(minus(x,y),s(y)))	(4)
app(nil,y)	→	y	(5)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
reverse(nil)	→	nil	(7)
reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
shuffle(nil)	→	nil	(9)
shuffle(add(n,x))	→	add(n,shuffle(reverse(x)))	(10)
concat(leaf,y)	→	y	(11)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
less_leaves(x,leaf)	→	false	(13)
less_leaves(leaf,cons(w,z))	→	true	(14)
less_leaves(cons(u,v),cons(w,z))	→	less_leaves(concat(u,v),concat(w,z))	(15)

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.

app^#(add(n,x),y)	→	app^#(x,y)	(16)
reverse^#(add(n,x))	→	app^#(reverse(x),add(n,nil))	(17)
less_leaves^#(cons(u,v),cons(w,z))	→	concat^#(u,v)	(18)
quot^#(s(x),s(y))	→	quot^#(minus(x,y),s(y))	(19)
quot^#(s(x),s(y))	→	minus^#(x,y)	(20)
reverse^#(add(n,x))	→	reverse^#(x)	(21)
less_leaves^#(cons(u,v),cons(w,z))	→	concat^#(w,z)	(22)
shuffle^#(add(n,x))	→	reverse^#(x)	(23)
concat^#(cons(u,v),y)	→	concat^#(v,y)	(24)
minus^#(s(x),s(y))	→	minus^#(x,y)	(25)
less_leaves^#(cons(u,v),cons(w,z))	→	less_leaves^#(concat(u,v),concat(w,z))	(26)
shuffle^#(add(n,x))	→	shuffle^#(reverse(x))	(27)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

shuffle^#(add(n,x))

→

shuffle^#(reverse(x))

(27)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	0
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	0
[less_leaves^#(x₁, x₂)]	=	0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 1
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	0
[0]	=	0
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	x₂ + 2439
[quot^#(x₁, x₂)]	=	0
[leaf]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
app(add(n,x),y)	→	add(n,app(x,y))	(6)

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

shuffle^#(add(n,x))

→

shuffle^#(reverse(x))

(27)

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

less_leaves^#(cons(u,v),cons(w,z))

→

less_leaves^#(concat(u,v),concat(w,z))

(26)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	0
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	0
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 1
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 1
[0]	=	0
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[add(x₁, x₂)]	=	x₂ + 16304
[quot^#(x₁, x₂)]	=	0
[leaf]	=	58713
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)

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

less_leaves^#(cons(u,v),cons(w,z))

→

less_leaves^#(concat(u,v),concat(w,z))

(26)

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

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(19)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 2
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 1
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 29483
[0]	=	1
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 16304
[quot^#(x₁, x₂)]	=	x₁ + 0
[leaf]	=	42207
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
minus(x,0)	→	x	(1)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(19)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

minus^#(s(x),s(y))

→

minus^#(x,y)

(25)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 2
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 1
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 29483
[0]	=	1
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	x₂ + 0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 16304
[quot^#(x₁, x₂)]	=	x₁ + 0
[leaf]	=	42207
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
minus(x,0)	→	x	(1)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(25)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

concat^#(cons(u,v),y)

→

concat^#(v,y)

(24)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	x₁ + 0
[false]	=	0
[reverse(x₁)]	=	x₁ + 1
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 53547
[0]	=	1
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 16304
[quot^#(x₁, x₂)]	=	x₁ + 0
[leaf]	=	42207
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
minus(x,0)	→	x	(1)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

concat^#(cons(u,v),y)

→

concat^#(v,y)

(24)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

reverse^#(add(n,x))

→

reverse^#(x)

(21)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[reverse^#(x₁)]	=	x₁ + 0
[minus(x₁, x₂)]	=	x₁ + 1
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 44364
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 53547
[0]	=	1
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 16304
[quot^#(x₁, x₂)]	=	x₁ + 0
[leaf]	=	42207
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
minus(x,0)	→	x	(1)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

reverse^#(add(n,x))

→

reverse^#(x)

(21)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

app^#(add(n,x),y)

→

app^#(x,y)

(16)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[reverse^#(x₁)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[less_leaves^#(x₁, x₂)]	=	x₁ + 0
[concat^#(x₁, x₂)]	=	0
[false]	=	0
[reverse(x₁)]	=	x₁ + 44364
[true]	=	0
[shuffle(x₁)]	=	0
[concat(x₁, x₂)]	=	x₁ + x₂ + 1
[0]	=	1
[quot(x₁, x₂)]	=	0
[less_leaves(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[shuffle^#(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 31122
[add(x₁, x₂)]	=	x₂ + 1
[quot^#(x₁, x₂)]	=	x₁ + 0
[leaf]	=	42207
[app(x₁, x₂)]	=	x₁ + x₂ + 0

together with the usable rules

reverse(add(n,x))	→	app(reverse(x),add(n,nil))	(8)
minus(x,0)	→	x	(1)
app(nil,y)	→	y	(5)
reverse(nil)	→	nil	(7)
concat(cons(u,v),y)	→	cons(u,concat(v,y))	(12)
concat(leaf,y)	→	y	(11)
app(add(n,x),y)	→	add(n,app(x,y))	(6)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

app^#(add(n,x),y)

→

app^#(x,y)

(16)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.