Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_7_37_Bor03_GM)

The rewrite relation of the following TRS is considered.

a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(0,cons(X,XS))	→	mark(X)	(2)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
a__minus(X,0)	→	0	(4)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__quot(0,s(Y))	→	0	(6)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__zWquot(XS,nil)	→	nil	(8)
a__zWquot(nil,XS)	→	nil	(9)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
mark(from(X))	→	a__from(mark(X))	(11)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(17)
mark(0)	→	0	(18)
mark(nil)	→	nil	(19)
a__from(X)	→	from(X)	(20)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)

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.

mark^#(minus(X1,X2))	→	a__minus^#(mark(X1),mark(X2))	(25)
a__from^#(X)	→	mark^#(X)	(26)
mark^#(from(X))	→	mark^#(X)	(27)
a__quot^#(s(X),s(Y))	→	a__quot^#(a__minus(mark(X),mark(Y)),s(mark(Y)))	(28)
mark^#(sel(X1,X2))	→	mark^#(X2)	(29)
mark^#(quot(X1,X2))	→	mark^#(X1)	(30)
mark^#(s(X))	→	mark^#(X)	(31)
a__minus^#(s(X),s(Y))	→	mark^#(Y)	(32)
mark^#(quot(X1,X2))	→	mark^#(X2)	(33)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(34)
a__quot^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(35)
mark^#(zWquot(X1,X2))	→	a__zWquot^#(mark(X1),mark(X2))	(36)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(38)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(39)
mark^#(quot(X1,X2))	→	a__quot^#(mark(X1),mark(X2))	(40)
mark^#(from(X))	→	a__from^#(mark(X))	(41)
a__sel^#(s(N),cons(X,XS))	→	mark^#(XS)	(42)
a__minus^#(s(X),s(Y))	→	mark^#(X)	(43)
a__sel^#(s(N),cons(X,XS))	→	mark^#(N)	(44)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
mark^#(zWquot(X1,X2))	→	mark^#(X2)	(46)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(47)
a__sel^#(s(N),cons(X,XS))	→	a__sel^#(mark(N),mark(XS))	(48)
a__minus^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(49)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
mark^#(minus(X1,X2))	→	mark^#(X1)	(50)
a__sel^#(0,cons(X,XS))	→	mark^#(X)	(51)
mark^#(sel(X1,X2))	→	mark^#(X1)	(52)
a__quot^#(s(X),s(Y))	→	mark^#(X)	(53)
mark^#(minus(X1,X2))	→	mark^#(X2)	(54)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	a__quot^#(mark(X),mark(Y))	(55)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__zWquot^#(cons(X,XS),cons(Y,YS))	→	a__quot^#(mark(X),mark(Y))	(55)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(minus(X1,X2))	→	mark^#(X2)	(54)
mark^#(zWquot(X1,X2))	→	a__zWquot^#(mark(X1),mark(X2))	(36)
a__quot^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(35)
a__quot^#(s(X),s(Y))	→	mark^#(X)	(53)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(34)
mark^#(quot(X1,X2))	→	mark^#(X2)	(33)
mark^#(sel(X1,X2))	→	mark^#(X1)	(52)
a__sel^#(0,cons(X,XS))	→	mark^#(X)	(51)
a__minus^#(s(X),s(Y))	→	mark^#(Y)	(32)
mark^#(minus(X1,X2))	→	mark^#(X1)	(50)
mark^#(s(X))	→	mark^#(X)	(31)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
a__minus^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(49)
a__sel^#(s(N),cons(X,XS))	→	a__sel^#(mark(N),mark(XS))	(48)
mark^#(quot(X1,X2))	→	mark^#(X1)	(30)
mark^#(sel(X1,X2))	→	mark^#(X2)	(29)
a__quot^#(s(X),s(Y))	→	a__quot^#(a__minus(mark(X),mark(Y)),s(mark(Y)))	(28)
mark^#(zWquot(X1,X2))	→	mark^#(X2)	(46)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(47)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
mark^#(from(X))	→	mark^#(X)	(27)
a__sel^#(s(N),cons(X,XS))	→	mark^#(N)	(44)
a__minus^#(s(X),s(Y))	→	mark^#(X)	(43)
a__sel^#(s(N),cons(X,XS))	→	mark^#(XS)	(42)
mark^#(from(X))	→	a__from^#(mark(X))	(41)
mark^#(quot(X1,X2))	→	a__quot^#(mark(X1),mark(X2))	(40)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(39)
a__from^#(X)	→	mark^#(X)	(26)
mark^#(minus(X1,X2))	→	a__minus^#(mark(X1),mark(X2))	(25)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(38)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	1
[s(x₁)]	=	12214
[a__zWquot^#(x₁, x₂)]	=	12214
[a__from^#(x₁)]	=	12214
[a__quot^#(x₁, x₂)]	=	x₁ + 0
[minus(x₁, x₂)]	=	1
[a__from(x₁)]	=	12214
[a__zWquot(x₁, x₂)]	=	x₁ + 0
[zWquot(x₁, x₂)]	=	0
[a__quot(x₁, x₂)]	=	12214
[mark^#(x₁)]	=	12214
[0]	=	1
[quot(x₁, x₂)]	=	1
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	1
[a__minus^#(x₁, x₂)]	=	x₁ + 0
[nil]	=	0
[a__sel^#(x₁, x₂)]	=	x₂ + 0
[mark(x₁)]	=	12214
[a__sel(x₁, x₂)]	=	12214
[cons(x₁, x₂)]	=	12214

together with the usable rules

mark(0)	→	0	(18)
a__minus(X,0)	→	0	(4)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
a__zWquot(XS,nil)	→	nil	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__from(X)	→	from(X)	(20)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)
mark(from(X))	→	a__from(mark(X))	(11)
a__zWquot(nil,XS)	→	nil	(9)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
a__quot(0,s(Y))	→	0	(6)
a__sel(0,cons(X,XS))	→	mark(X)	(2)

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

a__quot^#(s(X),s(Y))

→

a__quot^#(a__minus(mark(X),mark(Y)),s(mark(Y)))

(28)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(zWquot(X1,X2))	→	mark^#(X2)	(46)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(34)
mark^#(zWquot(X1,X2))	→	a__zWquot^#(mark(X1),mark(X2))	(36)
a__from^#(X)	→	mark^#(X)	(26)
a__sel^#(s(N),cons(X,XS))	→	mark^#(XS)	(42)
a__sel^#(s(N),cons(X,XS))	→	mark^#(N)	(44)
a__sel^#(s(N),cons(X,XS))	→	a__sel^#(mark(N),mark(XS))	(48)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
mark^#(s(X))	→	mark^#(X)	(31)
a__minus^#(s(X),s(Y))	→	mark^#(Y)	(32)
a__minus^#(s(X),s(Y))	→	mark^#(X)	(43)
a__minus^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(49)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(38)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(47)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	a__quot^#(mark(X),mark(Y))	(55)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
a__quot^#(s(X),s(Y))	→	mark^#(X)	(53)
a__quot^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(35)
mark^#(quot(X1,X2))	→	mark^#(X2)	(33)
mark^#(quot(X1,X2))	→	mark^#(X1)	(30)
mark^#(quot(X1,X2))	→	a__quot^#(mark(X1),mark(X2))	(40)
mark^#(sel(X1,X2))	→	mark^#(X2)	(29)
mark^#(sel(X1,X2))	→	mark^#(X1)	(52)
mark^#(sel(X1,X2))	→	a__sel^#(mark(X1),mark(X2))	(39)
mark^#(from(X))	→	mark^#(X)	(27)
mark^#(from(X))	→	a__from^#(mark(X))	(41)
mark^#(minus(X1,X2))	→	mark^#(X2)	(54)
mark^#(minus(X1,X2))	→	mark^#(X1)	(50)
mark^#(minus(X1,X2))	→	a__minus^#(mark(X1),mark(X2))	(25)
a__sel^#(0,cons(X,XS))	→	mark^#(X)	(51)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[s(x₁)]	=	x₁ + 0
[a__zWquot^#(x₁, x₂)]	=	max(x₁ + 46576, x₂ + 31893, 0)
[a__from^#(x₁)]	=	x₁ + 31893
[a__quot^#(x₁, x₂)]	=	max(x₁ + 31894, x₂ + 46575, 0)
[minus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[a__from(x₁)]	=	x₁ + 14682
[a__zWquot(x₁, x₂)]	=	max(x₁ + 14685, x₂ + 29368, 0)
[zWquot(x₁, x₂)]	=	max(x₁ + 14685, x₂ + 29368, 0)
[a__quot(x₁, x₂)]	=	max(x₁ + 14684, x₂ + 14687, 0)
[mark^#(x₁)]	=	x₁ + 31892
[0]	=	14688
[quot(x₁, x₂)]	=	max(x₁ + 14684, x₂ + 14687, 0)
[from(x₁)]	=	x₁ + 14682
[sel(x₁, x₂)]	=	max(x₁ + 35660, x₂ + 35661, 0)
[a__minus^#(x₁, x₂)]	=	max(x₁ + 31892, x₂ + 31893, 0)
[nil]	=	29369
[a__sel^#(x₁, x₂)]	=	max(x₁ + 67552, x₂ + 52869, 0)
[mark(x₁)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	max(x₁ + 35660, x₂ + 35661, 0)
[cons(x₁, x₂)]	=	max(x₁ + 14682, x₂ + 0, 0)

together with the usable rules

mark(0)	→	0	(18)
a__minus(X,0)	→	0	(4)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
a__zWquot(XS,nil)	→	nil	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__from(X)	→	from(X)	(20)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)
mark(from(X))	→	a__from(mark(X))	(11)
a__zWquot(nil,XS)	→	nil	(9)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
a__quot(0,s(Y))	→	0	(6)
a__sel(0,cons(X,XS))	→	mark(X)	(2)

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

mark^#(zWquot(X1,X2))	→	mark^#(X2)	(46)
mark^#(zWquot(X1,X2))	→	mark^#(X1)	(34)
mark^#(zWquot(X1,X2))	→	a__zWquot^#(mark(X1),mark(X2))	(36)
a__from^#(X)	→	mark^#(X)	(26)
a__sel^#(s(N),cons(X,XS))	→	mark^#(XS)	(42)
a__sel^#(s(N),cons(X,XS))	→	mark^#(N)	(44)
mark^#(cons(X1,X2))	→	mark^#(X1)	(37)
a__minus^#(s(X),s(Y))	→	mark^#(Y)	(32)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(Y)	(38)
a__zWquot^#(cons(X,XS),cons(Y,YS))	→	mark^#(X)	(47)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
a__quot^#(s(X),s(Y))	→	mark^#(Y)	(45)
a__quot^#(s(X),s(Y))	→	mark^#(X)	(53)
a__quot^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(35)
mark^#(quot(X1,X2))	→	mark^#(X2)	(33)
mark^#(quot(X1,X2))	→	mark^#(X1)	(30)
mark^#(quot(X1,X2))	→	a__quot^#(mark(X1),mark(X2))	(40)
mark^#(sel(X1,X2))	→	mark^#(X2)	(29)
mark^#(sel(X1,X2))	→	mark^#(X1)	(52)
mark^#(from(X))	→	mark^#(X)	(27)
mark^#(from(X))	→	a__from^#(mark(X))	(41)
mark^#(minus(X1,X2))	→	mark^#(X2)	(54)
a__sel^#(0,cons(X,XS))	→	mark^#(X)	(51)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(s(X))	→	mark^#(X)	(31)
a__minus^#(s(X),s(Y))	→	mark^#(X)	(43)
a__minus^#(s(X),s(Y))	→	a__minus^#(mark(X),mark(Y))	(49)
mark^#(minus(X1,X2))	→	mark^#(X1)	(50)
mark^#(minus(X1,X2))	→	a__minus^#(mark(X1),mark(X2))	(25)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	max(x₁ + 2334, x₂ + 2335, 0)
[s(x₁)]	=	x₁ + 0
[a__zWquot^#(x₁, x₂)]	=	max(0)
[a__from^#(x₁)]	=	31893
[a__quot^#(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 2334, x₂ + 2335, 0)
[a__from(x₁)]	=	x₁ + 41379
[a__zWquot(x₁, x₂)]	=	max(x₁ + 2336, x₂ + 2336, 0)
[zWquot(x₁, x₂)]	=	max(x₁ + 2336, x₂ + 2336, 0)
[a__quot(x₁, x₂)]	=	max(x₂ + 2335, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	2335
[quot(x₁, x₂)]	=	max(x₂ + 2335, 0)
[from(x₁)]	=	x₁ + 41379
[sel(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__minus^#(x₁, x₂)]	=	max(x₁ + 2332, x₂ + 2333, 0)
[nil]	=	2337
[a__sel^#(x₁, x₂)]	=	max(0)
[mark(x₁)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	max(x₂ + 0, 0)
[cons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)

together with the usable rules

mark(0)	→	0	(18)
a__minus(X,0)	→	0	(4)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
a__zWquot(XS,nil)	→	nil	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__from(X)	→	from(X)	(20)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)
mark(from(X))	→	a__from(mark(X))	(11)
a__zWquot(nil,XS)	→	nil	(9)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
a__quot(0,s(Y))	→	0	(6)
a__sel(0,cons(X,XS))	→	mark(X)	(2)

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

a__minus^#(s(X),s(Y))	→	mark^#(X)	(43)
mark^#(minus(X1,X2))	→	mark^#(X1)	(50)
mark^#(minus(X1,X2))	→	a__minus^#(mark(X1),mark(X2))	(25)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(s(X))

→

mark^#(X)

(31)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	3
[s(x₁)]	=	x₁ + 1
[a__zWquot^#(x₁, x₂)]	=	0
[a__from^#(x₁)]	=	0
[a__quot^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₂ + 4
[a__from(x₁)]	=	3
[a__zWquot(x₁, x₂)]	=	x₁ + 1
[zWquot(x₁, x₂)]	=	x₁ + x₂ + 2
[a__quot(x₁, x₂)]	=	x₁ + 29273
[mark^#(x₁)]	=	x₁ + 0
[0]	=	4
[quot(x₁, x₂)]	=	x₂ + 29274
[from(x₁)]	=	x₁ + 4
[sel(x₁, x₂)]	=	2
[a__minus^#(x₁, x₂)]	=	0
[nil]	=	3
[a__sel^#(x₁, x₂)]	=	0
[mark(x₁)]	=	2
[a__sel(x₁, x₂)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 14461

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(s(X))

→

mark^#(X)

(31)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__minus^#(s(X),s(Y))

→

a__minus^#(mark(X),mark(Y))

(49)

1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(mark)

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

prec(a__minus)	=	1	status(a__minus)	=	[]	list-extension(a__minus)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__zWquot^#)	=	0	status(a__zWquot^#)	=	[1]	list-extension(a__zWquot^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(a__quot^#)	=	0	status(a__quot^#)	=	[]	list-extension(a__quot^#)	=	Lex
prec(minus)	=	1	status(minus)	=	[]	list-extension(minus)	=	Lex
prec(a__from)	=	4	status(a__from)	=	[]	list-extension(a__from)	=	Lex
prec(a__zWquot)	=	4	status(a__zWquot)	=	[1, 2]	list-extension(a__zWquot)	=	Lex
prec(zWquot)	=	4	status(zWquot)	=	[1, 2]	list-extension(zWquot)	=	Lex
prec(a__quot)	=	2	status(a__quot)	=	[1]	list-extension(a__quot)	=	Lex
prec(mark^#)	=	0	status(mark^#)	=	[]	list-extension(mark^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	2	status(quot)	=	[1]	list-extension(quot)	=	Lex
prec(from)	=	4	status(from)	=	[]	list-extension(from)	=	Lex
prec(sel)	=	0	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(a__minus^#)	=	1	status(a__minus^#)	=	[1]	list-extension(a__minus^#)	=	Lex
prec(nil)	=	5	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(a__sel^#)	=	0	status(a__sel^#)	=	[]	list-extension(a__sel^#)	=	Lex
prec(a__sel)	=	0	status(a__sel)	=	[]	list-extension(a__sel)	=	Lex
prec(cons)	=	3	status(cons)	=	[1]	list-extension(cons)	=	Lex

and the following Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[a__zWquot^#(x₁, x₂)]	=	x₁ + 1
[a__from^#(x₁)]	=	1
[a__quot^#(x₁, x₂)]	=	x₂ + 0
[minus(x₁, x₂)]	=	max(0)
[a__from(x₁)]	=	x₁ + 29284
[a__zWquot(x₁, x₂)]	=	x₁ + x₂ + 29284
[zWquot(x₁, x₂)]	=	x₁ + x₂ + 29284
[a__quot(x₁, x₂)]	=	max(x₁ + 0, 0)
[mark^#(x₁)]	=	1
[0]	=	0
[quot(x₁, x₂)]	=	max(x₁ + 0, 0)
[from(x₁)]	=	x₁ + 29284
[sel(x₁, x₂)]	=	x₂ + 29284
[a__minus^#(x₁, x₂)]	=	x₁ + 0
[nil]	=	1
[a__sel^#(x₁, x₂)]	=	x₁ + 1
[a__sel(x₁, x₂)]	=	x₂ + 29284
[cons(x₁, x₂)]	=	max(x₁ + 29283, x₂ + 0, 0)

together with the usable rules

mark(0)	→	0	(18)
a__minus(X,0)	→	0	(4)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
a__zWquot(XS,nil)	→	nil	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__from(X)	→	from(X)	(20)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)
mark(from(X))	→	a__from(mark(X))	(11)
a__zWquot(nil,XS)	→	nil	(9)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
a__quot(0,s(Y))	→	0	(6)
a__sel(0,cons(X,XS))	→	mark(X)	(2)

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

a__minus^#(s(X),s(Y))

→

a__minus^#(mark(X),mark(Y))

(49)

could be deleted.

1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__sel^#(s(N),cons(X,XS))

→

a__sel^#(mark(N),mark(XS))

(48)

1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(mark)

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

prec(a__minus)	=	2	status(a__minus)	=	[]	list-extension(a__minus)	=	Lex
prec(s)	=	2	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__zWquot^#)	=	0	status(a__zWquot^#)	=	[1]	list-extension(a__zWquot^#)	=	Lex
prec(a__from^#)	=	0	status(a__from^#)	=	[]	list-extension(a__from^#)	=	Lex
prec(a__quot^#)	=	0	status(a__quot^#)	=	[]	list-extension(a__quot^#)	=	Lex
prec(minus)	=	2	status(minus)	=	[]	list-extension(minus)	=	Lex
prec(a__from)	=	5	status(a__from)	=	[]	list-extension(a__from)	=	Lex
prec(a__zWquot)	=	5	status(a__zWquot)	=	[1, 2]	list-extension(a__zWquot)	=	Lex
prec(zWquot)	=	5	status(zWquot)	=	[1, 2]	list-extension(zWquot)	=	Lex
prec(a__quot)	=	3	status(a__quot)	=	[1]	list-extension(a__quot)	=	Lex
prec(mark^#)	=	0	status(mark^#)	=	[]	list-extension(mark^#)	=	Lex
prec(0)	=	2	status(0)	=	[]	list-extension(0)	=	Lex
prec(quot)	=	3	status(quot)	=	[1]	list-extension(quot)	=	Lex
prec(from)	=	5	status(from)	=	[]	list-extension(from)	=	Lex
prec(sel)	=	1	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(a__minus^#)	=	1	status(a__minus^#)	=	[1]	list-extension(a__minus^#)	=	Lex
prec(nil)	=	6	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(a__sel^#)	=	0	status(a__sel^#)	=	[1]	list-extension(a__sel^#)	=	Lex
prec(a__sel)	=	1	status(a__sel)	=	[]	list-extension(a__sel)	=	Lex
prec(cons)	=	4	status(cons)	=	[1]	list-extension(cons)	=	Lex

and the following Max-polynomial interpretation

[a__minus(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[a__zWquot^#(x₁, x₂)]	=	x₁ + 1
[a__from^#(x₁)]	=	1
[a__quot^#(x₁, x₂)]	=	x₂ + 0
[minus(x₁, x₂)]	=	max(0)
[a__from(x₁)]	=	x₁ + 21657
[a__zWquot(x₁, x₂)]	=	x₁ + x₂ + 55190
[zWquot(x₁, x₂)]	=	x₁ + x₂ + 55190
[a__quot(x₁, x₂)]	=	max(x₁ + 0, 0)
[mark^#(x₁)]	=	1
[0]	=	0
[quot(x₁, x₂)]	=	max(x₁ + 0, 0)
[from(x₁)]	=	x₁ + 21657
[sel(x₁, x₂)]	=	x₂ + 31893
[a__minus^#(x₁, x₂)]	=	x₁ + 0
[nil]	=	1
[a__sel^#(x₁, x₂)]	=	x₁ + 0
[a__sel(x₁, x₂)]	=	x₂ + 31893
[cons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)

together with the usable rules

mark(0)	→	0	(18)
a__minus(X,0)	→	0	(4)
mark(zWquot(X1,X2))	→	a__zWquot(mark(X1),mark(X2))	(15)
a__zWquot(XS,nil)	→	nil	(8)
a__from(X)	→	cons(mark(X),from(s(X)))	(1)
a__sel(s(N),cons(X,XS))	→	a__sel(mark(N),mark(XS))	(3)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(16)
a__sel(X1,X2)	→	sel(X1,X2)	(21)
mark(nil)	→	nil	(19)
mark(s(X))	→	s(mark(X))	(17)
a__minus(X1,X2)	→	minus(X1,X2)	(22)
a__minus(s(X),s(Y))	→	a__minus(mark(X),mark(Y))	(5)
a__zWquot(cons(X,XS),cons(Y,YS))	→	cons(a__quot(mark(X),mark(Y)),zWquot(XS,YS))	(10)
a__quot(s(X),s(Y))	→	s(a__quot(a__minus(mark(X),mark(Y)),s(mark(Y))))	(7)
a__from(X)	→	from(X)	(20)
mark(quot(X1,X2))	→	a__quot(mark(X1),mark(X2))	(14)
mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(12)
a__quot(X1,X2)	→	quot(X1,X2)	(23)
a__zWquot(X1,X2)	→	zWquot(X1,X2)	(24)
mark(from(X))	→	a__from(mark(X))	(11)
a__zWquot(nil,XS)	→	nil	(9)
mark(minus(X1,X2))	→	a__minus(mark(X1),mark(X2))	(13)
a__quot(0,s(Y))	→	0	(6)
a__sel(0,cons(X,XS))	→	mark(X)	(2)

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

a__sel^#(s(N),cons(X,XS))

→

a__sel^#(mark(N),mark(XS))

(48)

could be deleted.

1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.