Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_iGM)

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)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(14)
mark(tt)	→	active(tt)	(15)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(16)
mark(s(X))	→	active(s(mark(X)))	(17)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(18)
mark(U31(X))	→	active(U31(mark(X)))	(19)
mark(0)	→	active(0)	(20)
mark(U41(X1,X2,X3))	→	active(U41(mark(X1),X2,X3))	(21)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(22)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(23)
mark(isNat(X))	→	active(isNat(X))	(24)
U11(mark(X1),X2)	→	U11(X1,X2)	(25)
U11(X1,mark(X2))	→	U11(X1,X2)	(26)
U11(active(X1),X2)	→	U11(X1,X2)	(27)
U11(X1,active(X2))	→	U11(X1,X2)	(28)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(29)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(30)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(31)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(32)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(33)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(34)
s(mark(X))	→	s(X)	(35)
s(active(X))	→	s(X)	(36)
plus(mark(X1),X2)	→	plus(X1,X2)	(37)
plus(X1,mark(X2))	→	plus(X1,X2)	(38)
plus(active(X1),X2)	→	plus(X1,X2)	(39)
plus(X1,active(X2))	→	plus(X1,X2)	(40)
U31(mark(X))	→	U31(X)	(41)
U31(active(X))	→	U31(X)	(42)
U41(mark(X1),X2,X3)	→	U41(X1,X2,X3)	(43)
U41(X1,mark(X2),X3)	→	U41(X1,X2,X3)	(44)
U41(X1,X2,mark(X3))	→	U41(X1,X2,X3)	(45)
U41(active(X1),X2,X3)	→	U41(X1,X2,X3)	(46)
U41(X1,active(X2),X3)	→	U41(X1,X2,X3)	(47)
U41(X1,X2,active(X3))	→	U41(X1,X2,X3)	(48)
x(mark(X1),X2)	→	x(X1,X2)	(49)
x(X1,mark(X2))	→	x(X1,X2)	(50)
x(active(X1),X2)	→	x(X1,X2)	(51)
x(X1,active(X2))	→	x(X1,X2)	(52)
and(mark(X1),X2)	→	and(X1,X2)	(53)
and(X1,mark(X2))	→	and(X1,X2)	(54)
and(active(X1),X2)	→	and(X1,X2)	(55)
and(X1,active(X2))	→	and(X1,X2)	(56)
isNat(mark(X))	→	isNat(X)	(57)
isNat(active(X))	→	isNat(X)	(58)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(U11)	=	0	stat(U11)	=	mul
prec(tt)	=	1	stat(tt)	=	mul
prec(U21)	=	4	stat(U21)	=	lex
prec(s)	=	3	stat(s)	=	mul
prec(plus)	=	4	stat(plus)	=	lex
prec(U31)	=	6	stat(U31)	=	mul
prec(0)	=	5	stat(0)	=	mul
prec(U41)	=	7	stat(U41)	=	lex
prec(x)	=	7	stat(x)	=	lex
prec(and)	=	2	stat(and)	=	mul

π(active)	=	1
π(U11)	=	[1,2]
π(tt)	=	[]
π(mark)	=	1
π(U21)	=	[3,2,1]
π(s)	=	[1]
π(plus)	=	[1,2]
π(U31)	=	[1]
π(0)	=	[]
π(U41)	=	[2,3,1]
π(x)	=	[2,1]
π(and)	=	[1,2]
π(isNat)	=	1

all of the following rules can be deleted.

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)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	1 + 2 · x₁
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[active(x₁)]	=	1 · x₁
[tt]	=	2
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[s(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[U31(x₁)]	=	1 · x₁
[0]	=	1
[U41(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 2 · x₃
[x(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isNat(x₁)]	=	2 + 1 · x₁

all of the following rules can be deleted.

mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(14)
mark(tt)	→	active(tt)	(15)
mark(0)	→	active(0)	(20)
mark(U41(X1,X2,X3))	→	active(U41(mark(X1),X2,X3))	(21)
mark(isNat(X))	→	active(isNat(X))	(24)
U11(mark(X1),X2)	→	U11(X1,X2)	(25)
U11(X1,mark(X2))	→	U11(X1,X2)	(26)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(29)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(30)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(31)
s(mark(X))	→	s(X)	(35)
plus(mark(X1),X2)	→	plus(X1,X2)	(37)
plus(X1,mark(X2))	→	plus(X1,X2)	(38)
U31(mark(X))	→	U31(X)	(41)
U41(mark(X1),X2,X3)	→	U41(X1,X2,X3)	(43)
U41(X1,mark(X2),X3)	→	U41(X1,X2,X3)	(44)
U41(X1,X2,mark(X3))	→	U41(X1,X2,X3)	(45)
x(mark(X1),X2)	→	x(X1,X2)	(49)
x(X1,mark(X2))	→	x(X1,X2)	(50)
and(mark(X1),X2)	→	and(X1,X2)	(53)
and(X1,mark(X2))	→	and(X1,X2)	(54)
isNat(mark(X))	→	isNat(X)	(57)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	2 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 1 · x₃
[active(x₁)]	=	1 · x₁
[s(x₁)]	=	2 + 1 · x₁
[plus(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U31(x₁)]	=	1 · x₁
[x(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[isNat(x₁)]	=	2 · x₁

all of the following rules can be deleted.

mark(s(X))	→	active(s(mark(X)))	(17)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(23)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	1 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[active(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U31(x₁)]	=	1 + 1 · x₁
[x(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[s(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isNat(x₁)]	=	2 · x₁

all of the following rules can be deleted.

mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(16)
mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(18)
mark(U31(X))	→	active(U31(mark(X)))	(19)
mark(x(X1,X2))	→	active(x(mark(X1),mark(X2)))	(22)

1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(active)	=	9	weight(active)	=	0
prec(s)	=	2	weight(s)	=	1
prec(U31)	=	4	weight(U31)	=	1
prec(isNat)	=	8	weight(isNat)	=	1
prec(U11)	=	0	weight(U11)	=	0
prec(U21)	=	1	weight(U21)	=	0
prec(plus)	=	3	weight(plus)	=	0
prec(U41)	=	5	weight(U41)	=	0
prec(x)	=	6	weight(x)	=	0
prec(and)	=	7	weight(and)	=	0

all of the following rules can be deleted.

U11(active(X1),X2)	→	U11(X1,X2)	(27)
U11(X1,active(X2))	→	U11(X1,X2)	(28)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(32)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(33)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(34)
s(active(X))	→	s(X)	(36)
plus(active(X1),X2)	→	plus(X1,X2)	(39)
plus(X1,active(X2))	→	plus(X1,X2)	(40)
U31(active(X))	→	U31(X)	(42)
U41(active(X1),X2,X3)	→	U41(X1,X2,X3)	(46)
U41(X1,active(X2),X3)	→	U41(X1,X2,X3)	(47)
U41(X1,X2,active(X3))	→	U41(X1,X2,X3)	(48)
x(active(X1),X2)	→	x(X1,X2)	(51)
x(X1,active(X2))	→	x(X1,X2)	(52)
and(active(X1),X2)	→	and(X1,X2)	(55)
and(X1,active(X2))	→	and(X1,X2)	(56)
isNat(active(X))	→	isNat(X)	(58)

1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.