Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_iGM)

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

• The 1^st component contains the pair

  mark#(isNat(X))	→	active#(isNat(X))	(76)
  active#(isNat(s(V1)))	→	mark#(isNat(V1))	(50)
  active#(isNat(plus(V1,V2)))	→	mark#(and(isNat(V1),isNat(V2)))	(48)
  mark#(and(X1,X2))	→	active#(and(mark(X1),X2))	(75)
  active#(and(tt,X))	→	mark#(X)	(43)
  mark#(and(X1,X2))	→	mark#(X1)	(73)
  mark#(plus(X1,X2))	→	active#(plus(mark(X1),mark(X2)))	(72)
  active#(plus(N,s(M)))	→	mark#(U21(and(isNat(M),isNat(N)),M,N))	(58)
  mark#(U21(X1,X2,X3))	→	active#(U21(mark(X1),X2,X3))	(65)
  active#(U21(tt,M,N))	→	mark#(s(plus(N,M)))	(42)
  mark#(s(X))	→	mark#(X)	(66)
  mark#(plus(X1,X2))	→	mark#(X1)	(70)
  mark#(plus(X1,X2))	→	mark#(X2)	(69)
  mark#(U21(X1,X2,X3))	→	mark#(X1)	(63)
  mark#(U11(X1,X2))	→	active#(U11(mark(X1),X2))	(61)
  active#(U11(tt,N))	→	mark#(N)	(39)
  mark#(U11(X1,X2))	→	mark#(X1)	(59)
  active#(plus(N,0))	→	mark#(U11(isNat(N),N))	(53)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [U21(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 7 · x3 + 0
  [0]	=	0
  [U11(x1, x2)]	=	2 · x1 + 7 · x2 + 0
  [mark(x1)]	=	0 · x1 + -∞
  [plus(x1, x2)]	=	7 · x1 + 0 · x2 + 0
  [active#(x1)]	=	0 · x1 + 0
  [tt]	=	0
  [and(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [mark#(x1)]	=	0 · x1 + 0
  [isNat(x1)]	=	0 · x1 + -∞
  [s(x1)]	=	0 · x1 + -∞
  [active(x1)]	=	0 · x1 + -∞

  together with the usable rules

  active(U11(tt,N))	→	mark(N)	(1)
  active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
  active(and(tt,X))	→	mark(X)	(3)
  active(isNat(0))	→	mark(tt)	(4)
  active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
  active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
  active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
  active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
  mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
  mark(tt)	→	active(tt)	(10)
  mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
  mark(s(X))	→	active(s(mark(X)))	(12)
  mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
  mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
  mark(isNat(X))	→	active(isNat(X))	(15)
  mark(0)	→	active(0)	(16)
  U11(mark(X1),X2)	→	U11(X1,X2)	(17)
  U11(X1,mark(X2))	→	U11(X1,X2)	(18)
  U11(active(X1),X2)	→	U11(X1,X2)	(19)
  U11(X1,active(X2))	→	U11(X1,X2)	(20)
  U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
  U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
  U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
  U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
  U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
  U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
  s(mark(X))	→	s(X)	(27)
  s(active(X))	→	s(X)	(28)
  plus(mark(X1),X2)	→	plus(X1,X2)	(29)
  plus(X1,mark(X2))	→	plus(X1,X2)	(30)
  plus(active(X1),X2)	→	plus(X1,X2)	(31)
  plus(X1,active(X2))	→	plus(X1,X2)	(32)
  and(mark(X1),X2)	→	and(X1,X2)	(33)
  and(X1,mark(X2))	→	and(X1,X2)	(34)
  and(active(X1),X2)	→	and(X1,X2)	(35)
  and(X1,active(X2))	→	and(X1,X2)	(36)
  isNat(mark(X))	→	isNat(X)	(37)
  isNat(active(X))	→	isNat(X)	(38)

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

  active#(U11(tt,N))

  →

  mark#(N)

  (39)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    mark#(isNat(X))	→	active#(isNat(X))	(76)
    active#(isNat(s(V1)))	→	mark#(isNat(V1))	(50)
    active#(isNat(plus(V1,V2)))	→	mark#(and(isNat(V1),isNat(V2)))	(48)
    mark#(and(X1,X2))	→	active#(and(mark(X1),X2))	(75)
    active#(and(tt,X))	→	mark#(X)	(43)
    mark#(and(X1,X2))	→	mark#(X1)	(73)
    mark#(plus(X1,X2))	→	active#(plus(mark(X1),mark(X2)))	(72)
    active#(plus(N,s(M)))	→	mark#(U21(and(isNat(M),isNat(N)),M,N))	(58)
    mark#(U21(X1,X2,X3))	→	active#(U21(mark(X1),X2,X3))	(65)
    active#(U21(tt,M,N))	→	mark#(s(plus(N,M)))	(42)
    mark#(s(X))	→	mark#(X)	(66)
    mark#(plus(X1,X2))	→	mark#(X1)	(70)
    mark#(plus(X1,X2))	→	mark#(X2)	(69)
    mark#(U21(X1,X2,X3))	→	mark#(X1)	(63)
    mark#(U11(X1,X2))	→	mark#(X1)	(59)
    active#(plus(N,0))	→	mark#(U11(isNat(N),N))	(53)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [U21(x1, x2, x3)]	=	0 · x1 + 0 · x2 + 1 · x3 + 0
    [0]	=	4
    [U11(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [mark(x1)]	=	0 · x1 + 0
    [plus(x1, x2)]	=	1 · x1 + 0 · x2 + 2
    [active#(x1)]	=	0 · x1 + -∞
    [tt]	=	2
    [and(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [mark#(x1)]	=	0 · x1 + 0
    [isNat(x1)]	=	0 · x1 + -∞
    [s(x1)]	=	0 · x1 + 0
    [active(x1)]	=	0 · x1 + 0

    together with the usable rules

    active(U11(tt,N))	→	mark(N)	(1)
    active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
    active(and(tt,X))	→	mark(X)	(3)
    active(isNat(0))	→	mark(tt)	(4)
    active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
    active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
    active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
    active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
    mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
    mark(tt)	→	active(tt)	(10)
    mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
    mark(s(X))	→	active(s(mark(X)))	(12)
    mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
    mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
    mark(isNat(X))	→	active(isNat(X))	(15)
    mark(0)	→	active(0)	(16)
    U11(mark(X1),X2)	→	U11(X1,X2)	(17)
    U11(X1,mark(X2))	→	U11(X1,X2)	(18)
    U11(active(X1),X2)	→	U11(X1,X2)	(19)
    U11(X1,active(X2))	→	U11(X1,X2)	(20)
    U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
    U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
    U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
    U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
    U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
    U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
    s(mark(X))	→	s(X)	(27)
    s(active(X))	→	s(X)	(28)
    plus(mark(X1),X2)	→	plus(X1,X2)	(29)
    plus(X1,mark(X2))	→	plus(X1,X2)	(30)
    plus(active(X1),X2)	→	plus(X1,X2)	(31)
    plus(X1,active(X2))	→	plus(X1,X2)	(32)
    and(mark(X1),X2)	→	and(X1,X2)	(33)
    and(X1,mark(X2))	→	and(X1,X2)	(34)
    and(active(X1),X2)	→	and(X1,X2)	(35)
    and(X1,active(X2))	→	and(X1,X2)	(36)
    isNat(mark(X))	→	isNat(X)	(37)
    isNat(active(X))	→	isNat(X)	(38)

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

    mark#(plus(X1,X2))	→	mark#(X1)	(70)
    active#(plus(N,0))	→	mark#(U11(isNat(N),N))	(53)

    could be deleted.

    1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

    [U21(x1, x2, x3)]	=	3 · x1 + 4 · x2 + 4 · x3 + -∞
    [0]	=	2
    [U11(x1, x2)]	=	0 · x1 + 4 · x2 + -∞
    [mark(x1)]	=	0 · x1 + -∞
    [plus(x1, x2)]	=	4 · x1 + 4 · x2 + 2
    [active#(x1)]	=	0 · x1 + 0
    [tt]	=	0
    [and(x1, x2)]	=	0 · x1 + 1 · x2 + 0
    [mark#(x1)]	=	0 · x1 + 0
    [isNat(x1)]	=	0 · x1 + 0
    [s(x1)]	=	0 · x1 + 0
    [active(x1)]	=	0 · x1 + -∞

    together with the usable rules

    active(U11(tt,N))	→	mark(N)	(1)
    active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
    active(and(tt,X))	→	mark(X)	(3)
    active(isNat(0))	→	mark(tt)	(4)
    active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
    active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
    active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
    active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
    mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
    mark(tt)	→	active(tt)	(10)
    mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
    mark(s(X))	→	active(s(mark(X)))	(12)
    mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
    mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
    mark(isNat(X))	→	active(isNat(X))	(15)
    mark(0)	→	active(0)	(16)
    U11(mark(X1),X2)	→	U11(X1,X2)	(17)
    U11(X1,mark(X2))	→	U11(X1,X2)	(18)
    U11(active(X1),X2)	→	U11(X1,X2)	(19)
    U11(X1,active(X2))	→	U11(X1,X2)	(20)
    U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
    U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
    U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
    U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
    U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
    U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
    s(mark(X))	→	s(X)	(27)
    s(active(X))	→	s(X)	(28)
    plus(mark(X1),X2)	→	plus(X1,X2)	(29)
    plus(X1,mark(X2))	→	plus(X1,X2)	(30)
    plus(active(X1),X2)	→	plus(X1,X2)	(31)
    plus(X1,active(X2))	→	plus(X1,X2)	(32)
    and(mark(X1),X2)	→	and(X1,X2)	(33)
    and(X1,mark(X2))	→	and(X1,X2)	(34)
    and(active(X1),X2)	→	and(X1,X2)	(35)
    and(X1,active(X2))	→	and(X1,X2)	(36)
    isNat(mark(X))	→	isNat(X)	(37)
    isNat(active(X))	→	isNat(X)	(38)

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

    active#(isNat(plus(V1,V2)))	→	mark#(and(isNat(V1),isNat(V2)))	(48)
    mark#(plus(X1,X2))	→	mark#(X2)	(69)

    could be deleted.

    1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 2 components.

    • The 1^st component contains the pair

      mark#(and(X1,X2))	→	mark#(X1)	(73)
      mark#(and(X1,X2))	→	active#(and(mark(X1),X2))	(75)
      active#(and(tt,X))	→	mark#(X)	(43)
      mark#(plus(X1,X2))	→	active#(plus(mark(X1),mark(X2)))	(72)
      active#(plus(N,s(M)))	→	mark#(U21(and(isNat(M),isNat(N)),M,N))	(58)
      mark#(U21(X1,X2,X3))	→	active#(U21(mark(X1),X2,X3))	(65)
      active#(U21(tt,M,N))	→	mark#(s(plus(N,M)))	(42)
      mark#(s(X))	→	mark#(X)	(66)
      mark#(U21(X1,X2,X3))	→	mark#(X1)	(63)
      mark#(U11(X1,X2))	→	mark#(X1)	(59)

      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

      [U21(x1, x2, x3)]	=	4 · x1 + 0 · x2 + 6 · x3 + 0
      [0]	=	5
      [U11(x1, x2)]	=	2 · x1 + 1 · x2 + 4
      [mark(x1)]	=	0 · x1 + -∞
      [plus(x1, x2)]	=	6 · x1 + 0 · x2 + -∞
      [active#(x1)]	=	0 · x1 + 0
      [tt]	=	3
      [and(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [mark#(x1)]	=	0 · x1 + 0
      [isNat(x1)]	=	-∞ · x1 + 3
      [s(x1)]	=	0 · x1 + 7
      [active(x1)]	=	0 · x1 + -∞

      together with the usable rules

      active(U11(tt,N))	→	mark(N)	(1)
      active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
      active(and(tt,X))	→	mark(X)	(3)
      active(isNat(0))	→	mark(tt)	(4)
      active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
      active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
      active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
      active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
      mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
      mark(tt)	→	active(tt)	(10)
      mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
      mark(s(X))	→	active(s(mark(X)))	(12)
      mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
      mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
      mark(isNat(X))	→	active(isNat(X))	(15)
      mark(0)	→	active(0)	(16)
      U11(mark(X1),X2)	→	U11(X1,X2)	(17)
      U11(X1,mark(X2))	→	U11(X1,X2)	(18)
      U11(active(X1),X2)	→	U11(X1,X2)	(19)
      U11(X1,active(X2))	→	U11(X1,X2)	(20)
      U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
      U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
      U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
      U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
      U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
      U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
      s(mark(X))	→	s(X)	(27)
      s(active(X))	→	s(X)	(28)
      plus(mark(X1),X2)	→	plus(X1,X2)	(29)
      plus(X1,mark(X2))	→	plus(X1,X2)	(30)
      plus(active(X1),X2)	→	plus(X1,X2)	(31)
      plus(X1,active(X2))	→	plus(X1,X2)	(32)
      and(mark(X1),X2)	→	and(X1,X2)	(33)
      and(X1,mark(X2))	→	and(X1,X2)	(34)
      and(active(X1),X2)	→	and(X1,X2)	(35)
      and(X1,active(X2))	→	and(X1,X2)	(36)
      isNat(mark(X))	→	isNat(X)	(37)
      isNat(active(X))	→	isNat(X)	(38)

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

      mark#(U11(X1,X2))

      →

      mark#(X1)

      (59)

      could be deleted.

      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

      [U21(x1, x2, x3)]	=	0 · x1 + 4 · x2 + 4 · x3 + 0
      [0]	=	0
      [U11(x1, x2)]	=	4 · x1 + 4 · x2 + 2
      [mark(x1)]	=	0 · x1 + -∞
      [plus(x1, x2)]	=	4 · x1 + 4 · x2 + 0
      [active#(x1)]	=	0 · x1 + -∞
      [tt]	=	0
      [and(x1, x2)]	=	4 · x1 + 0 · x2 + -∞
      [mark#(x1)]	=	0 · x1 + -∞
      [isNat(x1)]	=	0 · x1 + -∞
      [s(x1)]	=	0 · x1 + -∞
      [active(x1)]	=	0 · x1 + -∞

      together with the usable rules

      active(U11(tt,N))	→	mark(N)	(1)
      active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
      active(and(tt,X))	→	mark(X)	(3)
      active(isNat(0))	→	mark(tt)	(4)
      active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
      active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
      active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
      active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
      mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
      mark(tt)	→	active(tt)	(10)
      mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
      mark(s(X))	→	active(s(mark(X)))	(12)
      mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
      mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
      mark(isNat(X))	→	active(isNat(X))	(15)
      mark(0)	→	active(0)	(16)
      U11(mark(X1),X2)	→	U11(X1,X2)	(17)
      U11(X1,mark(X2))	→	U11(X1,X2)	(18)
      U11(active(X1),X2)	→	U11(X1,X2)	(19)
      U11(X1,active(X2))	→	U11(X1,X2)	(20)
      U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
      U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
      U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
      U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
      U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
      U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
      s(mark(X))	→	s(X)	(27)
      s(active(X))	→	s(X)	(28)
      plus(mark(X1),X2)	→	plus(X1,X2)	(29)
      plus(X1,mark(X2))	→	plus(X1,X2)	(30)
      plus(active(X1),X2)	→	plus(X1,X2)	(31)
      plus(X1,active(X2))	→	plus(X1,X2)	(32)
      and(mark(X1),X2)	→	and(X1,X2)	(33)
      and(X1,mark(X2))	→	and(X1,X2)	(34)
      and(active(X1),X2)	→	and(X1,X2)	(35)
      and(X1,active(X2))	→	and(X1,X2)	(36)
      isNat(mark(X))	→	isNat(X)	(37)
      isNat(active(X))	→	isNat(X)	(38)

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

      mark#(and(X1,X2))

      →

      mark#(X1)

      (73)

      could be deleted.

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

      [U21(x1, x2, x3)]	=	1 · x1 + 0 · x2 + 0 · x3 + 1
      [0]	=	0
      [U11(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [mark(x1)]	=	0 · x1 + 0
      [plus(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [active#(x1)]	=	0 · x1 + 0
      [tt]	=	0
      [and(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
      [mark#(x1)]	=	0 · x1 + 0
      [isNat(x1)]	=	-∞ · x1 + 0
      [s(x1)]	=	0 · x1 + 1
      [active(x1)]	=	0 · x1 + 0

      together with the usable rules

      active(U11(tt,N))	→	mark(N)	(1)
      active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
      active(and(tt,X))	→	mark(X)	(3)
      active(isNat(0))	→	mark(tt)	(4)
      active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
      active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
      active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
      active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
      mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
      mark(tt)	→	active(tt)	(10)
      mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
      mark(s(X))	→	active(s(mark(X)))	(12)
      mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
      mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
      mark(isNat(X))	→	active(isNat(X))	(15)
      mark(0)	→	active(0)	(16)
      U11(mark(X1),X2)	→	U11(X1,X2)	(17)
      U11(X1,mark(X2))	→	U11(X1,X2)	(18)
      U11(active(X1),X2)	→	U11(X1,X2)	(19)
      U11(X1,active(X2))	→	U11(X1,X2)	(20)
      U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
      U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
      U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
      U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
      U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
      U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
      s(mark(X))	→	s(X)	(27)
      s(active(X))	→	s(X)	(28)
      plus(mark(X1),X2)	→	plus(X1,X2)	(29)
      plus(X1,mark(X2))	→	plus(X1,X2)	(30)
      plus(active(X1),X2)	→	plus(X1,X2)	(31)
      plus(X1,active(X2))	→	plus(X1,X2)	(32)
      and(mark(X1),X2)	→	and(X1,X2)	(33)
      and(X1,mark(X2))	→	and(X1,X2)	(34)
      and(active(X1),X2)	→	and(X1,X2)	(35)
      and(X1,active(X2))	→	and(X1,X2)	(36)
      isNat(mark(X))	→	isNat(X)	(37)
      isNat(active(X))	→	isNat(X)	(38)

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

      mark#(U21(X1,X2,X3))

      →

      mark#(X1)

      (63)

      could be deleted.

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

      [U21(x1, x2, x3)]	=	-∞ · x1 + 6 · x2 + 0 · x3 + 0
      [0]	=	1
      [U11(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
      [mark(x1)]	=	0 · x1 + -∞
      [plus(x1, x2)]	=	0 · x1 + 6 · x2 + -∞
      [active#(x1)]	=	0 · x1 + -∞
      [tt]	=	1
      [and(x1, x2)]	=	0 · x1 + 4 · x2 + -∞
      [mark#(x1)]	=	0 · x1 + 0
      [isNat(x1)]	=	0 · x1 + -∞
      [s(x1)]	=	0 · x1 + 0
      [active(x1)]	=	0 · x1 + -∞

      together with the usable rules

      active(U11(tt,N))	→	mark(N)	(1)
      active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
      active(and(tt,X))	→	mark(X)	(3)
      active(isNat(0))	→	mark(tt)	(4)
      active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
      active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
      active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
      active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
      mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
      mark(tt)	→	active(tt)	(10)
      mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
      mark(s(X))	→	active(s(mark(X)))	(12)
      mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
      mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
      mark(isNat(X))	→	active(isNat(X))	(15)
      mark(0)	→	active(0)	(16)
      U11(mark(X1),X2)	→	U11(X1,X2)	(17)
      U11(X1,mark(X2))	→	U11(X1,X2)	(18)
      U11(active(X1),X2)	→	U11(X1,X2)	(19)
      U11(X1,active(X2))	→	U11(X1,X2)	(20)
      U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
      U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
      U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
      U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
      U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
      U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
      s(mark(X))	→	s(X)	(27)
      s(active(X))	→	s(X)	(28)
      plus(mark(X1),X2)	→	plus(X1,X2)	(29)
      plus(X1,mark(X2))	→	plus(X1,X2)	(30)
      plus(active(X1),X2)	→	plus(X1,X2)	(31)
      plus(X1,active(X2))	→	plus(X1,X2)	(32)
      and(mark(X1),X2)	→	and(X1,X2)	(33)
      and(X1,mark(X2))	→	and(X1,X2)	(34)
      and(active(X1),X2)	→	and(X1,X2)	(35)
      and(X1,active(X2))	→	and(X1,X2)	(36)
      isNat(mark(X))	→	isNat(X)	(37)
      isNat(active(X))	→	isNat(X)	(38)

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

      active#(and(tt,X))

      →

      mark#(X)

      (43)

      could be deleted.

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

        mark#(s(X))	→	mark#(X)	(66)
        mark#(plus(X1,X2))	→	active#(plus(mark(X1),mark(X2)))	(72)
        active#(plus(N,s(M)))	→	mark#(U21(and(isNat(M),isNat(N)),M,N))	(58)
        mark#(U21(X1,X2,X3))	→	active#(U21(mark(X1),X2,X3))	(65)
        active#(U21(tt,M,N))	→	mark#(s(plus(N,M)))	(42)

        1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

        [U21(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 3 · x3 + 2
        [0]	=	3
        [U11(x1, x2)]	=	2 · x1 + 2 · x2 + 0
        [mark(x1)]	=	1 · x1 + 0
        [plus(x1, x2)]	=	3 · x1 + 1 · x2 + 0
        [active#(x1)]	=	2 · x1 + 0
        [tt]	=	2
        [and(x1, x2)]	=	0 · x1 + 1 · x2 + 0
        [mark#(x1)]	=	2 · x1 + 0
        [isNat(x1)]	=	1/2 · x1 + 1/2
        [s(x1)]	=	1 · x1 + 2
        [active(x1)]	=	1 · x1 + 0

        together with the usable rules

        active(U11(tt,N))	→	mark(N)	(1)
        active(U21(tt,M,N))	→	mark(s(plus(N,M)))	(2)
        active(and(tt,X))	→	mark(X)	(3)
        active(isNat(0))	→	mark(tt)	(4)
        active(isNat(plus(V1,V2)))	→	mark(and(isNat(V1),isNat(V2)))	(5)
        active(isNat(s(V1)))	→	mark(isNat(V1))	(6)
        active(plus(N,0))	→	mark(U11(isNat(N),N))	(7)
        active(plus(N,s(M)))	→	mark(U21(and(isNat(M),isNat(N)),M,N))	(8)
        mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(9)
        mark(tt)	→	active(tt)	(10)
        mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(11)
        mark(s(X))	→	active(s(mark(X)))	(12)
        mark(plus(X1,X2))	→	active(plus(mark(X1),mark(X2)))	(13)
        mark(and(X1,X2))	→	active(and(mark(X1),X2))	(14)
        mark(isNat(X))	→	active(isNat(X))	(15)
        mark(0)	→	active(0)	(16)
        U11(mark(X1),X2)	→	U11(X1,X2)	(17)
        U11(X1,mark(X2))	→	U11(X1,X2)	(18)
        U11(active(X1),X2)	→	U11(X1,X2)	(19)
        U11(X1,active(X2))	→	U11(X1,X2)	(20)
        U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(21)
        U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(22)
        U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(23)
        U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(24)
        U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(25)
        U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(26)
        s(mark(X))	→	s(X)	(27)
        s(active(X))	→	s(X)	(28)
        plus(mark(X1),X2)	→	plus(X1,X2)	(29)
        plus(X1,mark(X2))	→	plus(X1,X2)	(30)
        plus(active(X1),X2)	→	plus(X1,X2)	(31)
        plus(X1,active(X2))	→	plus(X1,X2)	(32)
        and(mark(X1),X2)	→	and(X1,X2)	(33)
        and(X1,mark(X2))	→	and(X1,X2)	(34)
        and(active(X1),X2)	→	and(X1,X2)	(35)
        and(X1,active(X2))	→	and(X1,X2)	(36)
        isNat(mark(X))	→	isNat(X)	(37)
        isNat(active(X))	→	isNat(X)	(38)

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

        mark#(s(X))

        →

        mark#(X)

        (66)

        could be deleted.

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

      mark#(isNat(X))	→	active#(isNat(X))	(76)
      active#(isNat(s(V1)))	→	mark#(isNat(V1))	(50)

      1.1.1.1.1.1.1.2 Subterm Criterion Processor

      We use the projection to multisets

      π(mark#)	=	{ 1 }
      π(active#)	=	{ 1 }
      π(isNat)	=	{ 1 }

      to remove the pairs:

      active#(isNat(s(V1)))

      →

      mark#(isNat(V1))

      (50)

      1.1.1.1.1.1.1.2.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  plus#(mark(X1),X2)	→	plus#(X1,X2)	(90)
  plus#(X1,active(X2))	→	plus#(X1,X2)	(93)
  plus#(active(X1),X2)	→	plus#(X1,X2)	(92)
  plus#(X1,mark(X2))	→	plus#(X1,X2)	(91)

  1.1.2 Size-Change Termination

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

  plus#(mark(X1),X2)	→	plus#(X1,X2)	(90)
  2	≥	2
  1	>	1
  plus#(X1,active(X2))	→	plus#(X1,X2)	(93)
  2	>	2
  1	≥	1
  plus#(active(X1),X2)	→	plus#(X1,X2)	(92)
  2	≥	2
  1	>	1
  plus#(X1,mark(X2))	→	plus#(X1,X2)	(91)
  2	>	2
  1	≥	1

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

• The 3^rd component contains the pair

  s#(mark(X))	→	s#(X)	(88)
  s#(active(X))	→	s#(X)	(89)

  1.1.3 Size-Change Termination

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

  s#(mark(X))	→	s#(X)	(88)
  1	>	1
  s#(active(X))	→	s#(X)	(89)
  1	>	1

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

• The 4^th component contains the pair

  isNat#(mark(X))	→	isNat#(X)	(98)
  isNat#(active(X))	→	isNat#(X)	(99)

  1.1.4 Size-Change Termination

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

  isNat#(mark(X))	→	isNat#(X)	(98)
  1	>	1
  isNat#(active(X))	→	isNat#(X)	(99)
  1	>	1

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

• The 5^th component contains the pair

  and#(mark(X1),X2)	→	and#(X1,X2)	(94)
  and#(X1,active(X2))	→	and#(X1,X2)	(97)
  and#(active(X1),X2)	→	and#(X1,X2)	(96)
  and#(X1,mark(X2))	→	and#(X1,X2)	(95)

  1.1.5 Size-Change Termination

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

  and#(mark(X1),X2)	→	and#(X1,X2)	(94)
  2	≥	2
  1	>	1
  and#(X1,active(X2))	→	and#(X1,X2)	(97)
  2	>	2
  1	≥	1
  and#(active(X1),X2)	→	and#(X1,X2)	(96)
  2	≥	2
  1	>	1
  and#(X1,mark(X2))	→	and#(X1,X2)	(95)
  2	>	2
  1	≥	1

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

• The 6^th component contains the pair

  U11#(mark(X1),X2)	→	U11#(X1,X2)	(78)
  U11#(X1,active(X2))	→	U11#(X1,X2)	(81)
  U11#(active(X1),X2)	→	U11#(X1,X2)	(80)
  U11#(X1,mark(X2))	→	U11#(X1,X2)	(79)

  1.1.6 Size-Change Termination

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

  U11#(mark(X1),X2)	→	U11#(X1,X2)	(78)
  2	≥	2
  1	>	1
  U11#(X1,active(X2))	→	U11#(X1,X2)	(81)
  2	>	2
  1	≥	1
  U11#(active(X1),X2)	→	U11#(X1,X2)	(80)
  2	≥	2
  1	>	1
  U11#(X1,mark(X2))	→	U11#(X1,X2)	(79)
  2	>	2
  1	≥	1

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

• The 7^th component contains the pair

  U21#(mark(X1),X2,X3)	→	U21#(X1,X2,X3)	(82)
  U21#(X1,X2,active(X3))	→	U21#(X1,X2,X3)	(87)
  U21#(X1,active(X2),X3)	→	U21#(X1,X2,X3)	(86)
  U21#(active(X1),X2,X3)	→	U21#(X1,X2,X3)	(85)
  U21#(X1,X2,mark(X3))	→	U21#(X1,X2,X3)	(84)
  U21#(X1,mark(X2),X3)	→	U21#(X1,X2,X3)	(83)

  1.1.7 Size-Change Termination

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

  U21#(mark(X1),X2,X3)	→	U21#(X1,X2,X3)	(82)
  3	≥	3
  2	≥	2
  1	>	1
  U21#(X1,X2,active(X3))	→	U21#(X1,X2,X3)	(87)
  3	>	3
  2	≥	2
  1	≥	1
  U21#(X1,active(X2),X3)	→	U21#(X1,X2,X3)	(86)
  3	≥	3
  2	>	2
  1	≥	1
  U21#(active(X1),X2,X3)	→	U21#(X1,X2,X3)	(85)
  3	≥	3
  2	≥	2
  1	>	1
  U21#(X1,X2,mark(X3))	→	U21#(X1,X2,X3)	(84)
  3	>	3
  2	≥	2
  1	≥	1
  U21#(X1,mark(X2),X3)	→	U21#(X1,X2,X3)	(83)
  3	≥	3
  2	>	2
  1	≥	1

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