Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete-noand_FR)

The rewrite relation of the following TRS is considered.

U11(tt,V1,V2)	→	U12(isNatKind(activate(V1)),activate(V1),activate(V2))	(1)
U12(tt,V1,V2)	→	U13(isNatKind(activate(V2)),activate(V1),activate(V2))	(2)
U13(tt,V1,V2)	→	U14(isNatKind(activate(V2)),activate(V1),activate(V2))	(3)
U14(tt,V1,V2)	→	U15(isNat(activate(V1)),activate(V2))	(4)
U15(tt,V2)	→	U16(isNat(activate(V2)))	(5)
U16(tt)	→	tt	(6)
U21(tt,V1)	→	U22(isNatKind(activate(V1)),activate(V1))	(7)
U22(tt,V1)	→	U23(isNat(activate(V1)))	(8)
U23(tt)	→	tt	(9)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
U32(tt)	→	tt	(11)
U41(tt)	→	tt	(12)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
U52(tt,N)	→	activate(N)	(14)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
isNat(n__0)	→	tt	(19)
isNat(n__plus(V1,V2))	→	U11(isNatKind(activate(V1)),activate(V1),activate(V2))	(20)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(21)
isNatKind(n__0)	→	tt	(22)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
plus(N,0)	→	U51(isNat(N),N)	(25)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
0	→	n__0	(27)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
s(X)	→	n__s(X)	(29)
activate(n__0)	→	0	(30)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(31)
activate(n__s(X))	→	s(activate(X))	(32)
activate(X)	→	X	(33)

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.

U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(36)
U31^#(tt,V2)	→	activate^#(V2)	(37)
U11^#(tt,V1,V2)	→	activate^#(V2)	(38)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(39)
U63^#(tt,M,N)	→	activate^#(M)	(40)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(41)
U61^#(tt,M,N)	→	activate^#(M)	(42)
plus^#(N,s(M))	→	isNat^#(M)	(43)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(44)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(45)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(46)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(47)
U61^#(tt,M,N)	→	activate^#(N)	(48)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(49)
U13^#(tt,V1,V2)	→	activate^#(V2)	(50)
U15^#(tt,V2)	→	activate^#(V2)	(51)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
U13^#(tt,V1,V2)	→	activate^#(V2)	(50)
U62^#(tt,M,N)	→	activate^#(M)	(53)
U22^#(tt,V1)	→	U23^#(isNat(activate(V1)))	(54)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(55)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(60)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(61)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(62)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(63)
plus^#(N,0)	→	isNat^#(N)	(64)
U64^#(tt,M,N)	→	activate^#(N)	(65)
U14^#(tt,V1,V2)	→	activate^#(V2)	(66)
activate^#(n__s(X))	→	activate^#(X)	(67)
U22^#(tt,V1)	→	activate^#(V1)	(68)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(69)
U21^#(tt,V1)	→	activate^#(V1)	(70)
U64^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(71)
U62^#(tt,M,N)	→	activate^#(N)	(72)
U64^#(tt,M,N)	→	activate^#(M)	(73)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(74)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(75)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(76)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(77)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(78)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(79)
U52^#(tt,N)	→	activate^#(N)	(80)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(81)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(82)
isNatKind^#(n__s(V1))	→	U41^#(isNatKind(activate(V1)))	(83)
U11^#(tt,V1,V2)	→	activate^#(V1)	(84)
U31^#(tt,V2)	→	U32^#(isNatKind(activate(V2)))	(85)
U61^#(tt,M,N)	→	activate^#(M)	(42)
U12^#(tt,V1,V2)	→	activate^#(V2)	(86)
activate^#(n__s(X))	→	s^#(activate(X))	(87)
U11^#(tt,V1,V2)	→	activate^#(V1)	(84)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(88)
plus^#(N,0)	→	U51^#(isNat(N),N)	(89)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(90)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(91)
U13^#(tt,V1,V2)	→	activate^#(V1)	(92)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(93)
U21^#(tt,V1)	→	activate^#(V1)	(70)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(94)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(95)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(91)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(96)
U15^#(tt,V2)	→	U16^#(isNat(activate(V2)))	(97)
activate^#(n__0)	→	0^#	(98)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(99)
U12^#(tt,V1,V2)	→	activate^#(V2)	(86)
U14^#(tt,V1,V2)	→	activate^#(V1)	(100)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(101)
U62^#(tt,M,N)	→	activate^#(N)	(72)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(102)
U12^#(tt,V1,V2)	→	activate^#(V1)	(103)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(104)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(105)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

activate^#(n__plus(X1,X2))	→	activate^#(X1)	(105)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(104)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(79)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(77)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(78)
U12^#(tt,V1,V2)	→	activate^#(V1)	(103)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(75)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(76)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(74)
U64^#(tt,M,N)	→	activate^#(M)	(73)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(102)
U62^#(tt,M,N)	→	activate^#(N)	(72)
U21^#(tt,V1)	→	activate^#(V1)	(70)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(69)
U22^#(tt,V1)	→	activate^#(V1)	(68)
U51^#(tt,N)	→	activate^#(N)	(58)
activate^#(n__s(X))	→	activate^#(X)	(67)
U62^#(tt,M,N)	→	activate^#(N)	(72)
U14^#(tt,V1,V2)	→	activate^#(V2)	(66)
U64^#(tt,M,N)	→	activate^#(N)	(65)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(101)
plus^#(N,0)	→	isNat^#(N)	(64)
U14^#(tt,V1,V2)	→	activate^#(V1)	(100)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(63)
U12^#(tt,V1,V2)	→	activate^#(V2)	(86)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(62)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(99)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(61)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(60)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(96)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(91)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(95)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
U21^#(tt,V1)	→	activate^#(V1)	(70)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(94)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(93)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(55)
U62^#(tt,M,N)	→	activate^#(M)	(53)
U13^#(tt,V1,V2)	→	activate^#(V1)	(92)
U13^#(tt,V1,V2)	→	activate^#(V2)	(50)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(91)
U13^#(tt,V1,V2)	→	activate^#(V2)	(50)
U15^#(tt,V2)	→	activate^#(V2)	(51)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(49)
U61^#(tt,M,N)	→	activate^#(N)	(48)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(90)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(47)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(46)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(45)
plus^#(N,0)	→	U51^#(isNat(N),N)	(89)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(44)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(88)
U11^#(tt,V1,V2)	→	activate^#(V1)	(84)
U61^#(tt,M,N)	→	activate^#(M)	(42)
plus^#(N,s(M))	→	isNat^#(M)	(43)
U12^#(tt,V1,V2)	→	activate^#(V2)	(86)
U61^#(tt,M,N)	→	activate^#(M)	(42)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(41)
U11^#(tt,V1,V2)	→	activate^#(V1)	(84)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U63^#(tt,M,N)	→	activate^#(M)	(40)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(39)
U11^#(tt,V1,V2)	→	activate^#(V2)	(38)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(82)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(81)
U31^#(tt,V2)	→	activate^#(V2)	(37)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(36)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
U52^#(tt,N)	→	activate^#(N)	(80)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁)]	=	0
[isNatKind(x₁)]	=	x₁ + 2
[U16(x₁)]	=	3
[U21(x₁, x₂)]	=	x₁ + 26819
[U11(x₁, x₂, x₃)]	=	x₁ + 3
[U64(x₁, x₂, x₃)]	=	x₂ + x₃ + 26822
[s(x₁)]	=	x₁ + 26819
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 5
[activate^#(x₁)]	=	x₁ + 3
[U23^#(x₁)]	=	0
[U23(x₁)]	=	3
[U63(x₁, x₂, x₃)]	=	x₂ + x₃ + 26822
[U13^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[U52^#(x₁, x₂)]	=	x₂ + 4
[U12(x₁, x₂, x₃)]	=	x₁ + 6
[U16^#(x₁)]	=	0
[n__s(x₁)]	=	x₁ + 26819
[U12^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[U62^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 26822
[0]	=	2
[U14^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[s^#(x₁)]	=	0
[U62(x₁, x₂, x₃)]	=	x₂ + x₃ + 26822
[n__plus(x₁, x₂)]	=	x₁ + x₂ + 3
[U63^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 26821
[U15^#(x₁, x₂)]	=	x₂ + 3
[U32(x₁)]	=	4
[n__0]	=	2
[U14(x₁, x₂, x₃)]	=	0
[isNat(x₁)]	=	x₁ + 1
[U52(x₁, x₂)]	=	x₂ + 0
[U15(x₁, x₂)]	=	2
[U61(x₁, x₂, x₃)]	=	x₂ + x₃ + 26822
[plus(x₁, x₂)]	=	x₁ + x₂ + 3
[U51^#(x₁, x₂)]	=	x₂ + 6
[U11^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[U64^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 6
[U31(x₁, x₂)]	=	x₁ + 3
[U41^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	x₂ + 3
[U22^#(x₁, x₂)]	=	x₂ + 3
[tt]	=	4
[U13(x₁, x₂, x₃)]	=	x₁ + 9
[U22(x₁, x₂)]	=	x₁ + 26822
[U51(x₁, x₂)]	=	x₂ + 5
[isNatKind^#(x₁)]	=	x₁ + 0
[U41(x₁)]	=	x₁ + 0
[U31^#(x₁, x₂)]	=	x₁ + x₂ + 0
[U61^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 26823

together with the usable rules

U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
activate(n__s(X))	→	s(activate(X))	(32)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
0	→	n__0	(27)
isNatKind(n__0)	→	tt	(22)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
activate(X)	→	X	(33)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
plus(N,0)	→	U51(isNat(N),N)	(25)
activate(n__0)	→	0	(30)
U52(tt,N)	→	activate(N)	(14)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(31)
U41(tt)	→	tt	(12)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
U32(tt)	→	tt	(11)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
s(X)	→	n__s(X)	(29)

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

activate^#(n__plus(X1,X2))	→	activate^#(X1)	(105)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(104)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(79)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(77)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(78)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(76)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(74)
U64^#(tt,M,N)	→	activate^#(M)	(73)
U62^#(tt,M,N)	→	activate^#(N)	(72)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(69)
U51^#(tt,N)	→	activate^#(N)	(58)
activate^#(n__s(X))	→	activate^#(X)	(67)
U62^#(tt,M,N)	→	activate^#(N)	(72)
U64^#(tt,M,N)	→	activate^#(N)	(65)
plus^#(N,0)	→	isNat^#(N)	(64)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(63)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(61)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(96)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(95)
isNat^#(n__s(V1))	→	activate^#(V1)	(56)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(94)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(93)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(55)
U62^#(tt,M,N)	→	activate^#(M)	(53)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(49)
U61^#(tt,M,N)	→	activate^#(N)	(48)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(90)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(46)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(45)
plus^#(N,0)	→	U51^#(isNat(N),N)	(89)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(44)
U61^#(tt,M,N)	→	activate^#(M)	(42)
plus^#(N,s(M))	→	isNat^#(M)	(43)
U61^#(tt,M,N)	→	activate^#(M)	(42)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(41)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U63^#(tt,M,N)	→	activate^#(M)	(40)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(39)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(82)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(81)
U31^#(tt,V2)	→	activate^#(V2)	(37)
U63^#(tt,M,N)	→	activate^#(N)	(35)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
U52^#(tt,N)	→	activate^#(N)	(80)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.