Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_noand_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U12(tt)	→	tt	(2)
a__U21(tt)	→	tt	(3)
a__U31(tt,N)	→	mark(N)	(4)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__isNat(0)	→	tt	(7)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
mark(U12(X))	→	a__U12(mark(X))	(13)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U21(X))	→	a__U21(mark(X))	(15)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(tt)	→	tt	(20)
mark(s(X))	→	s(mark(X))	(21)
mark(0)	→	0	(22)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__isNat(X)	→	isNat(X)	(25)
a__U21(X)	→	U21(X)	(26)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__plus(X1,X2)	→	plus(X1,X2)	(30)

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.

a__U42^#(tt,M,N)	→	mark^#(N)	(31)
mark^#(U21(X))	→	a__U21^#(mark(X))	(32)
a__isNat^#(s(V1))	→	a__U21^#(a__isNat(V1))	(33)
a__plus^#(N,0)	→	a__U31^#(a__isNat(N),N)	(34)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(35)
mark^#(U11(X1,X2))	→	mark^#(X1)	(36)
mark^#(U31(X1,X2))	→	mark^#(X1)	(37)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(38)
mark^#(isNat(X))	→	a__isNat^#(X)	(39)
a__U31^#(tt,N)	→	mark^#(N)	(40)
a__plus^#(N,0)	→	a__isNat^#(N)	(41)
mark^#(U21(X))	→	mark^#(X)	(42)
a__U11^#(tt,V2)	→	a__U12^#(a__isNat(V2))	(43)
mark^#(plus(X1,X2))	→	mark^#(X1)	(44)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(45)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(46)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(47)
mark^#(U12(X))	→	mark^#(X)	(48)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(49)
mark^#(s(X))	→	mark^#(X)	(50)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(51)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(52)
mark^#(U42(X1,X2,X3))	→	a__U42^#(mark(X1),X2,X3)	(53)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(54)
a__U11^#(tt,V2)	→	a__isNat^#(V2)	(55)
mark^#(plus(X1,X2))	→	mark^#(X2)	(56)
a__U41^#(tt,M,N)	→	a__isNat^#(N)	(57)
a__U42^#(tt,M,N)	→	mark^#(M)	(58)
a__U42^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(59)
a__plus^#(N,s(M))	→	a__U41^#(a__isNat(M),M,N)	(60)
a__U41^#(tt,M,N)	→	a__U42^#(a__isNat(N),M,N)	(61)
mark^#(U12(X))	→	a__U12^#(mark(X))	(62)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(63)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(63)
mark^#(U21(X))	→	mark^#(X)	(42)
a__U41^#(tt,M,N)	→	a__U42^#(a__isNat(N),M,N)	(61)
a__U31^#(tt,N)	→	mark^#(N)	(40)
a__plus^#(N,s(M))	→	a__U41^#(a__isNat(M),M,N)	(60)
a__U42^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(59)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(38)
a__U42^#(tt,M,N)	→	mark^#(M)	(58)
mark^#(U31(X1,X2))	→	mark^#(X1)	(37)
mark^#(plus(X1,X2))	→	mark^#(X2)	(56)
mark^#(U11(X1,X2))	→	mark^#(X1)	(36)
a__plus^#(N,0)	→	a__U31^#(a__isNat(N),N)	(34)
mark^#(U42(X1,X2,X3))	→	a__U42^#(mark(X1),X2,X3)	(53)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(54)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(52)
mark^#(s(X))	→	mark^#(X)	(50)
mark^#(U12(X))	→	mark^#(X)	(48)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(47)
a__U42^#(tt,M,N)	→	mark^#(N)	(31)
mark^#(plus(X1,X2))	→	mark^#(X1)	(44)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U21(x₁)]	=	x₁ + 0
[U11(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 15924
[a__U31^#(x₁, x₂)]	=	x₂ + 8946
[U42(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 15924
[a__isNat^#(x₁)]	=	0
[a__U11^#(x₁, x₂)]	=	0
[a__U31(x₁, x₂)]	=	x₁ + x₂ + 8947
[U12(x₁)]	=	x₁ + 0
[a__U42^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[a__U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 15924
[a__U12^#(x₁)]	=	0
[a__U21^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	8947
[a__U21(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + 0
[a__U42(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 15924
[a__U12(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U31(x₁, x₂)]	=	x₁ + x₂ + 8947
[a__U41^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[tt]	=	1
[a__isNat(x₁)]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 15924

together with the usable rules

mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
a__U31(tt,N)	→	mark(N)	(4)
mark(U21(X))	→	a__U21(mark(X))	(15)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U21(tt)	→	tt	(3)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(21)
a__U21(X)	→	U21(X)	(26)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
mark(0)	→	0	(22)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__isNat(0)	→	tt	(7)
mark(tt)	→	tt	(20)
a__isNat(X)	→	isNat(X)	(25)
a__plus(X1,X2)	→	plus(X1,X2)	(30)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
mark(U12(X))	→	a__U12(mark(X))	(13)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__U12(tt)	→	tt	(2)

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

mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(63)
a__U41^#(tt,M,N)	→	a__U42^#(a__isNat(N),M,N)	(61)
a__U31^#(tt,N)	→	mark^#(N)	(40)
a__plus^#(N,s(M))	→	a__U41^#(a__isNat(M),M,N)	(60)
a__U42^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(59)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(38)
a__U42^#(tt,M,N)	→	mark^#(M)	(58)
mark^#(U31(X1,X2))	→	mark^#(X1)	(37)
mark^#(plus(X1,X2))	→	mark^#(X2)	(56)
a__plus^#(N,0)	→	a__U31^#(a__isNat(N),N)	(34)
mark^#(U42(X1,X2,X3))	→	a__U42^#(mark(X1),X2,X3)	(53)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(54)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(52)
mark^#(s(X))	→	mark^#(X)	(50)
mark^#(U42(X1,X2,X3))	→	mark^#(X1)	(47)
a__U42^#(tt,M,N)	→	mark^#(N)	(31)
mark^#(plus(X1,X2))	→	mark^#(X1)	(44)

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^#(U21(X))	→	mark^#(X)	(42)
mark^#(U11(X1,X2))	→	mark^#(X1)	(36)
mark^#(U12(X))	→	mark^#(X)	(48)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 53516
[U21(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	x₁ + 45789
[a__U31^#(x₁, x₂)]	=	8946
[U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 99305
[a__isNat^#(x₁)]	=	0
[a__U11^#(x₁, x₂)]	=	0
[a__U31(x₁, x₂)]	=	x₂ + 591
[U12(x₁)]	=	x₁ + 0
[a__U42^#(x₁, x₂, x₃)]	=	1
[a__U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 99305
[a__U12^#(x₁)]	=	0
[a__U21^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	3081
[a__U21(x₁)]	=	x₁ + 1
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 99305
[a__U12(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 28313
[plus(x₁, x₂)]	=	x₁ + x₂ + 53516
[U31(x₁, x₂)]	=	x₂ + 591
[a__U41^#(x₁, x₂, x₃)]	=	2
[tt]	=	28313
[a__isNat(x₁)]	=	x₁ + 28313
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 99305

together with the usable rules

mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
a__U31(tt,N)	→	mark(N)	(4)
mark(U21(X))	→	a__U21(mark(X))	(15)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U21(tt)	→	tt	(3)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(21)
a__U21(X)	→	U21(X)	(26)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
mark(0)	→	0	(22)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__isNat(0)	→	tt	(7)
mark(tt)	→	tt	(20)
a__isNat(X)	→	isNat(X)	(25)
a__plus(X1,X2)	→	plus(X1,X2)	(30)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
mark(U12(X))	→	a__U12(mark(X))	(13)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__U12(tt)	→	tt	(2)

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

mark^#(U21(X))

→

mark^#(X)

(42)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U11(X1,X2))	→	mark^#(X1)	(36)
mark^#(U12(X))	→	mark^#(X)	(48)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U21(x₁)]	=	x₁ + 28224
[U11(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	x₁ + 28226
[a__U31^#(x₁, x₂)]	=	8946
[U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__isNat^#(x₁)]	=	0
[a__U11^#(x₁, x₂)]	=	0
[a__U31(x₁, x₂)]	=	x₂ + 2
[U12(x₁)]	=	x₁ + 1
[a__U42^#(x₁, x₂, x₃)]	=	1
[a__U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12^#(x₁)]	=	0
[a__U21^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[a__U21(x₁)]	=	x₁ + 28224
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 61131
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U31(x₁, x₂)]	=	x₂ + 2
[a__U41^#(x₁, x₂, x₃)]	=	2
[tt]	=	61132
[a__isNat(x₁)]	=	x₁ + 61131
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227

together with the usable rules

mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
a__U31(tt,N)	→	mark(N)	(4)
mark(U21(X))	→	a__U21(mark(X))	(15)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U21(tt)	→	tt	(3)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(21)
a__U21(X)	→	U21(X)	(26)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
mark(0)	→	0	(22)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__isNat(0)	→	tt	(7)
mark(tt)	→	tt	(20)
a__isNat(X)	→	isNat(X)	(25)
a__plus(X1,X2)	→	plus(X1,X2)	(30)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
mark(U12(X))	→	a__U12(mark(X))	(13)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__U12(tt)	→	tt	(2)

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

mark^#(U12(X))

→

mark^#(X)

(48)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U11(X1,X2))

→

mark^#(X1)

(36)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U21(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 28226
[a__U31^#(x₁, x₂)]	=	8946
[U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__isNat^#(x₁)]	=	0
[a__U11^#(x₁, x₂)]	=	0
[a__U31(x₁, x₂)]	=	x₂ + 2
[U12(x₁)]	=	x₁ + 1
[a__U42^#(x₁, x₂, x₃)]	=	1
[a__U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12^#(x₁)]	=	0
[a__U21^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[a__U21(x₁)]	=	x₁ + 1
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12(x₁)]	=	x₁ + 1
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U31(x₁, x₂)]	=	x₂ + 2
[a__U41^#(x₁, x₂, x₃)]	=	2
[tt]	=	1
[a__isNat(x₁)]	=	x₁ + 1
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227

together with the usable rules

mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
a__U31(tt,N)	→	mark(N)	(4)
mark(U21(X))	→	a__U21(mark(X))	(15)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U21(tt)	→	tt	(3)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(21)
a__U21(X)	→	U21(X)	(26)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
mark(0)	→	0	(22)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__isNat(0)	→	tt	(7)
mark(tt)	→	tt	(20)
a__isNat(X)	→	isNat(X)	(25)
a__plus(X1,X2)	→	plus(X1,X2)	(30)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
mark(U12(X))	→	a__U12(mark(X))	(13)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__U12(tt)	→	tt	(2)

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

mark^#(U11(X1,X2))

→

mark^#(X1)

(36)

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__U11^#(tt,V2)	→	a__isNat^#(V2)	(55)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(51)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(49)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(45)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 2
[U21(x₁)]	=	x₁ + 1
[U11(x₁, x₂)]	=	x₁ + x₂ + 2
[s(x₁)]	=	x₁ + 28225
[a__U31^#(x₁, x₂)]	=	8946
[U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__isNat^#(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂)]	=	x₂ + 1
[a__U31(x₁, x₂)]	=	x₂ + 3
[U12(x₁)]	=	x₁ + 2
[a__U42^#(x₁, x₂, x₃)]	=	1
[a__U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12^#(x₁)]	=	0
[a__U21^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mark^#(x₁)]	=	0
[0]	=	1
[a__U21(x₁)]	=	x₁ + 1
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U42(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227
[a__U12(x₁)]	=	x₁ + 2
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 2
[U31(x₁, x₂)]	=	x₂ + 3
[a__U41^#(x₁, x₂, x₃)]	=	2
[tt]	=	1
[a__isNat(x₁)]	=	x₁ + 1
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 28227

together with the usable rules

mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(18)
a__U31(tt,N)	→	mark(N)	(4)
mark(U21(X))	→	a__U21(mark(X))	(15)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(8)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U21(tt)	→	tt	(3)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(16)
mark(s(X))	→	s(mark(X))	(21)
a__U21(X)	→	U21(X)	(26)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(19)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(17)
a__U31(X1,X2)	→	U31(X1,X2)	(27)
mark(0)	→	0	(22)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(28)
a__U41(tt,M,N)	→	a__U42(a__isNat(N),M,N)	(5)
a__plus(N,0)	→	a__U31(a__isNat(N),N)	(10)
a__isNat(0)	→	tt	(7)
mark(tt)	→	tt	(20)
a__isNat(X)	→	isNat(X)	(25)
a__plus(X1,X2)	→	plus(X1,X2)	(30)
mark(isNat(X))	→	a__isNat(X)	(14)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(12)
a__U11(X1,X2)	→	U11(X1,X2)	(23)
a__U12(X)	→	U12(X)	(24)
a__plus(N,s(M))	→	a__U41(a__isNat(M),M,N)	(11)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(9)
mark(U12(X))	→	a__U12(mark(X))	(13)
a__U42(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(6)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(29)
a__U12(tt)	→	tt	(2)

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

a__U11^#(tt,V2)	→	a__isNat^#(V2)	(55)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(51)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(49)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(45)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.