Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_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,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__U33(tt)	→	tt	(8)
a__U41(tt,N)	→	mark(N)	(9)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
a__U61(tt)	→	0	(11)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
a__and(tt,X)	→	mark(X)	(13)
a__isNat(0)	→	tt	(14)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__isNatKind(0)	→	tt	(18)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
mark(U22(X))	→	a__U22(mark(X))	(31)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
mark(U33(X))	→	a__U33(mark(X))	(34)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(U61(X))	→	a__U61(mark(X))	(38)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
mark(tt)	→	tt	(43)
mark(s(X))	→	s(mark(X))	(44)
mark(0)	→	0	(45)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
a__isNat(X)	→	isNat(X)	(48)
a__U13(X)	→	U13(X)	(49)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U22(X)	→	U22(X)	(51)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U33(X)	→	U33(X)	(54)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(X)	→	U61(X)	(58)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__x(X1,X2)	→	x(X1,X2)	(60)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__isNatKind(X)	→	isNatKind(X)	(62)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(a__U11)	=	0	stat(a__U11)	=	mul
prec(tt)	=	4	stat(tt)	=	mul
prec(a__U12)	=	0	stat(a__U12)	=	mul
prec(a__U21)	=	5	stat(a__U21)	=	mul
prec(a__U22)	=	1	stat(a__U22)	=	mul
prec(a__U31)	=	6	stat(a__U31)	=	mul
prec(a__U32)	=	2	stat(a__U32)	=	mul
prec(a__U41)	=	3	stat(a__U41)	=	mul
prec(a__U51)	=	8	stat(a__U51)	=	lex
prec(s)	=	7	stat(s)	=	mul
prec(a__plus)	=	8	stat(a__plus)	=	lex
prec(0)	=	4	stat(0)	=	mul
prec(a__U71)	=	9	stat(a__U71)	=	lex
prec(a__x)	=	9	stat(a__x)	=	lex
prec(a__and)	=	7	stat(a__and)	=	mul
prec(plus)	=	8	stat(plus)	=	lex
prec(x)	=	9	stat(x)	=	lex
prec(and)	=	7	stat(and)	=	mul
prec(U11)	=	0	stat(U11)	=	mul
prec(U12)	=	0	stat(U12)	=	mul
prec(U21)	=	5	stat(U21)	=	mul
prec(U22)	=	1	stat(U22)	=	mul
prec(U31)	=	6	stat(U31)	=	mul
prec(U32)	=	2	stat(U32)	=	mul
prec(U41)	=	3	stat(U41)	=	mul
prec(U51)	=	8	stat(U51)	=	lex
prec(U71)	=	9	stat(U71)	=	lex

π(a__U11)	=	[1,2,3]
π(tt)	=	[]
π(a__U12)	=	[1,2]
π(a__isNat)	=	1
π(a__U13)	=	1
π(a__U21)	=	[1,2]
π(a__U22)	=	[1]
π(a__U31)	=	[1,2,3]
π(a__U32)	=	[1,2]
π(a__U33)	=	1
π(a__U41)	=	[1,2]
π(mark)	=	1
π(a__U51)	=	[3,2,1]
π(s)	=	[1]
π(a__plus)	=	[1,2]
π(a__U61)	=	1
π(0)	=	[]
π(a__U71)	=	[2,3,1]
π(a__x)	=	[2,1]
π(a__and)	=	[1,2]
π(plus)	=	[1,2]
π(a__isNatKind)	=	1
π(isNatKind)	=	1
π(x)	=	[2,1]
π(and)	=	[1,2]
π(isNat)	=	1
π(U11)	=	[1,2,3]
π(U12)	=	[1,2]
π(U13)	=	1
π(U21)	=	[1,2]
π(U22)	=	[1]
π(U31)	=	[1,2,3]
π(U32)	=	[1,2]
π(U33)	=	1
π(U41)	=	[1,2]
π(U51)	=	[3,2,1]
π(U61)	=	1
π(U71)	=	[2,3,1]

all of the following rules can be deleted.

a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__U41(tt,N)	→	mark(N)	(9)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
a__and(tt,X)	→	mark(X)	(13)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)

1.1 Rule Removal

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

prec(tt)	=	13	weight(tt)	=	2
prec(0)	=	32	weight(0)	=	1
prec(a__U13)	=	12	weight(a__U13)	=	1
prec(a__U33)	=	35	weight(a__U33)	=	1
prec(a__U61)	=	33	weight(a__U61)	=	1
prec(a__isNat)	=	21	weight(a__isNat)	=	1
prec(a__isNatKind)	=	14	weight(a__isNatKind)	=	1
prec(mark)	=	37	weight(mark)	=	0
prec(isNat)	=	18	weight(isNat)	=	1
prec(U13)	=	11	weight(U13)	=	1
prec(U22)	=	1	weight(U22)	=	1
prec(a__U22)	=	27	weight(a__U22)	=	1
prec(U33)	=	28	weight(U33)	=	1
prec(U61)	=	30	weight(U61)	=	1
prec(isNatKind)	=	10	weight(isNatKind)	=	1
prec(s)	=	34	weight(s)	=	1
prec(U11)	=	0	weight(U11)	=	0
prec(a__U11)	=	36	weight(a__U11)	=	0
prec(U12)	=	19	weight(U12)	=	0
prec(a__U12)	=	24	weight(a__U12)	=	0
prec(U21)	=	25	weight(U21)	=	0
prec(a__U21)	=	26	weight(a__U21)	=	0
prec(U31)	=	2	weight(U31)	=	0
prec(a__U31)	=	3	weight(a__U31)	=	0
prec(U32)	=	15	weight(U32)	=	0
prec(a__U32)	=	16	weight(a__U32)	=	0
prec(U41)	=	4	weight(U41)	=	0
prec(a__U41)	=	5	weight(a__U41)	=	0
prec(U51)	=	6	weight(U51)	=	0
prec(a__U51)	=	29	weight(a__U51)	=	0
prec(plus)	=	17	weight(plus)	=	0
prec(a__plus)	=	20	weight(a__plus)	=	0
prec(U71)	=	7	weight(U71)	=	0
prec(a__U71)	=	8	weight(a__U71)	=	0
prec(x)	=	22	weight(x)	=	0
prec(a__x)	=	23	weight(a__x)	=	0
prec(and)	=	9	weight(and)	=	0
prec(a__and)	=	31	weight(a__and)	=	0

all of the following rules can be deleted.

a__U13(tt)	→	tt	(3)
a__U33(tt)	→	tt	(8)
a__U61(tt)	→	0	(11)
a__isNat(0)	→	tt	(14)
a__isNatKind(0)	→	tt	(18)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
mark(U22(X))	→	a__U22(mark(X))	(31)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
mark(U33(X))	→	a__U33(mark(X))	(34)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(U61(X))	→	a__U61(mark(X))	(38)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
mark(tt)	→	tt	(43)
mark(s(X))	→	s(mark(X))	(44)
mark(0)	→	0	(45)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
a__isNat(X)	→	isNat(X)	(48)
a__U13(X)	→	U13(X)	(49)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U22(X)	→	U22(X)	(51)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U33(X)	→	U33(X)	(54)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(X)	→	U61(X)	(58)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__x(X1,X2)	→	x(X1,X2)	(60)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__isNatKind(X)	→	isNatKind(X)	(62)

1.1.1 R is empty

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