Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_C)

The rewrite relation of the following TRS is considered.

active(U11(tt,N))	→	mark(N)	(1)
active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
active(U31(tt))	→	mark(0)	(3)
active(U41(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
active(and(tt,X))	→	mark(X)	(5)
active(isNat(0))	→	mark(tt)	(6)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(7)
active(isNat(s(V1)))	→	mark(isNat(V1))	(8)
active(isNat(x(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(9)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(10)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(11)
active(x(N,0))	→	mark(U31(isNat(N)))	(12)
active(x(N,s(M)))	→	mark(U41(and(isNat(M),isNat(N)),M,N))	(13)
active(U11(X1,X2))	→	U11(active(X1),X2)	(14)
active(U21(X1,X2,X3))	→	U21(active(X1),X2,X3)	(15)
active(s(X))	→	s(active(X))	(16)
active(plus(X1,X2))	→	plus(active(X1),X2)	(17)
active(plus(X1,X2))	→	plus(X1,active(X2))	(18)
active(U31(X))	→	U31(active(X))	(19)
active(U41(X1,X2,X3))	→	U41(active(X1),X2,X3)	(20)
active(x(X1,X2))	→	x(active(X1),X2)	(21)
active(x(X1,X2))	→	x(X1,active(X2))	(22)
active(and(X1,X2))	→	and(active(X1),X2)	(23)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
s(mark(X))	→	mark(s(X))	(26)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U31(mark(X))	→	mark(U31(X))	(29)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
proper(U11(X1,X2))	→	U11(proper(X1),proper(X2))	(34)
proper(tt)	→	ok(tt)	(35)
proper(U21(X1,X2,X3))	→	U21(proper(X1),proper(X2),proper(X3))	(36)
proper(s(X))	→	s(proper(X))	(37)
proper(plus(X1,X2))	→	plus(proper(X1),proper(X2))	(38)
proper(U31(X))	→	U31(proper(X))	(39)
proper(0)	→	ok(0)	(40)
proper(U41(X1,X2,X3))	→	U41(proper(X1),proper(X2),proper(X3))	(41)
proper(x(X1,X2))	→	x(proper(X1),proper(X2))	(42)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(43)
proper(isNat(X))	→	isNat(proper(X))	(44)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
s(ok(X))	→	ok(s(X))	(47)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
U31(ok(X))	→	ok(U31(X))	(49)
U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
isNat(ok(X))	→	ok(isNat(X))	(53)
top(mark(X))	→	top(proper(X))	(54)
top(ok(X))	→	top(active(X))	(55)

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.

active^#(U21(tt,M,N))	→	plus^#(N,M)	(56)
active^#(U21(X1,X2,X3))	→	U21^#(active(X1),X2,X3)	(57)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(58)
active^#(x(N,s(M)))	→	isNat^#(N)	(59)
active^#(plus(N,s(M)))	→	isNat^#(M)	(60)
top^#(mark(X))	→	top^#(proper(X))	(61)
proper^#(U11(X1,X2))	→	proper^#(X1)	(62)
U41^#(mark(X1),X2,X3)	→	U41^#(X1,X2,X3)	(63)
active^#(x(N,0))	→	isNat^#(N)	(64)
active^#(x(N,0))	→	U31^#(isNat(N))	(65)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(66)
active^#(plus(X1,X2))	→	plus^#(X1,active(X2))	(67)
active^#(U31(X))	→	active^#(X)	(68)
and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(69)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V1)	(70)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(71)
U31^#(ok(X))	→	U31^#(X)	(72)
proper^#(U21(X1,X2,X3))	→	U21^#(proper(X1),proper(X2),proper(X3))	(73)
s^#(mark(X))	→	s^#(X)	(74)
active^#(plus(N,0))	→	isNat^#(N)	(75)
proper^#(isNat(X))	→	proper^#(X)	(76)
active^#(and(X1,X2))	→	and^#(active(X1),X2)	(77)
U31^#(mark(X))	→	U31^#(X)	(78)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(79)
proper^#(U31(X))	→	U31^#(proper(X))	(80)
proper^#(U11(X1,X2))	→	proper^#(X2)	(81)
U11^#(ok(X1),ok(X2))	→	U11^#(X1,X2)	(82)
U41^#(ok(X1),ok(X2),ok(X3))	→	U41^#(X1,X2,X3)	(83)
active^#(U41(X1,X2,X3))	→	active^#(X1)	(84)
proper^#(U41(X1,X2,X3))	→	proper^#(X2)	(85)
proper^#(x(X1,X2))	→	proper^#(X1)	(86)
proper^#(U41(X1,X2,X3))	→	U41^#(proper(X1),proper(X2),proper(X3))	(87)
active^#(plus(N,0))	→	U11^#(isNat(N),N)	(88)
proper^#(U21(X1,X2,X3))	→	proper^#(X1)	(89)
top^#(ok(X))	→	active^#(X)	(90)
active^#(plus(X1,X2))	→	active^#(X1)	(91)
top^#(ok(X))	→	top^#(active(X))	(92)
active^#(s(X))	→	s^#(active(X))	(93)
proper^#(U21(X1,X2,X3))	→	proper^#(X3)	(94)
active^#(U11(X1,X2))	→	active^#(X1)	(95)
active^#(plus(X1,X2))	→	plus^#(active(X1),X2)	(96)
proper^#(U41(X1,X2,X3))	→	proper^#(X1)	(97)
active^#(isNat(x(V1,V2)))	→	isNat^#(V1)	(98)
active^#(x(X1,X2))	→	x^#(active(X1),X2)	(99)
proper^#(U31(X))	→	proper^#(X)	(100)
active^#(U41(tt,M,N))	→	x^#(N,M)	(101)
active^#(s(X))	→	active^#(X)	(102)
proper^#(U41(X1,X2,X3))	→	proper^#(X3)	(103)
plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(104)
active^#(isNat(x(V1,V2)))	→	and^#(isNat(V1),isNat(V2))	(105)
active^#(isNat(plus(V1,V2)))	→	and^#(isNat(V1),isNat(V2))	(106)
U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(107)
x^#(ok(X1),ok(X2))	→	x^#(X1,X2)	(108)
proper^#(plus(X1,X2))	→	plus^#(proper(X1),proper(X2))	(109)
active^#(U41(tt,M,N))	→	plus^#(x(N,M),N)	(110)
U21^#(ok(X1),ok(X2),ok(X3))	→	U21^#(X1,X2,X3)	(111)
active^#(and(X1,X2))	→	active^#(X1)	(112)
proper^#(x(X1,X2))	→	proper^#(X2)	(113)
active^#(plus(X1,X2))	→	active^#(X2)	(114)
active^#(x(X1,X2))	→	active^#(X2)	(115)
active^#(plus(N,s(M)))	→	U21^#(and(isNat(M),isNat(N)),M,N)	(116)
active^#(U31(X))	→	U31^#(active(X))	(117)
proper^#(and(X1,X2))	→	proper^#(X2)	(118)
active^#(U11(X1,X2))	→	U11^#(active(X1),X2)	(119)
proper^#(U11(X1,X2))	→	U11^#(proper(X1),proper(X2))	(120)
active^#(x(N,s(M)))	→	isNat^#(M)	(121)
proper^#(plus(X1,X2))	→	proper^#(X2)	(122)
active^#(plus(N,s(M)))	→	and^#(isNat(M),isNat(N))	(123)
top^#(mark(X))	→	proper^#(X)	(124)
active^#(U21(X1,X2,X3))	→	active^#(X1)	(125)
active^#(x(N,s(M)))	→	and^#(isNat(M),isNat(N))	(126)
proper^#(isNat(X))	→	isNat^#(proper(X))	(127)
s^#(ok(X))	→	s^#(X)	(128)
active^#(isNat(x(V1,V2)))	→	isNat^#(V2)	(129)
plus^#(ok(X1),ok(X2))	→	plus^#(X1,X2)	(130)
active^#(x(X1,X2))	→	x^#(X1,active(X2))	(131)
active^#(x(N,s(M)))	→	U41^#(and(isNat(M),isNat(N)),M,N)	(132)
active^#(isNat(s(V1)))	→	isNat^#(V1)	(133)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(134)
active^#(plus(N,s(M)))	→	isNat^#(N)	(135)
proper^#(plus(X1,X2))	→	proper^#(X1)	(136)
proper^#(s(X))	→	proper^#(X)	(137)
proper^#(and(X1,X2))	→	and^#(proper(X1),proper(X2))	(138)
proper^#(U21(X1,X2,X3))	→	proper^#(X2)	(139)
active^#(U21(tt,M,N))	→	s^#(plus(N,M))	(140)
active^#(isNat(plus(V1,V2)))	→	isNat^#(V2)	(141)
proper^#(x(X1,X2))	→	x^#(proper(X1),proper(X2))	(142)
proper^#(s(X))	→	s^#(proper(X))	(143)
proper^#(and(X1,X2))	→	proper^#(X1)	(144)
active^#(x(X1,X2))	→	active^#(X1)	(145)
active^#(U41(X1,X2,X3))	→	U41^#(active(X1),X2,X3)	(146)
isNat^#(ok(X))	→	isNat^#(X)	(147)

1.1 Dependency Graph Processor

The dependency pairs are split into 12 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(92)
top^#(mark(X))	→	top^#(proper(X))	(61)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(top)	=	1
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(x^#)	=	2
π(isNat)	=	1
π(active)	=	1
π(U31^#)	=	1

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

prec(U21)	=	5	status(U21)	=	[3, 2, 1]	list-extension(U21)	=	Lex
prec(U11)	=	4	status(U11)	=	[2, 1]	list-extension(U11)	=	Lex
prec(s)	=	0	status(s)	=	[1]	list-extension(s)	=	Lex
prec(isNat^#)	=	0	status(isNat^#)	=	[]	list-extension(isNat^#)	=	Lex
prec(and)	=	4	status(and)	=	[1, 2]	list-extension(and)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[1, 2]	list-extension(plus^#)	=	Lex
prec(x)	=	7	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(mark)	=	0	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(plus)	=	5	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[2, 1]	list-extension(U11^#)	=	Lex
prec(U31)	=	3	status(U31)	=	[1]	list-extension(U31)	=	Lex
prec(U41^#)	=	0	status(U41^#)	=	[1, 3, 2]	list-extension(U41^#)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[2, 1]	list-extension(U21^#)	=	Lex
prec(tt)	=	2	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U41)	=	7	status(U41)	=	[3, 2, 1]	list-extension(U41)	=	Lex
prec(and^#)	=	0	status(and^#)	=	[1, 2]	list-extension(and^#)	=	Lex

and the following Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[0]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[and^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

active(plus(X1,X2))	→	plus(X1,active(X2))	(18)
U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
active(U41(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
active(U21(X1,X2,X3))	→	U21(active(X1),X2,X3)	(15)
active(isNat(s(V1)))	→	mark(isNat(V1))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(U31(tt))	→	mark(0)	(3)
active(s(X))	→	s(active(X))	(16)
active(x(X1,X2))	→	x(active(X1),X2)	(21)
proper(U21(X1,X2,X3))	→	U21(proper(X1),proper(X2),proper(X3))	(36)
s(mark(X))	→	mark(s(X))	(26)
active(U31(X))	→	U31(active(X))	(19)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
active(plus(X1,X2))	→	plus(active(X1),X2)	(17)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
proper(U11(X1,X2))	→	U11(proper(X1),proper(X2))	(34)
active(x(X1,X2))	→	x(X1,active(X2))	(22)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
proper(isNat(X))	→	isNat(proper(X))	(44)
active(and(tt,X))	→	mark(X)	(5)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(10)
proper(U31(X))	→	U31(proper(X))	(39)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(7)
active(U41(X1,X2,X3))	→	U41(active(X1),X2,X3)	(20)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
active(U11(X1,X2))	→	U11(active(X1),X2)	(14)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
active(x(N,0))	→	mark(U31(isNat(N)))	(12)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
active(and(X1,X2))	→	and(active(X1),X2)	(23)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(11)
active(isNat(x(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(9)
active(x(N,s(M)))	→	mark(U41(and(isNat(M),isNat(N)),M,N))	(13)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
proper(0)	→	ok(0)	(40)
active(isNat(0))	→	mark(tt)	(6)
proper(plus(X1,X2))	→	plus(proper(X1),proper(X2))	(38)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
proper(s(X))	→	s(proper(X))	(37)
proper(U41(X1,X2,X3))	→	U41(proper(X1),proper(X2),proper(X3))	(41)
proper(x(X1,X2))	→	x(proper(X1),proper(X2))	(42)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
proper(tt)	→	ok(tt)	(35)
U31(mark(X))	→	mark(U31(X))	(29)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(43)
active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(61)

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

top^#(ok(X))

→

top^#(active(X))

(92)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + 0
[U11(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	x₁ + 0
[x(x₁, x₂)]	=	x₂ + 0
[proper(x₁)]	=	3
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	x₁ + 0
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	x₁ + 1
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₂ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

active(plus(X1,X2))	→	plus(X1,active(X2))	(18)
U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
active(U41(tt,M,N))	→	mark(plus(x(N,M),N))	(4)
active(U21(X1,X2,X3))	→	U21(active(X1),X2,X3)	(15)
active(isNat(s(V1)))	→	mark(isNat(V1))	(8)
active(U11(tt,N))	→	mark(N)	(1)
active(U31(tt))	→	mark(0)	(3)
active(s(X))	→	s(active(X))	(16)
active(x(X1,X2))	→	x(active(X1),X2)	(21)
proper(U21(X1,X2,X3))	→	U21(proper(X1),proper(X2),proper(X3))	(36)
s(mark(X))	→	mark(s(X))	(26)
active(U31(X))	→	U31(active(X))	(19)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
active(plus(X1,X2))	→	plus(active(X1),X2)	(17)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
proper(U11(X1,X2))	→	U11(proper(X1),proper(X2))	(34)
active(x(X1,X2))	→	x(X1,active(X2))	(22)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
proper(isNat(X))	→	isNat(proper(X))	(44)
active(and(tt,X))	→	mark(X)	(5)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
active(plus(N,0))	→	mark(U11(isNat(N),N))	(10)
proper(U31(X))	→	U31(proper(X))	(39)
active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(7)
active(U41(X1,X2,X3))	→	U41(active(X1),X2,X3)	(20)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
active(U11(X1,X2))	→	U11(active(X1),X2)	(14)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
active(x(N,0))	→	mark(U31(isNat(N)))	(12)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
active(and(X1,X2))	→	and(active(X1),X2)	(23)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(11)
active(isNat(x(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(9)
active(x(N,s(M)))	→	mark(U41(and(isNat(M),isNat(N)),M,N))	(13)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
proper(0)	→	ok(0)	(40)
active(isNat(0))	→	mark(tt)	(6)
proper(plus(X1,X2))	→	plus(proper(X1),proper(X2))	(38)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
proper(s(X))	→	s(proper(X))	(37)
proper(U41(X1,X2,X3))	→	U41(proper(X1),proper(X2),proper(X3))	(41)
proper(x(X1,X2))	→	x(proper(X1),proper(X2))	(42)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
proper(tt)	→	ok(tt)	(35)
U31(mark(X))	→	mark(U31(X))	(29)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(43)
active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(92)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

proper^#(and(X1,X2))	→	proper^#(X1)	(144)
proper^#(U41(X1,X2,X3))	→	proper^#(X3)	(103)
proper^#(U31(X))	→	proper^#(X)	(100)
proper^#(U41(X1,X2,X3))	→	proper^#(X1)	(97)
proper^#(U21(X1,X2,X3))	→	proper^#(X3)	(94)
proper^#(U21(X1,X2,X3))	→	proper^#(X2)	(139)
proper^#(s(X))	→	proper^#(X)	(137)
proper^#(plus(X1,X2))	→	proper^#(X1)	(136)
proper^#(U21(X1,X2,X3))	→	proper^#(X1)	(89)
proper^#(x(X1,X2))	→	proper^#(X1)	(86)
proper^#(U41(X1,X2,X3))	→	proper^#(X2)	(85)
proper^#(U11(X1,X2))	→	proper^#(X2)	(81)
proper^#(isNat(X))	→	proper^#(X)	(76)
proper^#(plus(X1,X2))	→	proper^#(X2)	(122)
proper^#(and(X1,X2))	→	proper^#(X2)	(118)
proper^#(x(X1,X2))	→	proper^#(X2)	(113)
proper^#(U11(X1,X2))	→	proper^#(X1)	(62)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	0
[ok(x₁)]	=	17891
[0]	=	10282
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	x₁ + 0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	0
[U31(x₁)]	=	x₁ + 6617
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	9123
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

proper^#(and(X1,X2))	→	proper^#(X1)	(144)
proper^#(U41(X1,X2,X3))	→	proper^#(X3)	(103)
proper^#(U31(X))	→	proper^#(X)	(100)
proper^#(U41(X1,X2,X3))	→	proper^#(X1)	(97)
proper^#(U21(X1,X2,X3))	→	proper^#(X3)	(94)
proper^#(U21(X1,X2,X3))	→	proper^#(X2)	(139)
proper^#(s(X))	→	proper^#(X)	(137)
proper^#(plus(X1,X2))	→	proper^#(X1)	(136)
proper^#(U21(X1,X2,X3))	→	proper^#(X1)	(89)
proper^#(x(X1,X2))	→	proper^#(X1)	(86)
proper^#(U41(X1,X2,X3))	→	proper^#(X2)	(85)
proper^#(U11(X1,X2))	→	proper^#(X2)	(81)
proper^#(isNat(X))	→	proper^#(X)	(76)
proper^#(plus(X1,X2))	→	proper^#(X2)	(122)
proper^#(and(X1,X2))	→	proper^#(X2)	(118)
proper^#(x(X1,X2))	→	proper^#(X2)	(113)
proper^#(U11(X1,X2))	→	proper^#(X1)	(62)

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

active^#(x(X1,X2))	→	active^#(X1)	(145)
active^#(s(X))	→	active^#(X)	(102)
active^#(U11(X1,X2))	→	active^#(X1)	(95)
active^#(plus(X1,X2))	→	active^#(X1)	(91)
active^#(U41(X1,X2,X3))	→	active^#(X1)	(84)
active^#(U21(X1,X2,X3))	→	active^#(X1)	(125)
active^#(U31(X))	→	active^#(X)	(68)
active^#(x(X1,X2))	→	active^#(X2)	(115)
active^#(plus(X1,X2))	→	active^#(X2)	(114)
active^#(and(X1,X2))	→	active^#(X1)	(112)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 1
[proper(x₁)]	=	0
[ok(x₁)]	=	1
[0]	=	9133
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	0
[U31(x₁)]	=	x₁ + 6617
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	x₁ + 0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	9123
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

active^#(x(X1,X2))	→	active^#(X1)	(145)
active^#(s(X))	→	active^#(X)	(102)
active^#(U11(X1,X2))	→	active^#(X1)	(95)
active^#(plus(X1,X2))	→	active^#(X1)	(91)
active^#(U41(X1,X2,X3))	→	active^#(X1)	(84)
active^#(U21(X1,X2,X3))	→	active^#(X1)	(125)
active^#(U31(X))	→	active^#(X)	(68)
active^#(x(X1,X2))	→	active^#(X2)	(115)
active^#(plus(X1,X2))	→	active^#(X2)	(114)
active^#(and(X1,X2))	→	active^#(X1)	(112)

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

U41^#(ok(X1),ok(X2),ok(X3))	→	U41^#(X1,X2,X3)	(83)
U41^#(mark(X1),X2,X3)	→	U41^#(X1,X2,X3)	(63)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	0
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	x₂ + 0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
and(mark(X1),X2)	→	mark(and(X1,X2))	(33)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(52)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

U41^#(ok(X1),ok(X2),ok(X3))

→

U41^#(X1,X2,X3)

(83)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U41^#(mark(X1),X2,X3)

→

U41^#(X1,X2,X3)

(63)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 20253
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 2
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 2631
[U41^#(x₁, x₂, x₃)]	=	x₁ + 0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

U41^#(mark(X1),X2,X3)

→

U41^#(X1,X2,X3)

(63)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

and^#(mark(X1),X2)	→	and^#(X1,X2)	(79)
and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(69)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 17979
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 2
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	x₁ + 0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

and^#(mark(X1),X2)	→	and^#(X1,X2)	(79)
and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(69)

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

U11^#(ok(X1),ok(X2))	→	U11^#(X1,X2)	(82)
U11^#(mark(X1),X2)	→	U11^#(X1,X2)	(66)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 21639
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	x₂ + 0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 32299
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

U11^#(ok(X1),ok(X2))

→

U11^#(X1,X2)

(82)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U11^#(mark(X1),X2)

→

U11^#(X1,X2)

(66)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 21639
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 15530
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	x₁ + 0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

U11^#(mark(X1),X2)

→

U11^#(X1,X2)

(66)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

U31^#(mark(X))	→	U31^#(X)	(78)
U31^#(ok(X))	→	U31^#(X)	(72)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[U11(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₂ + 21639
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + x₂ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 7362
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U31^#(x₁)]	=	x₁ + 0
[and^#(x₁, x₂)]	=	0

together with the usable rules

U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(50)
s(mark(X))	→	mark(s(X))	(26)
x(X1,mark(X2))	→	mark(x(X1,X2))	(32)
plus(mark(X1),X2)	→	mark(plus(X1,X2))	(27)
plus(X1,mark(X2))	→	mark(plus(X1,X2))	(28)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(25)
U31(ok(X))	→	ok(U31(X))	(49)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(30)
x(mark(X1),X2)	→	mark(x(X1,X2))	(31)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(45)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(24)
x(ok(X1),ok(X2))	→	ok(x(X1,X2))	(51)
plus(ok(X1),ok(X2))	→	ok(plus(X1,X2))	(48)
isNat(ok(X))	→	ok(isNat(X))	(53)
s(ok(X))	→	ok(s(X))	(47)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(46)
U31(mark(X))	→	mark(U31(X))	(29)

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

U31^#(mark(X))	→	U31^#(X)	(78)
U31^#(ok(X))	→	U31^#(X)	(72)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

s^#(ok(X))	→	s^#(X)	(128)
s^#(mark(X))	→	s^#(X)	(74)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₃ + 8703
[U11(x₁, x₂)]	=	21332
[s(x₁)]	=	x₁ + 1
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	28939
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	11404
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	8137
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	27073
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

s^#(ok(X))	→	s^#(X)	(128)
s^#(mark(X))	→	s^#(X)	(74)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

isNat^#(ok(X))

→

isNat^#(X)

(147)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	2
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	2
[isNat^#(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	2
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	17037
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	3
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	31607
[plus(x₁, x₂)]	=	x₂ + 2
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	x₁ + 1
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	x₂ + 2
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

isNat^#(ok(X))

→

isNat^#(X)

(147)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

U21^#(mark(X1),X2,X3)	→	U21^#(X1,X2,X3)	(107)
U21^#(ok(X1),ok(X2),ok(X3))	→	U21^#(X1,X2,X3)	(111)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	21541
[U11(x₁, x₂)]	=	27531
[s(x₁)]	=	29829
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	15093
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	29305
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[0]	=	17037
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 24228
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	31607
[plus(x₁, x₂)]	=	x₁ + 2160
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	2
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	x₂ + 0
[tt]	=	3288
[U41(x₁, x₂, x₃)]	=	x₂ + 2
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

U21^#(ok(X1),ok(X2),ok(X3))

→

U21^#(X1,X2,X3)

(111)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U21^#(mark(X1),X2,X3)

→

U21^#(X1,X2,X3)

(107)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	23033
[U11(x₁, x₂)]	=	23724
[s(x₁)]	=	12771
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	29351
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	21966
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 18418
[0]	=	17037
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 15079
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	29007
[plus(x₁, x₂)]	=	x₁ + 7675
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	2
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	x₁ + 0
[tt]	=	28472
[U41(x₁, x₂, x₃)]	=	24813
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

U21^#(mark(X1),X2,X3)

→

U21^#(X1,X2,X3)

(107)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

x^#(ok(X1),ok(X2))	→	x^#(X1,X2)	(108)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(71)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(58)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	2
[U11(x₁, x₂)]	=	23724
[s(x₁)]	=	19079
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2992
[plus^#(x₁, x₂)]	=	0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	21966
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 9251
[0]	=	1
[x^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 15079
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	2
[plus(x₁, x₂)]	=	x₁ + 879
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	13421
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	6753
[U41(x₁, x₂, x₃)]	=	21796
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

x^#(ok(X1),ok(X2))	→	x^#(X1,X2)	(108)
x^#(X1,mark(X2))	→	x^#(X1,X2)	(71)
x^#(mark(X1),X2)	→	x^#(X1,X2)	(58)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

plus^#(X1,mark(X2))	→	plus^#(X1,X2)	(104)
plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(134)
plus^#(ok(X1),ok(X2))	→	plus^#(X1,X2)	(130)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[U11(x₁, x₂)]	=	2
[s(x₁)]	=	12783
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2
[plus^#(x₁, x₂)]	=	x₁ + 0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	21966
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 4092
[0]	=	20540
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4331
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	2
[plus(x₁, x₂)]	=	x₁ + 9556
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	37711
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	16542
[U41(x₁, x₂, x₃)]	=	19691
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

plus^#(mark(X1),X2)	→	plus^#(X1,X2)	(134)
plus^#(ok(X1),ok(X2))	→	plus^#(X1,X2)	(130)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(X1,mark(X2))

→

plus^#(X1,X2)

(104)

1.1.12.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[U11(x₁, x₂)]	=	6559
[s(x₁)]	=	2954
[isNat^#(x₁)]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	2
[plus^#(x₁, x₂)]	=	x₂ + 0
[top^#(x₁)]	=	0
[x(x₁, x₂)]	=	21966
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 3
[0]	=	20540
[x^#(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 4331
[proper^#(x₁)]	=	0
[isNat(x₁)]	=	14652
[plus(x₁, x₂)]	=	x₁ + 16161
[U11^#(x₁, x₂)]	=	0
[active(x₁)]	=	1
[U31(x₁)]	=	28085
[U41^#(x₁, x₂, x₃)]	=	0
[active^#(x₁)]	=	0
[U21^#(x₁, x₂, x₃)]	=	0
[tt]	=	1
[U41(x₁, x₂, x₃)]	=	2
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	0

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

plus^#(X1,mark(X2))

→

plus^#(X1,X2)

(104)

could be deleted.

1.1.12.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.