Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_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,V2)	→	a__U32(a__isNat(V2))	(4)
a__U32(tt)	→	tt	(5)
a__U41(tt,N)	→	mark(N)	(6)
a__U51(tt,M,N)	→	a__U52(a__isNat(N),M,N)	(7)
a__U52(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(8)
a__U61(tt)	→	0	(9)
a__U71(tt,M,N)	→	a__U72(a__isNat(N),M,N)	(10)
a__U72(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(11)
a__isNat(0)	→	tt	(12)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(13)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(14)
a__isNat(x(V1,V2))	→	a__U31(a__isNat(V1),V2)	(15)
a__plus(N,0)	→	a__U41(a__isNat(N),N)	(16)
a__plus(N,s(M))	→	a__U51(a__isNat(M),M,N)	(17)
a__x(N,0)	→	a__U61(a__isNat(N))	(18)
a__x(N,s(M))	→	a__U71(a__isNat(M),M,N)	(19)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(20)
mark(U12(X))	→	a__U12(mark(X))	(21)
mark(isNat(X))	→	a__isNat(X)	(22)
mark(U21(X))	→	a__U21(mark(X))	(23)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(24)
mark(U32(X))	→	a__U32(mark(X))	(25)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(26)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(27)
mark(U52(X1,X2,X3))	→	a__U52(mark(X1),X2,X3)	(28)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(29)
mark(U61(X))	→	a__U61(mark(X))	(30)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(31)
mark(U72(X1,X2,X3))	→	a__U72(mark(X1),X2,X3)	(32)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(33)
mark(tt)	→	tt	(34)
mark(s(X))	→	s(mark(X))	(35)
mark(0)	→	0	(36)
a__U11(X1,X2)	→	U11(X1,X2)	(37)
a__U12(X)	→	U12(X)	(38)
a__isNat(X)	→	isNat(X)	(39)
a__U21(X)	→	U21(X)	(40)
a__U31(X1,X2)	→	U31(X1,X2)	(41)
a__U32(X)	→	U32(X)	(42)
a__U41(X1,X2)	→	U41(X1,X2)	(43)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(44)
a__U52(X1,X2,X3)	→	U52(X1,X2,X3)	(45)
a__plus(X1,X2)	→	plus(X1,X2)	(46)
a__U61(X)	→	U61(X)	(47)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(48)
a__U72(X1,X2,X3)	→	U72(X1,X2,X3)	(49)
a__x(X1,X2)	→	x(X1,X2)	(50)

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.

a__U11^#(tt,V2)	→	a__U12^#(a__isNat(V2))	(51)
a__U11^#(tt,V2)	→	a__isNat^#(V2)	(52)
a__U31^#(tt,V2)	→	a__U32^#(a__isNat(V2))	(53)
a__U31^#(tt,V2)	→	a__isNat^#(V2)	(54)
a__U41^#(tt,N)	→	mark^#(N)	(55)
a__U51^#(tt,M,N)	→	a__U52^#(a__isNat(N),M,N)	(56)
a__U51^#(tt,M,N)	→	a__isNat^#(N)	(57)
a__U52^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(58)
a__U52^#(tt,M,N)	→	mark^#(N)	(59)
a__U52^#(tt,M,N)	→	mark^#(M)	(60)
a__U71^#(tt,M,N)	→	a__U72^#(a__isNat(N),M,N)	(61)
a__U71^#(tt,M,N)	→	a__isNat^#(N)	(62)
a__U72^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(63)
a__U72^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(64)
a__U72^#(tt,M,N)	→	mark^#(N)	(65)
a__U72^#(tt,M,N)	→	mark^#(M)	(66)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(67)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(68)
a__isNat^#(s(V1))	→	a__U21^#(a__isNat(V1))	(69)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(70)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__isNat(V1),V2)	(71)
a__isNat^#(x(V1,V2))	→	a__isNat^#(V1)	(72)
a__plus^#(N,0)	→	a__U41^#(a__isNat(N),N)	(73)
a__plus^#(N,0)	→	a__isNat^#(N)	(74)
a__plus^#(N,s(M))	→	a__U51^#(a__isNat(M),M,N)	(75)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(76)
a__x^#(N,0)	→	a__U61^#(a__isNat(N))	(77)
a__x^#(N,0)	→	a__isNat^#(N)	(78)
a__x^#(N,s(M))	→	a__U71^#(a__isNat(M),M,N)	(79)
a__x^#(N,s(M))	→	a__isNat^#(M)	(80)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(81)
mark^#(U11(X1,X2))	→	mark^#(X1)	(82)
mark^#(U12(X))	→	a__U12^#(mark(X))	(83)
mark^#(U12(X))	→	mark^#(X)	(84)
mark^#(isNat(X))	→	a__isNat^#(X)	(85)
mark^#(U21(X))	→	a__U21^#(mark(X))	(86)
mark^#(U21(X))	→	mark^#(X)	(87)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(88)
mark^#(U31(X1,X2))	→	mark^#(X1)	(89)
mark^#(U32(X))	→	a__U32^#(mark(X))	(90)
mark^#(U32(X))	→	mark^#(X)	(91)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(92)
mark^#(U41(X1,X2))	→	mark^#(X1)	(93)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(95)
mark^#(U52(X1,X2,X3))	→	a__U52^#(mark(X1),X2,X3)	(96)
mark^#(U52(X1,X2,X3))	→	mark^#(X1)	(97)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(98)
mark^#(plus(X1,X2))	→	mark^#(X1)	(99)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
mark^#(U61(X))	→	a__U61^#(mark(X))	(101)
mark^#(U61(X))	→	mark^#(X)	(102)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(103)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(104)
mark^#(U72(X1,X2,X3))	→	a__U72^#(mark(X1),X2,X3)	(105)
mark^#(U72(X1,X2,X3))	→	mark^#(X1)	(106)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(107)
mark^#(x(X1,X2))	→	mark^#(X1)	(108)
mark^#(x(X1,X2))	→	mark^#(X2)	(109)
mark^#(s(X))	→	mark^#(X)	(110)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(U11(X1,X2))	→	mark^#(X1)	(82)
mark^#(U12(X))	→	mark^#(X)	(84)
mark^#(U21(X))	→	mark^#(X)	(87)
mark^#(U31(X1,X2))	→	mark^#(X1)	(89)
mark^#(U32(X))	→	mark^#(X)	(91)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(92)
a__U41^#(tt,N)	→	mark^#(N)	(55)
mark^#(U41(X1,X2))	→	mark^#(X1)	(93)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
a__U51^#(tt,M,N)	→	a__U52^#(a__isNat(N),M,N)	(56)
a__U52^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(58)
a__plus^#(N,0)	→	a__U41^#(a__isNat(N),N)	(73)
a__plus^#(N,s(M))	→	a__U51^#(a__isNat(M),M,N)	(75)
a__U52^#(tt,M,N)	→	mark^#(N)	(59)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(95)
mark^#(U52(X1,X2,X3))	→	a__U52^#(mark(X1),X2,X3)	(96)
a__U52^#(tt,M,N)	→	mark^#(M)	(60)
mark^#(U52(X1,X2,X3))	→	mark^#(X1)	(97)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(98)
mark^#(plus(X1,X2))	→	mark^#(X1)	(99)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
mark^#(U61(X))	→	mark^#(X)	(102)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(103)
a__U71^#(tt,M,N)	→	a__U72^#(a__isNat(N),M,N)	(61)
a__U72^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(63)
a__U72^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(64)
a__x^#(N,s(M))	→	a__U71^#(a__isNat(M),M,N)	(79)
a__U72^#(tt,M,N)	→	mark^#(N)	(65)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(104)
mark^#(U72(X1,X2,X3))	→	a__U72^#(mark(X1),X2,X3)	(105)
a__U72^#(tt,M,N)	→	mark^#(M)	(66)
mark^#(U72(X1,X2,X3))	→	mark^#(X1)	(106)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(107)
mark^#(x(X1,X2))	→	mark^#(X1)	(108)
mark^#(x(X1,X2))	→	mark^#(X2)	(109)
mark^#(s(X))	→	mark^#(X)	(110)

1.1.1 Reduction Pair Processor

Using the

prec(mark^#)	=	1	stat(mark^#)	=	mul
prec(U41)	=	0	stat(U41)	=	mul
prec(a__U41^#)	=	1	stat(a__U41^#)	=	mul
prec(tt)	=	2	stat(tt)	=	mul
prec(U51)	=	3	stat(U51)	=	mul
prec(a__U51^#)	=	1	stat(a__U51^#)	=	mul
prec(a__U52^#)	=	1	stat(a__U52^#)	=	mul
prec(a__isNat)	=	2	stat(a__isNat)	=	mul
prec(a__plus^#)	=	1	stat(a__plus^#)	=	mul
prec(0)	=	1	stat(0)	=	mul
prec(s)	=	2	stat(s)	=	mul
prec(U52)	=	3	stat(U52)	=	mul
prec(plus)	=	3	stat(plus)	=	mul
prec(U71)	=	4	stat(U71)	=	lex
prec(a__U71^#)	=	4	stat(a__U71^#)	=	lex
prec(a__U72^#)	=	4	stat(a__U72^#)	=	lex
prec(a__x)	=	4	stat(a__x)	=	lex
prec(a__x^#)	=	4	stat(a__x^#)	=	lex
prec(U72)	=	4	stat(U72)	=	lex
prec(x)	=	4	stat(x)	=	lex
prec(isNat)	=	2	stat(isNat)	=	mul
prec(a__U41)	=	0	stat(a__U41)	=	mul
prec(a__plus)	=	3	stat(a__plus)	=	mul
prec(a__U71)	=	4	stat(a__U71)	=	lex
prec(a__U72)	=	4	stat(a__U72)	=	lex
prec(a__U51)	=	3	stat(a__U51)	=	mul
prec(a__U52)	=	3	stat(a__U52)	=	mul

π(mark^#)	=	[1]
π(U11)	=	1
π(U12)	=	1
π(U21)	=	1
π(U31)	=	1
π(U32)	=	1
π(U41)	=	[1,2]
π(a__U41^#)	=	[2]
π(mark)	=	1
π(tt)	=	[]
π(U51)	=	[1,2,3]
π(a__U51^#)	=	[1,2,3]
π(a__U52^#)	=	[1,2,3]
π(a__isNat)	=	[]
π(a__plus^#)	=	[1,2]
π(0)	=	[]
π(s)	=	[1]
π(U52)	=	[1,2,3]
π(plus)	=	[1,2]
π(U61)	=	1
π(U71)	=	[2,3,1]
π(a__U71^#)	=	[2,3,1]
π(a__U72^#)	=	[2,3,1]
π(a__x)	=	[2,1]
π(a__x^#)	=	[2,1]
π(U72)	=	[2,3,1]
π(x)	=	[2,1]
π(a__U11)	=	1
π(a__U12)	=	1
π(isNat)	=	[]
π(a__U21)	=	1
π(a__U31)	=	1
π(a__U32)	=	1
π(a__U41)	=	[1,2]
π(a__plus)	=	[1,2]
π(a__U71)	=	[2,3,1]
π(a__U72)	=	[2,3,1]
π(a__U51)	=	[1,2,3]
π(a__U52)	=	[1,2,3]
π(a__U61)	=	1

the pairs

mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(92)
mark^#(U41(X1,X2))	→	mark^#(X1)	(93)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
a__U52^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(58)
a__plus^#(N,0)	→	a__U41^#(a__isNat(N),N)	(73)
a__plus^#(N,s(M))	→	a__U51^#(a__isNat(M),M,N)	(75)
a__U52^#(tt,M,N)	→	mark^#(N)	(59)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(95)
mark^#(U52(X1,X2,X3))	→	a__U52^#(mark(X1),X2,X3)	(96)
a__U52^#(tt,M,N)	→	mark^#(M)	(60)
mark^#(U52(X1,X2,X3))	→	mark^#(X1)	(97)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(98)
mark^#(plus(X1,X2))	→	mark^#(X1)	(99)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(103)
a__U72^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(63)
a__U72^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(64)
a__x^#(N,s(M))	→	a__U71^#(a__isNat(M),M,N)	(79)
a__U72^#(tt,M,N)	→	mark^#(N)	(65)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(104)
mark^#(U72(X1,X2,X3))	→	a__U72^#(mark(X1),X2,X3)	(105)
a__U72^#(tt,M,N)	→	mark^#(M)	(66)
mark^#(U72(X1,X2,X3))	→	mark^#(X1)	(106)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(107)
mark^#(x(X1,X2))	→	mark^#(X1)	(108)
mark^#(x(X1,X2))	→	mark^#(X2)	(109)
mark^#(s(X))	→	mark^#(X)	(110)

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^#(U12(X))	→	mark^#(X)	(84)
mark^#(U11(X1,X2))	→	mark^#(X1)	(82)
mark^#(U21(X))	→	mark^#(X)	(87)
mark^#(U31(X1,X2))	→	mark^#(X1)	(89)
mark^#(U32(X))	→	mark^#(X)	(91)
mark^#(U61(X))	→	mark^#(X)	(102)

1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U12(x₁)]	=	1 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U21(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U32(x₁)]	=	1 · x₁
[U61(x₁)]	=	1 · x₁
[mark^#(x₁)]	=	1 · x₁

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

1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

mark^#(U12(X))	→	mark^#(X)	(84)

1	>	1
mark^#(U11(X1,X2))	→	mark^#(X1)	(82)

1	>	1
mark^#(U21(X))	→	mark^#(X)	(87)

1	>	1
mark^#(U31(X1,X2))	→	mark^#(X1)	(89)

1	>	1
mark^#(U32(X))	→	mark^#(X)	(91)

1	>	1
mark^#(U61(X))	→	mark^#(X)	(102)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 2^nd component contains the pair

a__U11^#(tt,V2)	→	a__isNat^#(V2)	(52)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(67)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(68)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(70)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__isNat(V1),V2)	(71)
a__U31^#(tt,V2)	→	a__isNat^#(V2)	(54)
a__isNat^#(x(V1,V2))	→	a__isNat^#(V1)	(72)

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[a__isNat(x₁)]	=	1 · x₁
[0]	=	0
[tt]	=	0
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[a__U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[s(x₁)]	=	1 · x₁
[a__U21(x₁)]	=	1 · x₁
[x(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[a__U31(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isNat(x₁)]	=	1 · x₁
[a__U32(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U32(x₁)]	=	1 · x₁
[U21(x₁)]	=	1 · x₁
[a__U12(x₁)]	=	1 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U12(x₁)]	=	1 · x₁
[a__isNat^#(x₁)]	=	1 · x₁
[a__U11^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[a__U31^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

a__isNat(0)	→	tt	(12)
a__isNat(plus(V1,V2))	→	a__U11(a__isNat(V1),V2)	(13)
a__isNat(s(V1))	→	a__U21(a__isNat(V1))	(14)
a__isNat(x(V1,V2))	→	a__U31(a__isNat(V1),V2)	(15)
a__isNat(X)	→	isNat(X)	(39)
a__U31(tt,V2)	→	a__U32(a__isNat(V2))	(4)
a__U31(X1,X2)	→	U31(X1,X2)	(41)
a__U32(tt)	→	tt	(5)
a__U32(X)	→	U32(X)	(42)
a__U21(tt)	→	tt	(3)
a__U21(X)	→	U21(X)	(40)
a__U11(tt,V2)	→	a__U12(a__isNat(V2))	(1)
a__U11(X1,X2)	→	U11(X1,X2)	(37)
a__U12(tt)	→	tt	(2)
a__U12(X)	→	U12(X)	(38)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.2.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNat(V1),V2)	(67)

1	>	2
a__isNat^#(x(V1,V2))	→	a__U31^#(a__isNat(V1),V2)	(71)

1	>	2
a__U11^#(tt,V2)	→	a__isNat^#(V2)	(52)

2	≥	1
a__U31^#(tt,V2)	→	a__isNat^#(V2)	(54)

2	≥	1
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(68)

1	>	1
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(70)

1	>	1
a__isNat^#(x(V1,V2))	→	a__isNat^#(V1)	(72)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.