Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds-noand_FR)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ 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,0)	→	U31#(isNat(N),N)	(39)
  U31#(tt,N)	→	activate#(N)	(22)
  activate#(n__plus(X1,X2))	→	activate#(X2)	(43)
  activate#(n__plus(X1,X2))	→	activate#(X1)	(44)
  activate#(n__plus(X1,X2))	→	plus#(activate(X1),activate(X2))	(45)
  plus#(N,0)	→	isNat#(N)	(38)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(31)
  activate#(n__s(X))	→	activate#(X)	(46)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(32)
  isNat#(n__plus(V1,V2))	→	isNat#(activate(V1))	(33)
  isNat#(n__plus(V1,V2))	→	U11#(isNat(activate(V1)),activate(V2))	(34)
  U11#(tt,V2)	→	activate#(V2)	(19)
  U11#(tt,V2)	→	isNat#(activate(V2))	(20)
  isNat#(n__s(V1))	→	activate#(V1)	(35)
  isNat#(n__s(V1))	→	isNat#(activate(V1))	(36)
  plus#(N,s(M))	→	isNat#(M)	(40)
  plus#(N,s(M))	→	U41#(isNat(M),M,N)	(41)
  U41#(tt,M,N)	→	activate#(M)	(23)
  U41#(tt,M,N)	→	activate#(N)	(24)
  U41#(tt,M,N)	→	isNat#(activate(N))	(25)
  U41#(tt,M,N)	→	U42#(isNat(activate(N)),activate(M),activate(N))	(26)
  U42#(tt,M,N)	→	activate#(M)	(27)
  U42#(tt,M,N)	→	activate#(N)	(28)
  U42#(tt,M,N)	→	plus#(activate(N),activate(M))	(29)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [U12(x1)]	=	6 · x1 + 13
  [U11#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [U42(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 1 · x3 + 6
  [U11(x1, x2)]	=	-∞ · x1 + 4 · x2 + -∞
  [isNat(x1)]	=	0 · x1 + 1
  [activate#(x1)]	=	0 · x1 + -∞
  [U41#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + 6
  [isNat#(x1)]	=	0 · x1 + -∞
  [U42#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + -∞
  [U21(x1)]	=	1 · x1 + 8
  [s(x1)]	=	0 · x1 + 6
  [tt]	=	0
  [U41(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 1 · x3 + 6
  [U31#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [0]	=	4
  [n__plus(x1, x2)]	=	1 · x1 + 0 · x2 + 0
  [plus#(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [n__0]	=	4
  [plus(x1, x2)]	=	1 · x1 + 0 · x2 + 0
  [n__s(x1)]	=	0 · x1 + 6
  [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [activate(x1)]	=	0 · x1 + -∞

  together with the usable rules

  U31(tt,N)	→	activate(N)	(4)
  U41(tt,M,N)	→	U42(isNat(activate(N)),activate(M),activate(N))	(5)
  U42(tt,M,N)	→	s(plus(activate(N),activate(M)))	(6)
  plus(N,0)	→	U31(isNat(N),N)	(10)
  plus(N,s(M))	→	U41(isNat(M),M,N)	(11)
  0	→	n__0	(12)
  plus(X1,X2)	→	n__plus(X1,X2)	(13)
  s(X)	→	n__s(X)	(14)
  activate(n__0)	→	0	(15)
  activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(16)
  activate(n__s(X))	→	s(activate(X))	(17)
  activate(X)	→	X	(18)

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

  activate#(n__plus(X1,X2))	→	activate#(X1)	(44)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(32)
  isNat#(n__plus(V1,V2))	→	isNat#(activate(V1))	(33)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [U12(x1)]	=	6 · x1 + -16
  [U11#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [U42(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 0 · x3 + 5
  [U11(x1, x2)]	=	-∞ · x1 + 0 · x2 + -16
  [isNat(x1)]	=	0 · x1 + 0
  [activate#(x1)]	=	0 · x1 + -∞
  [U41#(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 0 · x3 + 0
  [isNat#(x1)]	=	0 · x1 + 0
  [U42#(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 0 · x3 + -16
  [U21(x1)]	=	0 · x1 + 0
  [s(x1)]	=	0 · x1 + 3
  [tt]	=	0
  [U41(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 0 · x3 + 5
  [U31#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 2
  [0]	=	0
  [n__plus(x1, x2)]	=	0 · x1 + 2 · x2 + 0
  [plus#(x1, x2)]	=	0 · x1 + 2 · x2 + -∞
  [n__0]	=	0
  [plus(x1, x2)]	=	0 · x1 + 2 · x2 + 0
  [n__s(x1)]	=	0 · x1 + 3
  [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + -8
  [activate(x1)]	=	0 · x1 + -∞

  together with the usable rules

  U31(tt,N)	→	activate(N)	(4)
  U41(tt,M,N)	→	U42(isNat(activate(N)),activate(M),activate(N))	(5)
  U42(tt,M,N)	→	s(plus(activate(N),activate(M)))	(6)
  plus(N,0)	→	U31(isNat(N),N)	(10)
  plus(N,s(M))	→	U41(isNat(M),M,N)	(11)
  0	→	n__0	(12)
  plus(X1,X2)	→	n__plus(X1,X2)	(13)
  s(X)	→	n__s(X)	(14)
  activate(n__0)	→	0	(15)
  activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(16)
  activate(n__s(X))	→	s(activate(X))	(17)
  activate(X)	→	X	(18)

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

  activate#(n__plus(X1,X2))	→	activate#(X2)	(43)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(31)
  plus#(N,s(M))	→	isNat#(M)	(40)
  U41#(tt,M,N)	→	activate#(M)	(23)
  U42#(tt,M,N)	→	activate#(M)	(27)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [U12(x1)]	=	0 · x1 + 0
  [U11#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [U42(x1, x2, x3)]	=	-∞ · x1 + 1 · x2 + 1 · x3 + 1
  [U11(x1, x2)]	=	0 · x1 + 1 · x2 + 0
  [isNat(x1)]	=	0 · x1 + 0
  [activate#(x1)]	=	0 · x1 + 0
  [U41#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + 0
  [isNat#(x1)]	=	0 · x1 + 0
  [U42#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + 0
  [U21(x1)]	=	-∞ · x1 + 0
  [s(x1)]	=	0 · x1 + 0
  [tt]	=	0
  [U41(x1, x2, x3)]	=	-∞ · x1 + 1 · x2 + 1 · x3 + 1
  [U31#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [0]	=	0
  [n__plus(x1, x2)]	=	1 · x1 + 1 · x2 + 1
  [plus#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [n__0]	=	0
  [plus(x1, x2)]	=	1 · x1 + 1 · x2 + 1
  [n__s(x1)]	=	0 · x1 + -∞
  [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [activate(x1)]	=	0 · x1 + 0

  together with the usable rules

  U31(tt,N)	→	activate(N)	(4)
  U41(tt,M,N)	→	U42(isNat(activate(N)),activate(M),activate(N))	(5)
  U42(tt,M,N)	→	s(plus(activate(N),activate(M)))	(6)
  plus(N,0)	→	U31(isNat(N),N)	(10)
  plus(N,s(M))	→	U41(isNat(M),M,N)	(11)
  0	→	n__0	(12)
  plus(X1,X2)	→	n__plus(X1,X2)	(13)
  s(X)	→	n__s(X)	(14)
  activate(n__0)	→	0	(15)
  activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(16)
  activate(n__s(X))	→	s(activate(X))	(17)
  activate(X)	→	X	(18)

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

  activate#(n__plus(X1,X2))	→	plus#(activate(X1),activate(X2))	(45)
  isNat#(n__plus(V1,V2))	→	U11#(isNat(activate(V1)),activate(V2))	(34)

  could be deleted.

  1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 3 components.

  • The 1^st component contains the pair

    plus#(N,s(M))	→	U41#(isNat(M),M,N)	(41)
    U41#(tt,M,N)	→	U42#(isNat(activate(N)),activate(M),activate(N))	(26)
    U42#(tt,M,N)	→	plus#(activate(N),activate(M))	(29)

    1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [U12(x1)]	=	0 · x1 + 0
    [U42(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 1 · x3 + 1
    [U11(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [isNat(x1)]	=	0 · x1 + 1
    [U41#(x1, x2, x3)]	=	0 · x1 + 4 · x2 + 0 · x3 + 4
    [U42#(x1, x2, x3)]	=	2 · x1 + 4 · x2 + 0 · x3 + 2
    [U21(x1)]	=	0 · x1 + 1
    [s(x1)]	=	1 · x1 + 1
    [tt]	=	0
    [U41(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 1 · x3 + 1
    [0]	=	0
    [n__plus(x1, x2)]	=	1 · x1 + 1 · x2 + 0
    [plus#(x1, x2)]	=	0 · x1 + 4 · x2 + 0
    [n__0]	=	0
    [plus(x1, x2)]	=	1 · x1 + 1 · x2 + 0
    [n__s(x1)]	=	1 · x1 + 1
    [U31(x1, x2)]	=	0 · x1 + 1 · x2 + 0
    [activate(x1)]	=	1 · x1 + 0

    together with the usable rules

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

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

    U42#(tt,M,N)

    →

    plus#(activate(N),activate(M))

    (29)

    could be deleted.

    1.1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 2^nd component contains the pair

    isNat#(n__s(V1))

    →

    isNat#(activate(V1))

    (36)

    1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the rationals with delta = 1/64

    [U12(x1)]	=	1/2 · x1 + 3/2
    [U42(x1, x2, x3)]	=	0 · x1 + 2 · x2 + 2 · x3 + 3/2
    [U11(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [isNat(x1)]	=	1 · x1 + 2
    [isNat#(x1)]	=	1 · x1 + 0
    [U21(x1)]	=	5/2 · x1 + 1
    [s(x1)]	=	1 · x1 + 1/2
    [tt]	=	1
    [U41(x1, x2, x3)]	=	0 · x1 + 2 · x2 + 2 · x3 + 2
    [0]	=	0
    [n__plus(x1, x2)]	=	2 · x1 + 2 · x2 + 1
    [n__0]	=	0
    [plus(x1, x2)]	=	2 · x1 + 2 · x2 + 1
    [n__s(x1)]	=	1 · x1 + 1/2
    [U31(x1, x2)]	=	0 · x1 + 2 · x2 + 1
    [activate(x1)]	=	1 · x1 + 0

    together with the usable rules

    U31(tt,N)	→	activate(N)	(4)
    U41(tt,M,N)	→	U42(isNat(activate(N)),activate(M),activate(N))	(5)
    U42(tt,M,N)	→	s(plus(activate(N),activate(M)))	(6)
    plus(N,0)	→	U31(isNat(N),N)	(10)
    plus(N,s(M))	→	U41(isNat(M),M,N)	(11)
    0	→	n__0	(12)
    plus(X1,X2)	→	n__plus(X1,X2)	(13)
    s(X)	→	n__s(X)	(14)
    activate(n__0)	→	0	(15)
    activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(16)
    activate(n__s(X))	→	s(activate(X))	(17)
    activate(X)	→	X	(18)

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

    isNat#(n__s(V1))

    →

    isNat#(activate(V1))

    (36)

    could be deleted.

    1.1.1.1.1.1.2.1 P is empty

    There are no pairs anymore.

  • The 3^rd component contains the pair

    activate#(n__s(X))

    →

    activate#(X)

    (46)

    1.1.1.1.1.1.3 Size-Change Termination

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

    activate#(n__s(X))	→	activate#(X)	(46)
    1	>	1

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