Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)
a__U13(tt)	→	tt	(3)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,N)	→	mark(N)	(6)
a__U41(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(7)
a__and(tt,X)	→	mark(X)	(8)
a__isNat(0)	→	tt	(9)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(10)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(11)
a__isNatKind(0)	→	tt	(12)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(13)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(14)
a__plus(N,0)	→	a__U31(a__and(a__isNat(N),isNatKind(N)),N)	(15)
a__plus(N,s(M))	→	a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(16)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(17)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(18)
mark(isNat(X))	→	a__isNat(X)	(19)
mark(U13(X))	→	a__U13(mark(X))	(20)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(21)
mark(U22(X))	→	a__U22(mark(X))	(22)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(23)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(24)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(25)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(26)
mark(isNatKind(X))	→	a__isNatKind(X)	(27)
mark(tt)	→	tt	(28)
mark(s(X))	→	s(mark(X))	(29)
mark(0)	→	0	(30)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(31)
a__U12(X1,X2)	→	U12(X1,X2)	(32)
a__isNat(X)	→	isNat(X)	(33)
a__U13(X)	→	U13(X)	(34)
a__U21(X1,X2)	→	U21(X1,X2)	(35)
a__U22(X)	→	U22(X)	(36)
a__U31(X1,X2)	→	U31(X1,X2)	(37)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(38)
a__plus(X1,X2)	→	plus(X1,X2)	(39)
a__and(X1,X2)	→	and(X1,X2)	(40)
a__isNatKind(X)	→	isNatKind(X)	(41)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(42)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(43)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(44)
a__U12^#(tt,V2)	→	a__U13^#(a__isNat(V2))	(45)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(46)
a__U21^#(tt,V1)	→	a__U22^#(a__isNat(V1))	(47)
a__U31^#(tt,N)	→	mark^#(N)	(48)
a__U41^#(tt,M,N)	→	mark^#(M)	(49)
a__U41^#(tt,M,N)	→	mark^#(N)	(50)
a__U41^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(51)
a__and^#(tt,X)	→	mark^#(X)	(52)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(53)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(54)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(55)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(56)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(57)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(58)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(59)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(60)
a__plus^#(N,0)	→	a__isNat^#(N)	(61)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(62)
a__plus^#(N,0)	→	a__U31^#(a__and(a__isNat(N),isNatKind(N)),N)	(63)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(64)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(65)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(66)
a__plus^#(N,s(M))	→	a__U41^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(67)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(68)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(69)
mark^#(U12(X1,X2))	→	mark^#(X1)	(70)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(71)
mark^#(isNat(X))	→	a__isNat^#(X)	(72)
mark^#(U13(X))	→	mark^#(X)	(73)
mark^#(U13(X))	→	a__U13^#(mark(X))	(74)
mark^#(U21(X1,X2))	→	mark^#(X1)	(75)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(76)
mark^#(U22(X))	→	mark^#(X)	(77)
mark^#(U22(X))	→	a__U22^#(mark(X))	(78)
mark^#(U31(X1,X2))	→	mark^#(X1)	(79)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(80)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(82)
mark^#(plus(X1,X2))	→	mark^#(X2)	(83)
mark^#(plus(X1,X2))	→	mark^#(X1)	(84)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(85)
mark^#(and(X1,X2))	→	mark^#(X1)	(86)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(87)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(88)
mark^#(s(X))	→	mark^#(X)	(89)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(58)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(59)
a__and^#(tt,X)	→	mark^#(X)	(52)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(68)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(69)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(42)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(53)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(60)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(54)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(55)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(43)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(44)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(56)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(57)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(46)
mark^#(U12(X1,X2))	→	mark^#(X1)	(70)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(71)
mark^#(isNat(X))	→	a__isNat^#(X)	(72)
mark^#(U13(X))	→	mark^#(X)	(73)
mark^#(U21(X1,X2))	→	mark^#(X1)	(75)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(76)
mark^#(U22(X))	→	mark^#(X)	(77)
mark^#(U31(X1,X2))	→	mark^#(X1)	(79)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(80)
a__U31^#(tt,N)	→	mark^#(N)	(48)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(82)
a__U41^#(tt,M,N)	→	mark^#(M)	(49)
mark^#(plus(X1,X2))	→	mark^#(X2)	(83)
mark^#(plus(X1,X2))	→	mark^#(X1)	(84)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(85)
a__plus^#(N,0)	→	a__isNat^#(N)	(61)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(62)
a__plus^#(N,0)	→	a__U31^#(a__and(a__isNat(N),isNatKind(N)),N)	(63)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(64)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(65)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(66)
a__plus^#(N,s(M))	→	a__U41^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(67)
a__U41^#(tt,M,N)	→	mark^#(N)	(50)
mark^#(and(X1,X2))	→	mark^#(X1)	(86)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(87)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(88)
mark^#(s(X))	→	mark^#(X)	(89)
a__U41^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(51)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[and(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U13(x₁)]	=	0 · x₁ + 0
[a__isNatKind(x₁)]	=	0 · x₁ + 0
[mark(x₁)]	=	0 · x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + 0
[a__U12(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[isNatKind(x₁)]	=	0 · x₁ + -∞
[U13(x₁)]	=	0 · x₁ + -∞
[a__and^#(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + -∞
[a__U11^#(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + 0
[a__U31^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U11(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + 0
[isNat(x₁)]	=	0 · x₁ + -∞
[a__isNat^#(x₁)]	=	0 · x₁ + -∞
[a__U41^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 7 · x₃ + 0
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U12^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[mark^#(x₁)]	=	0 · x₁ + -∞
[a__plus(x₁, x₂)]	=	7 · x₁ + 0 · x₂ + 7
[tt]	=	7
[a__U31(x₁, x₂)]	=	0 · x₁ + 7 · x₂ + 3
[U12(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U41(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 7 · x₃ + 2
[a__U21^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[plus(x₁, x₂)]	=	7 · x₁ + 0 · x₂ + 7
[a__and(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U22(x₁)]	=	0 · x₁ + -∞
[U31(x₁, x₂)]	=	0 · x₁ + 7 · x₂ + 3
[s(x₁)]	=	0 · x₁ + 0
[a__U41(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 7 · x₃ + 2
[0]	=	7
[a__U22(x₁)]	=	0 · x₁ + 0
[a__isNatKind^#(x₁)]	=	0 · x₁ + -∞
[a__plus^#(x₁, x₂)]	=	7 · x₁ + 0 · x₂ + 0
[a__isNat(x₁)]	=	0 · x₁ + 0

together with the usable rules

a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)
a__U13(tt)	→	tt	(3)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,N)	→	mark(N)	(6)
a__U41(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(7)
a__and(tt,X)	→	mark(X)	(8)
a__isNat(0)	→	tt	(9)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(10)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(11)
a__isNatKind(0)	→	tt	(12)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(13)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(14)
a__plus(N,0)	→	a__U31(a__and(a__isNat(N),isNatKind(N)),N)	(15)
a__plus(N,s(M))	→	a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(16)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(17)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(18)
mark(isNat(X))	→	a__isNat(X)	(19)
mark(U13(X))	→	a__U13(mark(X))	(20)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(21)
mark(U22(X))	→	a__U22(mark(X))	(22)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(23)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(24)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(25)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(26)
mark(isNatKind(X))	→	a__isNatKind(X)	(27)
mark(tt)	→	tt	(28)
mark(s(X))	→	s(mark(X))	(29)
mark(0)	→	0	(30)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(31)
a__U12(X1,X2)	→	U12(X1,X2)	(32)
a__isNat(X)	→	isNat(X)	(33)
a__U13(X)	→	U13(X)	(34)
a__U21(X1,X2)	→	U21(X1,X2)	(35)
a__U22(X)	→	U22(X)	(36)
a__U31(X1,X2)	→	U31(X1,X2)	(37)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(38)
a__plus(X1,X2)	→	plus(X1,X2)	(39)
a__and(X1,X2)	→	and(X1,X2)	(40)
a__isNatKind(X)	→	isNatKind(X)	(41)

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

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(58)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(42)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(53)
mark^#(plus(X1,X2))	→	mark^#(X1)	(84)
a__plus^#(N,0)	→	a__isNat^#(N)	(61)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(62)
a__plus^#(N,0)	→	a__U31^#(a__and(a__isNat(N),isNatKind(N)),N)	(63)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(66)
a__U41^#(tt,M,N)	→	mark^#(N)	(50)

could be deleted.

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[and(x₁, x₂)]	=	2 · x₁ + 1 · x₂ + 0
[a__U13(x₁)]	=	1 · x₁ + 0
[a__isNatKind(x₁)]	=	0 · x₁ + 0
[mark(x₁)]	=	1 · x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	1 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U12(x₁, x₂)]	=	4 · x₁ + 0 · x₂ + 0
[isNatKind(x₁)]	=	0 · x₁ + 0
[U13(x₁)]	=	1 · x₁ + 0
[a__and^#(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + 0
[a__U11^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U31^#(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + 0
[U11(x₁, x₂, x₃)]	=	1 · x₁ + 0 · x₂ + 0 · x₃ + 0
[isNat(x₁)]	=	0 · x₁ + 0
[a__isNat^#(x₁)]	=	0 · x₁ + 0
[a__U41^#(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + 0
[U21(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + 0
[a__U12^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U21(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + 0
[mark^#(x₁)]	=	4 · x₁ + 0
[a__plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[tt]	=	0
[a__U31(x₁, x₂)]	=	4 · x₁ + 1 · x₂ + 0
[U12(x₁, x₂)]	=	4 · x₁ + 0 · x₂ + 0
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃ + 1
[a__U21^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[a__and(x₁, x₂)]	=	2 · x₁ + 1 · x₂ + 0
[U22(x₁)]	=	4 · x₁ + 0
[U31(x₁, x₂)]	=	4 · x₁ + 1 · x₂ + 0
[s(x₁)]	=	1 · x₁ + 1
[a__U41(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃ + 1
[0]	=	0
[a__U22(x₁)]	=	4 · x₁ + 0
[a__isNatKind^#(x₁)]	=	0 · x₁ + 0
[a__plus^#(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + 0
[a__isNat(x₁)]	=	0 · x₁ + 0

together with the usable rules

a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)
a__U13(tt)	→	tt	(3)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,N)	→	mark(N)	(6)
a__U41(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(7)
a__and(tt,X)	→	mark(X)	(8)
a__isNat(0)	→	tt	(9)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(10)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(11)
a__isNatKind(0)	→	tt	(12)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(13)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(14)
a__plus(N,0)	→	a__U31(a__and(a__isNat(N),isNatKind(N)),N)	(15)
a__plus(N,s(M))	→	a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(16)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(17)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(18)
mark(isNat(X))	→	a__isNat(X)	(19)
mark(U13(X))	→	a__U13(mark(X))	(20)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(21)
mark(U22(X))	→	a__U22(mark(X))	(22)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(23)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(24)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(25)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(26)
mark(isNatKind(X))	→	a__isNatKind(X)	(27)
mark(tt)	→	tt	(28)
mark(s(X))	→	s(mark(X))	(29)
mark(0)	→	0	(30)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(31)
a__U12(X1,X2)	→	U12(X1,X2)	(32)
a__isNat(X)	→	isNat(X)	(33)
a__U13(X)	→	U13(X)	(34)
a__U21(X1,X2)	→	U21(X1,X2)	(35)
a__U22(X)	→	U22(X)	(36)
a__U31(X1,X2)	→	U31(X1,X2)	(37)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(38)
a__plus(X1,X2)	→	plus(X1,X2)	(39)
a__and(X1,X2)	→	and(X1,X2)	(40)
a__isNatKind(X)	→	isNatKind(X)	(41)

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

mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(81)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(82)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(64)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(65)
a__plus^#(N,s(M))	→	a__U41^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(67)
mark^#(s(X))	→	mark^#(X)	(89)

could be deleted.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(59)
a__and^#(tt,X)	→	mark^#(X)	(52)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(68)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(69)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(43)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(44)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(54)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(55)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(56)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(60)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(57)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(46)
mark^#(U12(X1,X2))	→	mark^#(X1)	(70)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(71)
mark^#(isNat(X))	→	a__isNat^#(X)	(72)
mark^#(U13(X))	→	mark^#(X)	(73)
mark^#(U21(X1,X2))	→	mark^#(X1)	(75)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(76)
mark^#(U22(X))	→	mark^#(X)	(77)
mark^#(U31(X1,X2))	→	mark^#(X1)	(79)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(80)
a__U31^#(tt,N)	→	mark^#(N)	(48)
mark^#(plus(X1,X2))	→	mark^#(X2)	(83)
mark^#(and(X1,X2))	→	mark^#(X1)	(86)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(87)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(88)

1.1.1.1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(a__isNatKind^#)	=	{ 1 }
π(a__and^#)	=	{ 2 }
π(mark^#)	=	{ 1 }
π(a__U31^#)	=	{ 2 }
π(a__U21^#)	=	{ 2 }
π(a__U12^#)	=	{ 2 }
π(a__isNat^#)	=	{ 1 }
π(a__U11^#)	=	{ 3 }
π(isNatKind)	=	{ 1 }

to remove the pairs:

a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(59)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(68)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(69)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(54)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(55)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(56)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(60)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(57)
mark^#(U12(X1,X2))	→	mark^#(X1)	(70)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(71)
mark^#(isNat(X))	→	a__isNat^#(X)	(72)
mark^#(U13(X))	→	mark^#(X)	(73)
mark^#(U21(X1,X2))	→	mark^#(X1)	(75)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(76)
mark^#(U22(X))	→	mark^#(X)	(77)
mark^#(U31(X1,X2))	→	mark^#(X1)	(79)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(80)
mark^#(plus(X1,X2))	→	mark^#(X2)	(83)
mark^#(and(X1,X2))	→	mark^#(X1)	(86)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(87)

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.