Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_Z)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  plus#(N,s(M))	→	U21#(and(isNat(M),n__isNat(N)),M,N)	(38)
  U21#(tt,M,N)	→	activate#(M)	(37)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(24)
  isNat#(n__plus(V1,V2))	→	isNat#(activate(V1))	(23)
  activate#(n__plus(X1,X2))	→	plus#(X1,X2)	(35)
  U21#(tt,M,N)	→	activate#(N)	(33)
  and#(tt,X)	→	activate#(X)	(32)
  activate#(n__isNat(X))	→	isNat#(X)	(31)
  isNat#(n__plus(V1,V2))	→	and#(isNat(activate(V1)),n__isNat(activate(V2)))	(22)
  plus#(N,0)	→	U11#(isNat(N),N)	(21)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(20)
  plus#(N,s(M))	→	and#(isNat(M),n__isNat(N))	(30)
  U11#(tt,N)	→	activate#(N)	(29)
  isNat#(n__s(V1))	→	activate#(V1)	(19)
  isNat#(n__s(V1))	→	isNat#(activate(V1))	(28)
  plus#(N,0)	→	isNat#(N)	(27)
  U21#(tt,M,N)	→	plus#(activate(N),activate(M))	(18)
  plus#(N,s(M))	→	isNat#(M)	(25)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [0#]	=	0
  [U21(x1, x2, x3)]	=	x2 + x3 + 25911
  [U11(x1, x2)]	=	x2 + 0
  [s(x1)]	=	x1 + 25908
  [isNat#(x1)]	=	x1 + 0
  [activate(x1)]	=	x1 + 0
  [and(x1, x2)]	=	x1 + x2 + 0
  [plus#(x1, x2)]	=	x1 + x2 + 2
  [activate#(x1)]	=	x1 + 0
  [n__s(x1)]	=	x1 + 25908
  [0]	=	47339
  [s#(x1)]	=	0
  [n__isNat(x1)]	=	x1 + 1
  [n__plus(x1, x2)]	=	x1 + x2 + 3
  [n__0]	=	47339
  [isNat(x1)]	=	x1 + 1
  [plus(x1, x2)]	=	x1 + x2 + 3
  [U11#(x1, x2)]	=	x2 + 1
  [U21#(x1, x2, x3)]	=	x2 + x3 + 3
  [tt]	=	2241
  [and#(x1, x2)]	=	x2 + 1

  together with the usable rules

  isNat(n__0)	→	tt	(4)
  activate(n__isNat(X))	→	isNat(X)	(15)
  plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
  U11(tt,N)	→	activate(N)	(1)
  and(tt,X)	→	activate(X)	(3)
  activate(n__s(X))	→	s(X)	(16)
  activate(X)	→	X	(17)
  isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
  plus(X1,X2)	→	n__plus(X1,X2)	(10)
  plus(N,0)	→	U11(isNat(N),N)	(7)
  activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
  s(X)	→	n__s(X)	(12)
  isNat(X)	→	n__isNat(X)	(11)
  0	→	n__0	(9)
  activate(n__0)	→	0	(13)
  isNat(n__s(V1))	→	isNat(activate(V1))	(6)
  U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)

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

  plus#(N,s(M))	→	U21#(and(isNat(M),n__isNat(N)),M,N)	(38)
  U21#(tt,M,N)	→	activate#(M)	(37)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(24)
  isNat#(n__plus(V1,V2))	→	isNat#(activate(V1))	(23)
  activate#(n__plus(X1,X2))	→	plus#(X1,X2)	(35)
  U21#(tt,M,N)	→	activate#(N)	(33)
  and#(tt,X)	→	activate#(X)	(32)
  activate#(n__isNat(X))	→	isNat#(X)	(31)
  isNat#(n__plus(V1,V2))	→	and#(isNat(activate(V1)),n__isNat(activate(V2)))	(22)
  plus#(N,0)	→	U11#(isNat(N),N)	(21)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(20)
  plus#(N,s(M))	→	and#(isNat(M),n__isNat(N))	(30)
  U11#(tt,N)	→	activate#(N)	(29)
  isNat#(n__s(V1))	→	activate#(V1)	(19)
  isNat#(n__s(V1))	→	isNat#(activate(V1))	(28)
  plus#(N,0)	→	isNat#(N)	(27)
  U21#(tt,M,N)	→	plus#(activate(N),activate(M))	(18)
  plus#(N,s(M))	→	isNat#(M)	(25)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.