Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds-noand_FR)

The rewrite relation of the following TRS is considered.

U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U12(tt)	→	tt	(2)
U21(tt)	→	tt	(3)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
U32(tt)	→	tt	(5)
U41(tt,N)	→	activate(N)	(6)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U61(tt)	→	0	(9)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
isNat(n__0)	→	tt	(12)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
x(N,0)	→	U61(isNat(N))	(18)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
0	→	n__0	(20)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
s(X)	→	n__s(X)	(22)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(25)
activate(n__s(X))	→	s(activate(X))	(26)
activate(n__x(X1,X2))	→	x(activate(X1),activate(X2))	(27)
activate(X)	→	X	(28)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

U11^#(tt,V2)	→	U12^#(isNat(activate(V2)))	(29)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(30)
U11^#(tt,V2)	→	activate^#(V2)	(31)
U31^#(tt,V2)	→	U32^#(isNat(activate(V2)))	(32)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(33)
U31^#(tt,V2)	→	activate^#(V2)	(34)
U41^#(tt,N)	→	activate^#(N)	(35)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(36)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(37)
U51^#(tt,M,N)	→	activate^#(N)	(38)
U51^#(tt,M,N)	→	activate^#(M)	(39)
U52^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(40)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(41)
U52^#(tt,M,N)	→	activate^#(N)	(42)
U52^#(tt,M,N)	→	activate^#(M)	(43)
U61^#(tt)	→	0^#	(44)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(45)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(46)
U71^#(tt,M,N)	→	activate^#(N)	(47)
U71^#(tt,M,N)	→	activate^#(M)	(48)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(49)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(50)
U72^#(tt,M,N)	→	activate^#(N)	(51)
U72^#(tt,M,N)	→	activate^#(M)	(52)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(53)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(55)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(56)
isNat^#(n__s(V1))	→	U21^#(isNat(activate(V1)))	(57)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(58)
isNat^#(n__s(V1))	→	activate^#(V1)	(59)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(60)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(61)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(63)
plus^#(N,0)	→	U41^#(isNat(N),N)	(64)
plus^#(N,0)	→	isNat^#(N)	(65)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(66)
plus^#(N,s(M))	→	isNat^#(M)	(67)
x^#(N,0)	→	U61^#(isNat(N))	(68)
x^#(N,0)	→	isNat^#(N)	(69)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(70)
x^#(N,s(M))	→	isNat^#(M)	(71)
activate^#(n__0)	→	0^#	(72)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(73)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(74)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(75)
activate^#(n__s(X))	→	s^#(activate(X))	(76)
activate^#(n__s(X))	→	activate^#(X)	(77)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(78)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(79)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(80)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U11^#(tt,V2)	→	isNat^#(activate(V2))	(30)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(53)
U11^#(tt,V2)	→	activate^#(V2)	(31)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(73)
plus^#(N,0)	→	U41^#(isNat(N),N)	(64)
U41^#(tt,N)	→	activate^#(N)	(35)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(74)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(75)
activate^#(n__s(X))	→	activate^#(X)	(77)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(78)
x^#(N,0)	→	isNat^#(N)	(69)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(55)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(79)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(80)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(56)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(58)
isNat^#(n__s(V1))	→	activate^#(V1)	(59)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(60)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(33)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(61)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(63)
U31^#(tt,V2)	→	activate^#(V2)	(34)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(70)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(45)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(49)
plus^#(N,0)	→	isNat^#(N)	(65)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(66)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(36)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(41)
plus^#(N,s(M))	→	isNat^#(M)	(67)
U52^#(tt,M,N)	→	activate^#(N)	(42)
U52^#(tt,M,N)	→	activate^#(M)	(43)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(37)
U51^#(tt,M,N)	→	activate^#(N)	(38)
U51^#(tt,M,N)	→	activate^#(M)	(39)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(50)
x^#(N,s(M))	→	isNat^#(M)	(71)
U72^#(tt,M,N)	→	activate^#(N)	(51)
U72^#(tt,M,N)	→	activate^#(M)	(52)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(46)
U71^#(tt,M,N)	→	activate^#(N)	(47)
U71^#(tt,M,N)	→	activate^#(M)	(48)

1.1.1 Reduction Pair Processor

Using the

prec(U11^#)	=	1	stat(U11^#)	=	mul
prec(tt)	=	3	stat(tt)	=	mul
prec(isNat^#)	=	0	stat(isNat^#)	=	mul
prec(n__plus)	=	5	stat(n__plus)	=	mul
prec(isNat)	=	3	stat(isNat)	=	mul
prec(plus^#)	=	2	stat(plus^#)	=	mul
prec(0)	=	6	stat(0)	=	mul
prec(n__s)	=	4	stat(n__s)	=	mul
prec(n__x)	=	9	stat(n__x)	=	mul
prec(x^#)	=	9	stat(x^#)	=	mul
prec(U31^#)	=	7	stat(U31^#)	=	mul
prec(s)	=	4	stat(s)	=	mul
prec(U71^#)	=	9	stat(U71^#)	=	mul
prec(U72^#)	=	9	stat(U72^#)	=	mul
prec(x)	=	9	stat(x)	=	mul
prec(U51^#)	=	2	stat(U51^#)	=	mul
prec(U52^#)	=	2	stat(U52^#)	=	mul
prec(n__0)	=	6	stat(n__0)	=	mul
prec(plus)	=	5	stat(plus)	=	mul
prec(U71)	=	9	stat(U71)	=	mul
prec(U72)	=	9	stat(U72)	=	mul
prec(U61)	=	8	stat(U61)	=	mul
prec(U51)	=	5	stat(U51)	=	mul
prec(U32)	=	3	stat(U32)	=	mul
prec(U52)	=	5	stat(U52)	=	mul

π(U11^#)	=	[2]
π(tt)	=	[]
π(isNat^#)	=	[1]
π(activate)	=	1
π(n__plus)	=	[1,2]
π(isNat)	=	[]
π(activate^#)	=	1
π(plus^#)	=	[1,2]
π(0)	=	[]
π(U41^#)	=	2
π(n__s)	=	[1]
π(n__x)	=	[1,2]
π(x^#)	=	[1,2]
π(U31^#)	=	[1,2]
π(s)	=	[1]
π(U71^#)	=	[1,2,3]
π(U72^#)	=	[1,2,3]
π(x)	=	[1,2]
π(U51^#)	=	[1,2,3]
π(U52^#)	=	[2,3]
π(n__0)	=	[]
π(plus)	=	[1,2]
π(U41)	=	2
π(U71)	=	[1,2,3]
π(U72)	=	[1,2,3]
π(U11)	=	1
π(U21)	=	1
π(U31)	=	1
π(U61)	=	[1]
π(U51)	=	[1,2,3]
π(U32)	=	[]
π(U12)	=	1
π(U52)	=	[1,2,3]

the pairs

U11^#(tt,V2)	→	isNat^#(activate(V2))	(30)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(53)
U11^#(tt,V2)	→	activate^#(V2)	(31)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(73)
plus^#(N,0)	→	U41^#(isNat(N),N)	(64)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(74)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(75)
activate^#(n__s(X))	→	activate^#(X)	(77)
x^#(N,0)	→	isNat^#(N)	(69)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(55)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(79)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(80)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(56)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(58)
isNat^#(n__s(V1))	→	activate^#(V1)	(59)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(60)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(33)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(61)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(63)
U31^#(tt,V2)	→	activate^#(V2)	(34)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(70)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(49)
plus^#(N,0)	→	isNat^#(N)	(65)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(66)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(36)
plus^#(N,s(M))	→	isNat^#(M)	(67)
U52^#(tt,M,N)	→	activate^#(N)	(42)
U52^#(tt,M,N)	→	activate^#(M)	(43)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(37)
U51^#(tt,M,N)	→	activate^#(N)	(38)
U51^#(tt,M,N)	→	activate^#(M)	(39)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(50)
x^#(N,s(M))	→	isNat^#(M)	(71)
U72^#(tt,M,N)	→	activate^#(N)	(51)
U72^#(tt,M,N)	→	activate^#(M)	(52)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(46)
U71^#(tt,M,N)	→	activate^#(N)	(47)
U71^#(tt,M,N)	→	activate^#(M)	(48)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.