Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann14)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

• The 1^st component contains the pair

  if2#(false,x,y)	→	int#(p(x),p(y))	(34)
  int#(x,y)	→	if_int#(zero(x),zero(y),x,y)	(27)
  if_int#(true,b,x,y)	→	if1#(b,x,y)	(30)
  if1#(false,x,y)	→	int#(s(0),y)	(32)
  if_int#(false,b,x,y)	→	if2#(b,x,y)	(31)

  1.1.1.1 Usable Rules Processor

  We restrict the rewrite rules to the following usable rules of the DP problem.

  zero(0)	→	true	(6)
  zero(s(x))	→	false	(7)
  p(0)	→	0	(8)
  p(s(0))	→	0	(9)
  p(s(s(x)))	→	s(p(s(x)))	(10)

  1.1.1.1.1 Innermost Lhss Removal Processor

  We restrict the innermost strategy to the following left hand sides.

  zero(0)

  zero(s(x0))

  p(0)

  p(s(0))

  p(s(s(x0)))

  1.1.1.1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  int#(0,y1)	→	if_int#(true,zero(y1),0,y1)	(37)
  int#(s(x0),y1)	→	if_int#(false,zero(y1),s(x0),y1)	(38)

  1.1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  if_int#(true,y_0,0,z0)

  →

  if1#(y_0,0,z0)

  (39)

  1.1.1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  if1#(false,0,z1)

  →

  int#(s(0),z1)

  (40)

  1.1.1.1.1.1.1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  if2#(false,0,y1)	→	int#(0,p(y1))	(41)
  if2#(false,s(0),y1)	→	int#(0,p(y1))	(42)
  if2#(false,s(s(x0)),y1)	→	int#(s(p(s(x0))),p(y1))	(43)

  1.1.1.1.1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  if_int#(false,y_0,s(z0),z1)

  →

  if2#(y_0,s(z0),z1)

  (44)

  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

    if_int#(true,y_0,0,z0)	→	if1#(y_0,0,z0)	(39)
    if1#(false,0,z1)	→	int#(s(0),z1)	(40)
    int#(s(x0),y1)	→	if_int#(false,zero(y1),s(x0),y1)	(38)
    if_int#(false,y_0,s(z0),z1)	→	if2#(y_0,s(z0),z1)	(44)
    if2#(false,s(0),y1)	→	int#(0,p(y1))	(42)
    int#(0,y1)	→	if_int#(true,zero(y1),0,y1)	(37)
    if2#(false,s(s(x0)),y1)	→	int#(s(p(s(x0))),p(y1))	(43)

    1.1.1.1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

    We instantiate the pair to the following set of pairs

    if_int#(true,false,0,x1)

    →

    if1#(false,0,x1)

    (45)

    1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

    We consider all narrowings of the pair below position 2 to get the following set of pairs

    int#(0,0)	→	if_int#(true,true,0,0)	(46)
    int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)

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

      int#(s(x0),y1)	→	if_int#(false,zero(y1),s(x0),y1)	(38)
      if_int#(false,y_0,s(z0),z1)	→	if2#(y_0,s(z0),z1)	(44)
      if2#(false,s(0),y1)	→	int#(0,p(y1))	(42)
      int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)
      if_int#(true,false,0,x1)	→	if1#(false,0,x1)	(45)
      if1#(false,0,z1)	→	int#(s(0),z1)	(40)
      if2#(false,s(s(x0)),y1)	→	int#(s(p(s(x0))),p(y1))	(43)

      1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

      We consider all narrowings of the pair below position 2 to get the following set of pairs

      if2#(false,s(0),0)	→	int#(0,0)	(48)
      if2#(false,s(0),s(0))	→	int#(0,0)	(49)
      if2#(false,s(0),s(s(x0)))	→	int#(0,s(p(s(x0))))	(50)

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

        if_int#(false,y_0,s(z0),z1)	→	if2#(y_0,s(z0),z1)	(44)
        if2#(false,s(s(x0)),y1)	→	int#(s(p(s(x0))),p(y1))	(43)
        int#(s(x0),y1)	→	if_int#(false,zero(y1),s(x0),y1)	(38)
        if2#(false,s(0),s(s(x0)))	→	int#(0,s(p(s(x0))))	(50)
        int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)
        if_int#(true,false,0,x1)	→	if1#(false,0,x1)	(45)
        if1#(false,0,z1)	→	int#(s(0),z1)	(40)

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Instantiation Processor

        We instantiate the pair to the following set of pairs

        if_int#(true,false,0,s(z0))

        →

        if1#(false,0,s(z0))

        (51)

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Instantiation Processor

        We instantiate the pair to the following set of pairs

        if1#(false,0,s(z0))

        →

        int#(s(0),s(z0))

        (52)

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

        We instantiate the pair to the following set of pairs

        if_int#(false,false,s(s(y_0)),x2)	→	if2#(false,s(s(y_0)),x2)	(53)
        if_int#(false,false,s(0),s(s(y_0)))	→	if2#(false,s(0),s(s(y_0)))	(54)

        1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

        We consider all narrowings of the pair below position 2 to get the following set of pairs

        int#(s(y0),0)	→	if_int#(false,true,s(y0),0)	(55)
        int#(s(y0),s(x0))	→	if_int#(false,false,s(y0),s(x0))	(56)

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

          int#(s(y0),s(x0))	→	if_int#(false,false,s(y0),s(x0))	(56)
          if_int#(false,false,s(s(y_0)),x2)	→	if2#(false,s(s(y_0)),x2)	(53)
          if2#(false,s(s(x0)),y1)	→	int#(s(p(s(x0))),p(y1))	(43)
          if_int#(false,false,s(0),s(s(y_0)))	→	if2#(false,s(0),s(s(y_0)))	(54)
          if2#(false,s(0),s(s(x0)))	→	int#(0,s(p(s(x0))))	(50)
          int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)
          if_int#(true,false,0,s(z0))	→	if1#(false,0,s(z0))	(51)
          if1#(false,0,s(z0))	→	int#(s(0),s(z0))	(52)

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Usable Rules Processor

          We restrict the rewrite rules to the following usable rules of the DP problem.

          p(s(0))	→	0	(9)
          p(s(s(x)))	→	s(p(s(x)))	(10)
          p(0)	→	0	(8)

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor

          We restrict the innermost strategy to the following left hand sides.

          p(0)

          p(s(0))

          p(s(s(x0)))

          1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor

          We consider all narrowings of the pair below position 2 to get the following set of pairs

          if2#(false,s(s(y0)),s(0))	→	int#(s(p(s(y0))),0)	(57)
          if2#(false,s(s(y0)),s(s(x0)))	→	int#(s(p(s(y0))),s(p(s(x0))))	(58)
          if2#(false,s(s(y0)),0)	→	int#(s(p(s(y0))),0)	(59)

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

            if_int#(false,false,s(s(y_0)),x2)	→	if2#(false,s(s(y_0)),x2)	(53)
            if2#(false,s(s(y0)),s(s(x0)))	→	int#(s(p(s(y0))),s(p(s(x0))))	(58)
            int#(s(y0),s(x0))	→	if_int#(false,false,s(y0),s(x0))	(56)
            if_int#(false,false,s(0),s(s(y_0)))	→	if2#(false,s(0),s(s(y_0)))	(54)
            if2#(false,s(0),s(s(x0)))	→	int#(0,s(p(s(x0))))	(50)
            int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)
            if_int#(true,false,0,s(z0))	→	if1#(false,0,s(z0))	(51)
            if1#(false,0,s(z0))	→	int#(s(0),s(z0))	(52)

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Usable Rules Processor

            We restrict the rewrite rules to the following usable rules of the DP problem.

            p(s(0))	→	0	(9)
            p(s(s(x)))	→	s(p(s(x)))	(10)

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Instantiation Processor

            We instantiate the pair to the following set of pairs

            if_int#(false,false,s(s(x0)),s(z1))

            →

            if2#(false,s(s(x0)),s(z1))

            (60)

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

            We instantiate the pair to the following set of pairs

            int#(s(0),s(s(y_0)))	→	if_int#(false,false,s(0),s(s(y_0)))	(61)
            int#(s(s(y_0)),s(x1))	→	if_int#(false,false,s(s(y_0)),s(x1))	(62)

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

              int#(s(s(y_0)),s(x1))	→	if_int#(false,false,s(s(y_0)),s(x1))	(62)
              if_int#(false,false,s(s(x0)),s(z1))	→	if2#(false,s(s(x0)),s(z1))	(60)
              if2#(false,s(s(y0)),s(s(x0)))	→	int#(s(p(s(y0))),s(p(s(x0))))	(58)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

              Using the linear polynomial interpretation over the naturals

              [p(x1)]	=	1 · x1
              [s(x1)]	=	2 · x1
              [0]	=	2
              [int#(x1, x2)]	=	1 · x1 + 1 · x2
              [if_int#(x1,...,x4)]	=	2 · x1 + 2 · x2 + 1 · x3 + 1 · x4
              [false]	=	0
              [if2#(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3

              the rules

              empty(nil)	→	true	(1)
              empty(cons(x,y))	→	false	(2)
              tail(nil)	→	nil	(3)
              tail(cons(x,y))	→	y	(4)
              head(cons(x,y))	→	x	(5)
              zero(0)	→	true	(6)
              zero(s(x))	→	false	(7)
              p(0)	→	0	(8)
              p(s(0))	→	0	(9)
              intlist(x)	→	if_intlist(empty(x),x)	(11)
              if_intlist(true,x)	→	nil	(12)
              if_intlist(false,x)	→	cons(s(head(x)),intlist(tail(x)))	(13)
              int(x,y)	→	if_int(zero(x),zero(y),x,y)	(14)
              if_int(true,b,x,y)	→	if1(b,x,y)	(15)
              if_int(false,b,x,y)	→	if2(b,x,y)	(16)
              if1(true,x,y)	→	cons(0,nil)	(17)
              if1(false,x,y)	→	cons(0,int(s(0),y))	(18)
              if2(true,x,y)	→	nil	(19)
              if2(false,x,y)	→	intlist(int(p(x),p(y)))	(20)

              could be deleted.

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

              Using the linear polynomial interpretation over the naturals

              [int#(x1, x2)]	=	x1
              [s(x1)]	=	2 + 2 · x1
              [p(x1)]	=	-1 + x1
              [if_int#(x1,...,x4)]	=	2 · x1 + 2 · x2 + x3
              [false]	=	0
              [if2#(x1, x2, x3)]	=	2 · x1 + x2

              the pair

              if2#(false,s(s(y0)),s(s(x0)))

              →

              int#(s(p(s(y0))),s(p(s(x0))))

              (58)

              could be deleted.

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

              if2#(false,s(0),s(s(x0)))	→	int#(0,s(p(s(x0))))	(50)
              int#(0,s(x0))	→	if_int#(true,false,0,s(x0))	(47)
              if_int#(true,false,0,s(z0))	→	if1#(false,0,s(z0))	(51)
              if1#(false,0,s(z0))	→	int#(s(0),s(z0))	(52)
              int#(s(0),s(s(y_0)))	→	if_int#(false,false,s(0),s(s(y_0)))	(61)
              if_int#(false,false,s(0),s(s(y_0)))	→	if2#(false,s(0),s(s(y_0)))	(54)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 Forward Instantiation Processor

              We instantiate the pair to the following set of pairs

              if1#(false,0,s(s(y_0)))

              →

              int#(s(0),s(s(y_0)))

              (63)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 Reduction Pair Processor

              Using the linear polynomial interpretation over the naturals

              [int#(x1, x2)]	=	-2 + 2 · x2
              [s(x1)]	=	2 + 2 · x1
              [p(x1)]	=	-1 + x1
              [0]	=	1
              [if2#(x1, x2, x3)]	=	-2 + 2 · x1 + 2 · x3
              [false]	=	0
              [if_int#(x1,...,x4)]	=	-2 + 2 · x2 + 2 · x4
              [true]	=	2
              [if1#(x1, x2, x3)]	=	-2 + 2 · x1 + 2 · x3

              the pair

              if2#(false,s(0),s(s(x0)))

              →

              int#(0,s(p(s(x0))))

              (50)

              could be deleted.

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 Dependency Graph Processor

              The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  if_intlist#(false,x)	→	intlist#(tail(x))	(25)
  intlist#(x)	→	if_intlist#(empty(x),x)	(22)

  1.1.1.2 Usable Rules Processor

  We restrict the rewrite rules to the following usable rules of the DP problem.

  empty(nil)	→	true	(1)
  empty(cons(x,y))	→	false	(2)
  tail(nil)	→	nil	(3)
  tail(cons(x,y))	→	y	(4)

  1.1.1.2.1 Innermost Lhss Removal Processor

  We restrict the innermost strategy to the following left hand sides.

  empty(nil)

  empty(cons(x0,x1))

  tail(nil)

  tail(cons(x0,x1))

  1.1.1.2.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the rationals with delta = 3/16

  [if_intlist#(x1, x2)]	=	0 + 1/4 · x1 + 1 · x2
  [false]	=	1
  [intlist#(x1)]	=	1/4 + 2 · x1
  [tail(x1)]	=	0 + 1/2 · x1
  [empty(x1)]	=	1/4 + 2 · x1
  [nil]	=	0
  [cons(x1, x2)]	=	1 + 0 · x1 + 4 · x2
  [true]	=	1/4

  the pair

  intlist#(x)

  →

  if_intlist#(empty(x),x)

  (22)

  could be deleted.

  1.1.1.2.1.1.1 Usable Rules Processor

  We restrict the rewrite rules to the following usable rules of the DP problem.

  tail(nil)	→	nil	(3)
  tail(cons(x,y))	→	y	(4)

  1.1.1.2.1.1.1.1 Innermost Lhss Removal Processor

  We restrict the innermost strategy to the following left hand sides.

  tail(nil)

  tail(cons(x0,x1))

  1.1.1.2.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [tail(x1)]	=	1 · x1
  [nil]	=	0
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [if_intlist#(x1, x2)]	=	1 · x1 + 1 · x2
  [false]	=	0
  [intlist#(x1)]	=	1 · x1

  together with the usable rules

  tail(nil)	→	nil	(3)
  tail(cons(x,y))	→	y	(4)

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

  if_intlist#(false,x)

  →

  intlist#(tail(x))

  (25)

  and the rule

  tail(cons(x,y))

  →

  y

  (4)

  could be deleted.

  1.1.1.2.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  p#(s(s(x)))

  →

  p#(s(x))

  (21)

  1.1.1.3 Usable Rules Processor

  We restrict the rewrite rules to the following usable rules of the DP problem.

  There are no rules.

  1.1.1.3.1 Innermost Lhss Removal Processor

  We restrict the innermost strategy to the following left hand sides.

  There are no lhss.

  1.1.1.3.1.1 Size-Change Termination

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

  p#(s(s(x)))	→	p#(s(x))	(21)
  1	>	1

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