Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete_Z)

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

  isNatKind#(n__s(V1))	→	isNatKind#(activate(V1))	(57)
  isNatKind#(n__plus(V1,V2))	→	activate#(V2)	(52)
  activate#(n__plus(X1,X2))	→	plus#(X1,X2)	(67)
  plus#(N,0)	→	isNat#(N)	(58)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(44)
  activate#(n__isNatKind(X))	→	isNatKind#(X)	(68)
  isNatKind#(n__plus(V1,V2))	→	activate#(V1)	(53)
  activate#(n__and(X1,X2))	→	and#(X1,X2)	(70)
  and#(tt,X)	→	activate#(X)	(43)
  isNatKind#(n__plus(V1,V2))	→	isNatKind#(activate(V1))	(54)
  isNatKind#(n__plus(V1,V2))	→	and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(55)
  isNatKind#(n__s(V1))	→	activate#(V1)	(56)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(45)
  isNat#(n__plus(V1,V2))	→	isNatKind#(activate(V1))	(46)
  isNat#(n__plus(V1,V2))	→	and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(47)
  isNat#(n__plus(V1,V2))	→	U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(48)
  U11#(tt,V1,V2)	→	activate#(V2)	(28)
  U11#(tt,V1,V2)	→	activate#(V1)	(29)
  U11#(tt,V1,V2)	→	isNat#(activate(V1))	(30)
  isNat#(n__s(V1))	→	activate#(V1)	(49)
  isNat#(n__s(V1))	→	isNatKind#(activate(V1))	(50)
  isNat#(n__s(V1))	→	U21#(isNatKind(activate(V1)),activate(V1))	(51)
  U21#(tt,V1)	→	activate#(V1)	(35)
  U21#(tt,V1)	→	isNat#(activate(V1))	(36)
  U11#(tt,V1,V2)	→	U12#(isNat(activate(V1)),activate(V2))	(31)
  U12#(tt,V2)	→	activate#(V2)	(32)
  U12#(tt,V2)	→	isNat#(activate(V2))	(33)
  plus#(N,0)	→	and#(isNat(N),n__isNatKind(N))	(59)
  plus#(N,0)	→	U31#(and(isNat(N),n__isNatKind(N)),N)	(60)
  U31#(tt,N)	→	activate#(N)	(38)
  plus#(N,s(M))	→	isNat#(N)	(61)
  plus#(N,s(M))	→	isNat#(M)	(62)
  plus#(N,s(M))	→	and#(isNat(M),n__isNatKind(M))	(63)
  plus#(N,s(M))	→	and#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(64)
  plus#(N,s(M))	→	U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(65)
  U41#(tt,M,N)	→	activate#(M)	(39)
  U41#(tt,M,N)	→	activate#(N)	(40)
  U41#(tt,M,N)	→	plus#(activate(N),activate(M))	(41)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [0]	=	2
  [U12(x1, x2)]	=	0 · x1 + 4 · x2 + 0
  [isNatKind(x1)]	=	0 · x1 + 2
  [U31(x1, x2)]	=	0 · x1 + 1 · x2 + 0
  [U11(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 6 · x3 + -∞
  [isNat(x1)]	=	5 · x1 + 0
  [n__isNatKind(x1)]	=	0 · x1 + 2
  [activate#(x1)]	=	0 · x1 + -∞
  [n__and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [isNatKind#(x1)]	=	0 · x1 + 0
  [n__s(x1)]	=	0 · x1 + 2
  [U31#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [isNat#(x1)]	=	0 · x1 + -∞
  [U41#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
  [U13(x1)]	=	0 · x1 + 0
  [plus(x1, x2)]	=	1 · x1 + 0 · x2 + 2
  [tt]	=	0
  [U22(x1)]	=	1 · x1 + 0
  [U11#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
  [U21#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [n__plus(x1, x2)]	=	1 · x1 + 0 · x2 + 2
  [and#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [U12#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [s(x1)]	=	0 · x1 + 2
  [U41(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 1 · x3 + 2
  [n__0]	=	2
  [U21(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [plus#(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [activate(x1)]	=	0 · x1 + -∞

  together with the usable rules

  U31(tt,N)	→	activate(N)	(6)
  U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
  and(tt,X)	→	activate(X)	(8)
  isNatKind(n__0)	→	tt	(12)
  isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
  isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
  plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
  plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
  0	→	n__0	(17)
  plus(X1,X2)	→	n__plus(X1,X2)	(18)
  isNatKind(X)	→	n__isNatKind(X)	(19)
  s(X)	→	n__s(X)	(20)
  and(X1,X2)	→	n__and(X1,X2)	(21)
  activate(n__0)	→	0	(22)
  activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
  activate(n__isNatKind(X))	→	isNatKind(X)	(24)
  activate(n__s(X))	→	s(X)	(25)
  activate(n__and(X1,X2))	→	and(X1,X2)	(26)
  activate(X)	→	X	(27)

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

  isNatKind#(n__plus(V1,V2))	→	activate#(V1)	(53)
  isNatKind#(n__plus(V1,V2))	→	isNatKind#(activate(V1))	(54)
  isNat#(n__plus(V1,V2))	→	activate#(V1)	(45)
  isNat#(n__plus(V1,V2))	→	isNatKind#(activate(V1))	(46)

  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

  [0]	=	3
  [U12(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [isNatKind(x1)]	=	0 · x1 + -∞
  [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [U11(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 4 · x3 + -∞
  [isNat(x1)]	=	-∞ · x1 + 0
  [n__isNatKind(x1)]	=	0 · x1 + -∞
  [activate#(x1)]	=	0 · x1 + -∞
  [n__and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [isNatKind#(x1)]	=	0 · x1 + -∞
  [n__s(x1)]	=	0 · x1 + 0
  [U31#(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [isNat#(x1)]	=	0 · x1 + 0
  [U41#(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 0 · x3 + -∞
  [U13(x1)]	=	5 · x1 + 6
  [plus(x1, x2)]	=	0 · x1 + 1 · x2 + 0
  [tt]	=	0
  [U22(x1)]	=	5 · x1 + 0
  [U11#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 0 · x3 + 0
  [U21#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [n__plus(x1, x2)]	=	0 · x1 + 1 · x2 + 0
  [and#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [U12#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [s(x1)]	=	0 · x1 + 0
  [U41(x1, x2, x3)]	=	-∞ · x1 + 1 · x2 + 0 · x3 + 0
  [n__0]	=	3
  [U21(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [plus#(x1, x2)]	=	0 · x1 + 1 · x2 + 0
  [activate(x1)]	=	0 · x1 + -∞

  together with the usable rules

  U31(tt,N)	→	activate(N)	(6)
  U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
  and(tt,X)	→	activate(X)	(8)
  isNatKind(n__0)	→	tt	(12)
  isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
  isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
  plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
  plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
  0	→	n__0	(17)
  plus(X1,X2)	→	n__plus(X1,X2)	(18)
  isNatKind(X)	→	n__isNatKind(X)	(19)
  s(X)	→	n__s(X)	(20)
  and(X1,X2)	→	n__and(X1,X2)	(21)
  activate(n__0)	→	0	(22)
  activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
  activate(n__isNatKind(X))	→	isNatKind(X)	(24)
  activate(n__s(X))	→	s(X)	(25)
  activate(n__and(X1,X2))	→	and(X1,X2)	(26)
  activate(X)	→	X	(27)

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

  isNatKind#(n__plus(V1,V2))	→	activate#(V2)	(52)
  isNat#(n__plus(V1,V2))	→	activate#(V2)	(44)
  isNatKind#(n__plus(V1,V2))	→	and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(55)
  isNat#(n__plus(V1,V2))	→	and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(47)
  plus#(N,s(M))	→	isNat#(M)	(62)
  plus#(N,s(M))	→	and#(isNat(M),n__isNatKind(M))	(63)
  U41#(tt,M,N)	→	activate#(M)	(39)

  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

  [0]	=	4
  [U12(x1, x2)]	=	3 · x1 + 4 · x2 + 5
  [isNatKind(x1)]	=	0 · x1 + 0
  [U31(x1, x2)]	=	0 · x1 + 2 · x2 + 5
  [U11(x1, x2, x3)]	=	0 · x1 + 6 · x2 + 0 · x3 + 5
  [isNat(x1)]	=	-∞ · x1 + 0
  [n__isNatKind(x1)]	=	0 · x1 + 0
  [activate#(x1)]	=	0 · x1 + 0
  [n__and(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [isNatKind#(x1)]	=	0 · x1 + 0
  [n__s(x1)]	=	0 · x1 + 0
  [U31#(x1, x2)]	=	3 · x1 + 0 · x2 + 0
  [isNat#(x1)]	=	0 · x1 + -∞
  [U41#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 3 · x3 + 0
  [U13(x1)]	=	1 · x1 + 8
  [plus(x1, x2)]	=	3 · x1 + 1 · x2 + 0
  [tt]	=	4
  [U22(x1)]	=	-∞ · x1 + 0
  [U11#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
  [U21#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [n__plus(x1, x2)]	=	3 · x1 + 1 · x2 + 0
  [and#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [U12#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [s(x1)]	=	0 · x1 + 0
  [U41(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 3 · x3 + 0
  [n__0]	=	4
  [U21(x1, x2)]	=	1 · x1 + 1 · x2 + 1
  [plus#(x1, x2)]	=	3 · x1 + 0 · x2 + -∞
  [activate(x1)]	=	0 · x1 + 0

  together with the usable rules

  U31(tt,N)	→	activate(N)	(6)
  U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
  and(tt,X)	→	activate(X)	(8)
  isNatKind(n__0)	→	tt	(12)
  isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
  isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
  plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
  plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
  0	→	n__0	(17)
  plus(X1,X2)	→	n__plus(X1,X2)	(18)
  isNatKind(X)	→	n__isNatKind(X)	(19)
  s(X)	→	n__s(X)	(20)
  and(X1,X2)	→	n__and(X1,X2)	(21)
  activate(n__0)	→	0	(22)
  activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
  activate(n__isNatKind(X))	→	isNatKind(X)	(24)
  activate(n__s(X))	→	s(X)	(25)
  activate(n__and(X1,X2))	→	and(X1,X2)	(26)
  activate(X)	→	X	(27)

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

  plus#(N,0)	→	isNat#(N)	(58)
  plus#(N,0)	→	and#(isNat(N),n__isNatKind(N))	(59)
  plus#(N,s(M))	→	isNat#(N)	(61)
  U41#(tt,M,N)	→	activate#(N)	(40)

  could be deleted.

  1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    U21#(tt,V1)	→	isNat#(activate(V1))	(36)
    isNat#(n__plus(V1,V2))	→	U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(48)
    U11#(tt,V1,V2)	→	isNat#(activate(V1))	(30)
    isNat#(n__s(V1))	→	U21#(isNatKind(activate(V1)),activate(V1))	(51)
    U11#(tt,V1,V2)	→	U12#(isNat(activate(V1)),activate(V2))	(31)
    U12#(tt,V2)	→	isNat#(activate(V2))	(33)

    1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [0]	=	0
    [U12(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
    [isNatKind(x1)]	=	1 · x1 + 0
    [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + 1
    [U11(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 0
    [isNat(x1)]	=	0 · x1 + -∞
    [n__isNatKind(x1)]	=	1 · x1 + 0
    [n__and(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
    [n__s(x1)]	=	0 · x1 + 0
    [isNat#(x1)]	=	0 · x1 + -∞
    [U13(x1)]	=	0 · x1 + 0
    [plus(x1, x2)]	=	0 · x1 + 2 · x2 + 0
    [tt]	=	0
    [U22(x1)]	=	-∞ · x1 + 0
    [U11#(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 2 · x3 + 0
    [U21#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
    [n__plus(x1, x2)]	=	0 · x1 + 2 · x2 + 0
    [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
    [U12#(x1, x2)]	=	0 · x1 + 2 · x2 + -∞
    [s(x1)]	=	0 · x1 + 0
    [U41(x1, x2, x3)]	=	-∞ · x1 + 2 · x2 + 0 · x3 + 1
    [n__0]	=	0
    [U21(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
    [activate(x1)]	=	0 · x1 + -∞

    together with the usable rules

    U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
    U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)
    U13(tt)	→	tt	(3)
    U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
    U22(tt)	→	tt	(5)
    U31(tt,N)	→	activate(N)	(6)
    U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
    and(tt,X)	→	activate(X)	(8)
    isNat(n__0)	→	tt	(9)
    isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(10)
    isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(11)
    isNatKind(n__0)	→	tt	(12)
    isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
    isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
    plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
    plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
    0	→	n__0	(17)
    plus(X1,X2)	→	n__plus(X1,X2)	(18)
    isNatKind(X)	→	n__isNatKind(X)	(19)
    s(X)	→	n__s(X)	(20)
    and(X1,X2)	→	n__and(X1,X2)	(21)
    activate(n__0)	→	0	(22)
    activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
    activate(n__isNatKind(X))	→	isNatKind(X)	(24)
    activate(n__s(X))	→	s(X)	(25)
    activate(n__and(X1,X2))	→	and(X1,X2)	(26)
    activate(X)	→	X	(27)

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

    U12#(tt,V2)

    →

    isNat#(activate(V2))

    (33)

    could be deleted.

    1.1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      U21#(tt,V1)	→	isNat#(activate(V1))	(36)
      isNat#(n__plus(V1,V2))	→	U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(48)
      U11#(tt,V1,V2)	→	isNat#(activate(V1))	(30)
      isNat#(n__s(V1))	→	U21#(isNatKind(activate(V1)),activate(V1))	(51)

      1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

      [0]	=	0
      [U12(x1, x2)]	=	3 · x1 + -∞ · x2 + 5
      [isNatKind(x1)]	=	0 · x1 + 0
      [U31(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
      [U11(x1, x2, x3)]	=	-∞ · x1 + -∞ · x2 + 4 · x3 + 0
      [isNat(x1)]	=	-∞ · x1 + 1
      [n__isNatKind(x1)]	=	0 · x1 + -∞
      [n__and(x1, x2)]	=	0 · x1 + 1 · x2 + -∞
      [n__s(x1)]	=	0 · x1 + 0
      [isNat#(x1)]	=	0 · x1 + 0
      [U13(x1)]	=	3 · x1 + 5
      [plus(x1, x2)]	=	1 · x1 + 4 · x2 + 1
      [tt]	=	0
      [U22(x1)]	=	0 · x1 + 0
      [U11#(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 1 · x3 + 1
      [U21#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [n__plus(x1, x2)]	=	1 · x1 + 4 · x2 + 1
      [and(x1, x2)]	=	0 · x1 + 1 · x2 + 0
      [s(x1)]	=	0 · x1 + 0
      [U41(x1, x2, x3)]	=	-∞ · x1 + 4 · x2 + 1 · x3 + 4
      [n__0]	=	0
      [U21(x1, x2)]	=	-∞ · x1 + 2 · x2 + -∞
      [activate(x1)]	=	0 · x1 + 0

      together with the usable rules

      U31(tt,N)	→	activate(N)	(6)
      U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
      and(tt,X)	→	activate(X)	(8)
      isNatKind(n__0)	→	tt	(12)
      isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
      isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
      plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
      plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
      0	→	n__0	(17)
      plus(X1,X2)	→	n__plus(X1,X2)	(18)
      isNatKind(X)	→	n__isNatKind(X)	(19)
      s(X)	→	n__s(X)	(20)
      and(X1,X2)	→	n__and(X1,X2)	(21)
      activate(n__0)	→	0	(22)
      activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
      activate(n__isNatKind(X))	→	isNatKind(X)	(24)
      activate(n__s(X))	→	s(X)	(25)
      activate(n__and(X1,X2))	→	and(X1,X2)	(26)
      activate(X)	→	X	(27)

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

      U11#(tt,V1,V2)

      →

      isNat#(activate(V1))

      (30)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        U21#(tt,V1)	→	isNat#(activate(V1))	(36)
        isNat#(n__s(V1))	→	U21#(isNatKind(activate(V1)),activate(V1))	(51)

        1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [0]	=	0
        [U12(x1, x2)]	=	0 · x1 + 4 · x2 + 4
        [isNatKind(x1)]	=	0 · x1 + 2
        [U31(x1, x2)]	=	0 · x1 + 1 · x2 + 0
        [U11(x1, x2, x3)]	=	0 · x1 + 5 · x2 + 0 · x3 + 1
        [isNat(x1)]	=	0 · x1 + 0
        [n__isNatKind(x1)]	=	0 · x1 + 2
        [n__and(x1, x2)]	=	0 · x1 + 1 · x2 + 0
        [n__s(x1)]	=	1 · x1 + 1
        [isNat#(x1)]	=	4 · x1 + 4
        [U13(x1)]	=	0 · x1 + 4
        [plus(x1, x2)]	=	1 · x1 + 4 · x2 + 0
        [tt]	=	1
        [U22(x1)]	=	2 · x1 + 4
        [U21#(x1, x2)]	=	1 · x1 + 4 · x2 + 6
        [n__plus(x1, x2)]	=	1 · x1 + 4 · x2 + 0
        [and(x1, x2)]	=	0 · x1 + 1 · x2 + 0
        [s(x1)]	=	1 · x1 + 1
        [U41(x1, x2, x3)]	=	0 · x1 + 4 · x2 + 1 · x3 + 4
        [n__0]	=	0
        [U21(x1, x2)]	=	4 · x1 + 0 · x2 + 0
        [activate(x1)]	=	1 · x1 + 0

        together with the usable rules

        U31(tt,N)	→	activate(N)	(6)
        U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
        and(tt,X)	→	activate(X)	(8)
        isNatKind(n__0)	→	tt	(12)
        isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
        isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
        plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
        plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
        0	→	n__0	(17)
        plus(X1,X2)	→	n__plus(X1,X2)	(18)
        isNatKind(X)	→	n__isNatKind(X)	(19)
        s(X)	→	n__s(X)	(20)
        and(X1,X2)	→	n__and(X1,X2)	(21)
        activate(n__0)	→	0	(22)
        activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
        activate(n__isNatKind(X))	→	isNatKind(X)	(24)
        activate(n__s(X))	→	s(X)	(25)
        activate(n__and(X1,X2))	→	and(X1,X2)	(26)
        activate(X)	→	X	(27)

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

        U21#(tt,V1)

        →

        isNat#(activate(V1))

        (36)

        could be deleted.

        1.1.1.1.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

    isNatKind#(n__s(V1))	→	isNatKind#(activate(V1))	(57)
    isNatKind#(n__s(V1))	→	activate#(V1)	(56)
    activate#(n__plus(X1,X2))	→	plus#(X1,X2)	(67)
    plus#(N,0)	→	U31#(and(isNat(N),n__isNatKind(N)),N)	(60)
    U31#(tt,N)	→	activate#(N)	(38)
    activate#(n__isNatKind(X))	→	isNatKind#(X)	(68)
    activate#(n__and(X1,X2))	→	and#(X1,X2)	(70)
    and#(tt,X)	→	activate#(X)	(43)
    plus#(N,s(M))	→	and#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(64)
    plus#(N,s(M))	→	U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(65)
    U41#(tt,M,N)	→	plus#(activate(N),activate(M))	(41)

    1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

    [0]	=	0
    [U12(x1, x2)]	=	1 · x1 + 1 · x2 + 0
    [isNatKind(x1)]	=	0 · x1 + -∞
    [U31(x1, x2)]	=	-∞ · x1 + 1 · x2 + -∞
    [U11(x1, x2, x3)]	=	0 · x1 + -∞ · x2 + 3 · x3 + -∞
    [isNat(x1)]	=	2 · x1 + 5
    [n__isNatKind(x1)]	=	0 · x1 + -∞
    [activate#(x1)]	=	4 · x1 + 0
    [n__and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
    [isNatKind#(x1)]	=	4 · x1 + 0
    [n__s(x1)]	=	0 · x1 + -∞
    [U31#(x1, x2)]	=	-∞ · x1 + 4 · x2 + 0
    [U41#(x1, x2, x3)]	=	0 · x1 + -∞ · x2 + 4 · x3 + 0
    [U13(x1)]	=	-∞ · x1 + 4
    [plus(x1, x2)]	=	1 · x1 + 2 · x2 + 1
    [tt]	=	0
    [U22(x1)]	=	2 · x1 + 0
    [n__plus(x1, x2)]	=	1 · x1 + 2 · x2 + 1
    [and#(x1, x2)]	=	-∞ · x1 + 4 · x2 + 0
    [and(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
    [s(x1)]	=	0 · x1 + -∞
    [U41(x1, x2, x3)]	=	0 · x1 + 2 · x2 + 1 · x3 + 1
    [n__0]	=	0
    [U21(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [plus#(x1, x2)]	=	4 · x1 + -∞ · x2 + 0
    [activate(x1)]	=	0 · x1 + -∞

    together with the usable rules

    U31(tt,N)	→	activate(N)	(6)
    U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
    and(tt,X)	→	activate(X)	(8)
    isNatKind(n__0)	→	tt	(12)
    isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
    isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
    plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
    plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
    0	→	n__0	(17)
    plus(X1,X2)	→	n__plus(X1,X2)	(18)
    isNatKind(X)	→	n__isNatKind(X)	(19)
    s(X)	→	n__s(X)	(20)
    and(X1,X2)	→	n__and(X1,X2)	(21)
    activate(n__0)	→	0	(22)
    activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
    activate(n__isNatKind(X))	→	isNatKind(X)	(24)
    activate(n__s(X))	→	s(X)	(25)
    activate(n__and(X1,X2))	→	and(X1,X2)	(26)
    activate(X)	→	X	(27)

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

    activate#(n__plus(X1,X2))

    →

    plus#(X1,X2)

    (67)

    could be deleted.

    1.1.1.1.1.1.2.1 Dependency Graph Processor

    The dependency pairs are split into 2 components.

    • The 1^st component contains the pair

      plus#(N,s(M))	→	U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(65)
      U41#(tt,M,N)	→	plus#(activate(N),activate(M))	(41)

      1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [0]	=	0
      [U12(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [isNatKind(x1)]	=	0 · x1 + 0
      [U31(x1, x2)]	=	0 · x1 + 2 · x2 + 0
      [U11(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 0 · x3 + 1
      [isNat(x1)]	=	0 · x1 + 1
      [n__isNatKind(x1)]	=	0 · x1 + 0
      [n__and(x1, x2)]	=	4 · x1 + 2 · x2 + 0
      [n__s(x1)]	=	1 · x1 + 5
      [U41#(x1, x2, x3)]	=	0 · x1 + 4 · x2 + 0 · x3 + 4
      [U13(x1)]	=	0 · x1 + 0
      [plus(x1, x2)]	=	2 · x1 + 6 · x2 + 0
      [tt]	=	0
      [U22(x1)]	=	0 · x1 + 0
      [n__plus(x1, x2)]	=	2 · x1 + 6 · x2 + 0
      [and(x1, x2)]	=	4 · x1 + 2 · x2 + 0
      [s(x1)]	=	1 · x1 + 5
      [U41(x1, x2, x3)]	=	1 · x1 + 6 · x2 + 2 · x3 + 6
      [n__0]	=	0
      [U21(x1, x2)]	=	0 · x1 + 0 · x2 + 1
      [plus#(x1, x2)]	=	0 · x1 + 4 · x2 + 1
      [activate(x1)]	=	1 · x1 + 0

      together with the usable rules

      U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
      U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)
      U13(tt)	→	tt	(3)
      U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
      U22(tt)	→	tt	(5)
      U31(tt,N)	→	activate(N)	(6)
      U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
      and(tt,X)	→	activate(X)	(8)
      isNat(n__0)	→	tt	(9)
      isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(10)
      isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(11)
      isNatKind(n__0)	→	tt	(12)
      isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
      isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
      plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
      plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
      0	→	n__0	(17)
      plus(X1,X2)	→	n__plus(X1,X2)	(18)
      isNatKind(X)	→	n__isNatKind(X)	(19)
      s(X)	→	n__s(X)	(20)
      and(X1,X2)	→	n__and(X1,X2)	(21)
      activate(n__0)	→	0	(22)
      activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
      activate(n__isNatKind(X))	→	isNatKind(X)	(24)
      activate(n__s(X))	→	s(X)	(25)
      activate(n__and(X1,X2))	→	and(X1,X2)	(26)
      activate(X)	→	X	(27)

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

      plus#(N,s(M))	→	U41#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(65)
      U41#(tt,M,N)	→	plus#(activate(N),activate(M))	(41)

      could be deleted.

      1.1.1.1.1.1.2.1.1.1 P is empty

      There are no pairs anymore.

    • The 2^nd component contains the pair

      isNatKind#(n__s(V1))	→	isNatKind#(activate(V1))	(57)
      isNatKind#(n__s(V1))	→	activate#(V1)	(56)
      activate#(n__isNatKind(X))	→	isNatKind#(X)	(68)
      activate#(n__and(X1,X2))	→	and#(X1,X2)	(70)
      and#(tt,X)	→	activate#(X)	(43)

      1.1.1.1.1.1.2.1.2 Reduction Pair Processor with Usable Rules

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

      [0]	=	2
      [U12(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
      [isNatKind(x1)]	=	2 · x1 + -∞
      [U31(x1, x2)]	=	-∞ · x1 + 1 · x2 + -∞
      [U11(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 2 · x3 + -∞
      [isNat(x1)]	=	0 · x1 + -∞
      [n__isNatKind(x1)]	=	2 · x1 + -∞
      [activate#(x1)]	=	0 · x1 + -∞
      [n__and(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
      [isNatKind#(x1)]	=	0 · x1 + -∞
      [n__s(x1)]	=	0 · x1 + 0
      [U13(x1)]	=	-∞ · x1 + 0
      [plus(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
      [tt]	=	3
      [U22(x1)]	=	-∞ · x1 + 0
      [n__plus(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
      [and#(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
      [and(x1, x2)]	=	1 · x1 + 0 · x2 + -∞
      [s(x1)]	=	0 · x1 + 0
      [U41(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 1 · x3 + 0
      [n__0]	=	2
      [U21(x1, x2)]	=	2 · x1 + 1 · x2 + 12
      [activate(x1)]	=	0 · x1 + -∞

      together with the usable rules

      U31(tt,N)	→	activate(N)	(6)
      U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
      and(tt,X)	→	activate(X)	(8)
      isNatKind(n__0)	→	tt	(12)
      isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
      isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
      plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
      plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
      0	→	n__0	(17)
      plus(X1,X2)	→	n__plus(X1,X2)	(18)
      isNatKind(X)	→	n__isNatKind(X)	(19)
      s(X)	→	n__s(X)	(20)
      and(X1,X2)	→	n__and(X1,X2)	(21)
      activate(n__0)	→	0	(22)
      activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
      activate(n__isNatKind(X))	→	isNatKind(X)	(24)
      activate(n__s(X))	→	s(X)	(25)
      activate(n__and(X1,X2))	→	and(X1,X2)	(26)
      activate(X)	→	X	(27)

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

      activate#(n__isNatKind(X))

      →

      isNatKind#(X)

      (68)

      could be deleted.

      1.1.1.1.1.1.2.1.2.1 Dependency Graph Processor

      The dependency pairs are split into 2 components.

      • The 1^st component contains the pair

        isNatKind#(n__s(V1))

        →

        isNatKind#(activate(V1))

        (57)

        1.1.1.1.1.1.2.1.2.1.1 Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [0]	=	2
        [U12(x1, x2)]	=	0 · x1 + 0 · x2 + 0
        [isNatKind(x1)]	=	0 · x1 + 1
        [U31(x1, x2)]	=	1 · x1 + 1 · x2 + 6
        [U11(x1, x2, x3)]	=	0 · x1 + 2 · x2 + 0 · x3 + 2
        [isNat(x1)]	=	0 · x1 + 0
        [n__isNatKind(x1)]	=	0 · x1 + 0
        [n__and(x1, x2)]	=	0 · x1 + 4 · x2 + 0
        [isNatKind#(x1)]	=	1 · x1 + 0
        [n__s(x1)]	=	1 · x1 + 2
        [U13(x1)]	=	4 · x1 + 0
        [plus(x1, x2)]	=	1 · x1 + 3 · x2 + 1
        [tt]	=	1
        [U22(x1)]	=	0 · x1 + 2
        [n__plus(x1, x2)]	=	1 · x1 + 3 · x2 + 1
        [and(x1, x2)]	=	0 · x1 + 4 · x2 + 1
        [s(x1)]	=	1 · x1 + 2
        [U41(x1, x2, x3)]	=	0 · x1 + 3 · x2 + 1 · x3 + 7
        [n__0]	=	2
        [U21(x1, x2)]	=	0 · x1 + 0 · x2 + 3
        [activate(x1)]	=	1 · x1 + 1

        together with the usable rules

        U31(tt,N)	→	activate(N)	(6)
        U41(tt,M,N)	→	s(plus(activate(N),activate(M)))	(7)
        and(tt,X)	→	activate(X)	(8)
        isNatKind(n__0)	→	tt	(12)
        isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(13)
        isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(14)
        plus(N,0)	→	U31(and(isNat(N),n__isNatKind(N)),N)	(15)
        plus(N,s(M))	→	U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(16)
        0	→	n__0	(17)
        plus(X1,X2)	→	n__plus(X1,X2)	(18)
        isNatKind(X)	→	n__isNatKind(X)	(19)
        s(X)	→	n__s(X)	(20)
        and(X1,X2)	→	n__and(X1,X2)	(21)
        activate(n__0)	→	0	(22)
        activate(n__plus(X1,X2))	→	plus(X1,X2)	(23)
        activate(n__isNatKind(X))	→	isNatKind(X)	(24)
        activate(n__s(X))	→	s(X)	(25)
        activate(n__and(X1,X2))	→	and(X1,X2)	(26)
        activate(X)	→	X	(27)

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

        isNatKind#(n__s(V1))

        →

        isNatKind#(activate(V1))

        (57)

        could be deleted.

        1.1.1.1.1.1.2.1.2.1.1.1 P is empty

        There are no pairs anymore.

      • The 2^nd component contains the pair

        activate#(n__and(X1,X2))	→	and#(X1,X2)	(70)
        and#(tt,X)	→	activate#(X)	(43)

        1.1.1.1.1.1.2.1.2.1.2 Size-Change Termination

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

        activate#(n__and(X1,X2))	→	and#(X1,X2)	(70)
        1	>	2
        1	>	1
        and#(tt,X)	→	activate#(X)	(43)
        2	≥	1

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