Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwaprove2)

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

• The 1^st component contains the pair

  f#(f(a,x),y)	→	f#(x,h(y))	(4)
  f#(f(a,x),y)	→	f#(f(x,h(y)),a)	(3)

  1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,x0),h(z1))	→	f#(x0,h(h(z1)))	(5)
  f#(f(a,x0),a)	→	f#(x0,h(a))	(6)

  1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,x0),a)	→	f#(f(x0,h(a)),a)	(7)
  f#(f(a,x0),h(h(z1)))	→	f#(f(x0,h(h(h(z1)))),a)	(8)
  f#(f(a,x0),h(a))	→	f#(f(x0,h(h(a))),a)	(9)

  1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,x0),h(h(z1)))	→	f#(x0,h(h(h(z1))))	(10)
  f#(f(a,x0),h(a))	→	f#(x0,h(h(a)))	(11)

  1.1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,x0),h(h(h(z1))))	→	f#(f(x0,h(h(h(h(z1))))),a)	(12)
  f#(f(a,x0),h(h(a)))	→	f#(f(x0,h(h(h(a)))),a)	(13)

  1.1.1.1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,f(a,y_0)),a)

  →

  f#(f(a,y_0),h(a))

  (14)

  1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,f(a,y_0)),h(h(x1)))

  →

  f#(f(a,y_0),h(h(h(x1))))

  (15)

  1.1.1.1.1.1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(a,f(a,y_0)),h(a))	→	f#(f(a,y_0),h(h(a)))	(16)
  f#(f(a,f(a,f(a,y_0))),h(a))	→	f#(f(a,f(a,y_0)),h(h(a)))	(17)

  1.1.1.1.1.1.1.1.1.1.1 Semantic Labeling Processor

  The following interpretations form a model of the rules.

  As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

  [a]	=	1
  [f(x1, x2)]	=	0
  [h(x1)]	=	0
  [f#(x1, x2)]	=	0

  We obtain the set of labeled pairs

  f#01(f10(a,x0),a)	→	f#01(f00(x0,h1(a)),a)	(18)
  f#01(f11(a,x0),a)	→	f#01(f10(x0,h1(a)),a)	(19)
  f#01(f10(a,f10(a,y_0)),a)	→	f#00(f10(a,y_0),h1(a))	(20)
  f#01(f10(a,f11(a,y_0)),a)	→	f#00(f11(a,y_0),h1(a))	(21)
  f#00(f10(a,x0),h1(a))	→	f#01(f00(x0,h0(h1(a))),a)	(22)
  f#00(f11(a,x0),h1(a))	→	f#01(f10(x0,h0(h1(a))),a)	(23)
  f#00(f10(a,x0),h0(h0(h0(z1))))	→	f#01(f00(x0,h0(h0(h0(h0(z1))))),a)	(24)
  f#00(f10(a,x0),h0(h0(h1(z1))))	→	f#01(f00(x0,h0(h0(h0(h1(z1))))),a)	(25)
  f#00(f11(a,x0),h0(h0(h0(z1))))	→	f#01(f10(x0,h0(h0(h0(h0(z1))))),a)	(26)
  f#00(f11(a,x0),h0(h0(h1(z1))))	→	f#01(f10(x0,h0(h0(h0(h1(z1))))),a)	(27)
  f#00(f10(a,x0),h0(h1(a)))	→	f#01(f00(x0,h0(h0(h1(a)))),a)	(28)
  f#00(f11(a,x0),h0(h1(a)))	→	f#01(f10(x0,h0(h0(h1(a)))),a)	(29)
  f#00(f10(a,f10(a,y_0)),h1(a))	→	f#00(f10(a,y_0),h0(h1(a)))	(30)
  f#00(f10(a,f11(a,y_0)),h1(a))	→	f#00(f11(a,y_0),h0(h1(a)))	(31)
  f#00(f10(a,f10(a,f10(a,y_0))),h1(a))	→	f#00(f10(a,f10(a,y_0)),h0(h1(a)))	(32)
  f#00(f10(a,f10(a,f11(a,y_0))),h1(a))	→	f#00(f10(a,f11(a,y_0)),h0(h1(a)))	(33)
  f#00(f10(a,f10(a,y_0)),h0(h0(x1)))	→	f#00(f10(a,y_0),h0(h0(h0(x1))))	(34)
  f#00(f10(a,f10(a,y_0)),h0(h1(x1)))	→	f#00(f10(a,y_0),h0(h0(h1(x1))))	(35)
  f#00(f10(a,f11(a,y_0)),h0(h0(x1)))	→	f#00(f11(a,y_0),h0(h0(h0(x1))))	(36)
  f#00(f10(a,f11(a,y_0)),h0(h1(x1)))	→	f#00(f11(a,y_0),h0(h0(h1(x1))))	(37)

  and the set of labeled rules:

  f00(f10(a,x),y)	→	f10(a,f01(f00(x,h0(y)),a))	(38)
  f01(f10(a,x),y)	→	f10(a,f01(f00(x,h1(y)),a))	(39)
  f00(f11(a,x),y)	→	f10(a,f01(f10(x,h0(y)),a))	(40)
  f01(f11(a,x),y)	→	f10(a,f01(f10(x,h1(y)),a))	(41)

  Innermost rewriting w.r.t. the following left-hand sides is considered:

  f00(f10(a,x0),x1)

  f01(f10(a,x0),x1)

  f00(f11(a,x0),x1)

  f01(f11(a,x0),x1)

  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

    f#01(f10(a,x0),a)	→	f#01(f00(x0,h1(a)),a)	(18)
    f#01(f10(a,f10(a,y_0)),a)	→	f#00(f10(a,y_0),h1(a))	(20)
    f#00(f10(a,x0),h1(a))	→	f#01(f00(x0,h0(h1(a))),a)	(22)
    f#00(f10(a,f10(a,y_0)),h1(a))	→	f#00(f10(a,y_0),h0(h1(a)))	(30)
    f#00(f10(a,x0),h0(h1(a)))	→	f#01(f00(x0,h0(h0(h1(a)))),a)	(28)
    f#00(f10(a,f10(a,y_0)),h0(h1(x1)))	→	f#00(f10(a,y_0),h0(h0(h1(x1))))	(35)
    f#00(f10(a,x0),h0(h0(h1(z1))))	→	f#01(f00(x0,h0(h0(h0(h1(z1))))),a)	(25)
    f#00(f10(a,f10(a,y_0)),h0(h0(x1)))	→	f#00(f10(a,y_0),h0(h0(h0(x1))))	(34)
    f#00(f10(a,x0),h0(h0(h0(z1))))	→	f#01(f00(x0,h0(h0(h0(h0(z1))))),a)	(24)
    f#00(f10(a,f11(a,y_0)),h0(h0(x1)))	→	f#00(f11(a,y_0),h0(h0(h0(x1))))	(36)
    f#00(f11(a,x0),h0(h0(h0(z1))))	→	f#01(f10(x0,h0(h0(h0(h0(z1))))),a)	(26)
    f#00(f10(a,f11(a,y_0)),h0(h1(x1)))	→	f#00(f11(a,y_0),h0(h0(h1(x1))))	(37)
    f#00(f11(a,x0),h0(h0(h1(z1))))	→	f#01(f10(x0,h0(h0(h0(h1(z1))))),a)	(27)
    f#00(f10(a,f11(a,y_0)),h1(a))	→	f#00(f11(a,y_0),h0(h1(a)))	(31)
    f#00(f11(a,x0),h0(h1(a)))	→	f#01(f10(x0,h0(h0(h1(a)))),a)	(29)
    f#00(f10(a,f10(a,f10(a,y_0))),h1(a))	→	f#00(f10(a,f10(a,y_0)),h0(h1(a)))	(32)
    f#00(f10(a,f10(a,f11(a,y_0))),h1(a))	→	f#00(f10(a,f11(a,y_0)),h0(h1(a)))	(33)

    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

    [f00(x1, x2)]	=	1 · x1 + 1 · x2
    [f10(x1, x2)]	=	1 · x1 + 1 · x2
    [a]	=	0
    [f01(x1, x2)]	=	1 · x1 + 1 · x2
    [h0(x1)]	=	1 · x1
    [h1(x1)]	=	1 · x1
    [f11(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f#01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f#00(x1, x2)]	=	1 + 1 · x1 + 1 · x2

    the pairs

    f#00(f11(a,x0),h0(h0(h0(z1))))	→	f#01(f10(x0,h0(h0(h0(h0(z1))))),a)	(26)
    f#00(f11(a,x0),h0(h0(h1(z1))))	→	f#01(f10(x0,h0(h0(h0(h1(z1))))),a)	(27)
    f#00(f11(a,x0),h0(h1(a)))	→	f#01(f10(x0,h0(h0(h1(a)))),a)	(29)

    and the rules

    f00(f11(a,x),y)	→	f10(a,f01(f10(x,h0(y)),a))	(40)
    f01(f11(a,x),y)	→	f10(a,f01(f10(x,h1(y)),a))	(41)

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

    • The 1^st component contains the pair

      f#01(f10(a,x0),a)	→	f#01(f00(x0,h1(a)),a)	(18)
      f#01(f10(a,f10(a,y_0)),a)	→	f#00(f10(a,y_0),h1(a))	(20)
      f#00(f10(a,x0),h1(a))	→	f#01(f00(x0,h0(h1(a))),a)	(22)
      f#00(f10(a,f10(a,y_0)),h1(a))	→	f#00(f10(a,y_0),h0(h1(a)))	(30)
      f#00(f10(a,x0),h0(h1(a)))	→	f#01(f00(x0,h0(h0(h1(a)))),a)	(28)
      f#00(f10(a,f10(a,y_0)),h0(h1(x1)))	→	f#00(f10(a,y_0),h0(h0(h1(x1))))	(35)
      f#00(f10(a,x0),h0(h0(h1(z1))))	→	f#01(f00(x0,h0(h0(h0(h1(z1))))),a)	(25)
      f#00(f10(a,f10(a,y_0)),h0(h0(x1)))	→	f#00(f10(a,y_0),h0(h0(h0(x1))))	(34)
      f#00(f10(a,x0),h0(h0(h0(z1))))	→	f#01(f00(x0,h0(h0(h0(h0(z1))))),a)	(24)
      f#00(f10(a,f10(a,f10(a,y_0))),h1(a))	→	f#00(f10(a,f10(a,y_0)),h0(h1(a)))	(32)
      f#00(f10(a,f10(a,f11(a,y_0))),h1(a))	→	f#00(f10(a,f11(a,y_0)),h0(h1(a)))	(33)

      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

      [f00(x1, x2)]	=	1 · x1 + 1 · x2
      [f10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [a]	=	0
      [f01(x1, x2)]	=	1 · x1 + 1 · x2
      [h0(x1)]	=	1 · x1
      [h1(x1)]	=	1 · x1
      [f#01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [f#00(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [f11(x1, x2)]	=	1 · x1 + 1 · x2

      the pairs

      f#01(f10(a,x0),a)	→	f#01(f00(x0,h1(a)),a)	(18)
      f#01(f10(a,f10(a,y_0)),a)	→	f#00(f10(a,y_0),h1(a))	(20)
      f#00(f10(a,x0),h1(a))	→	f#01(f00(x0,h0(h1(a))),a)	(22)
      f#00(f10(a,f10(a,y_0)),h1(a))	→	f#00(f10(a,y_0),h0(h1(a)))	(30)
      f#00(f10(a,x0),h0(h1(a)))	→	f#01(f00(x0,h0(h0(h1(a)))),a)	(28)
      f#00(f10(a,f10(a,y_0)),h0(h1(x1)))	→	f#00(f10(a,y_0),h0(h0(h1(x1))))	(35)
      f#00(f10(a,x0),h0(h0(h1(z1))))	→	f#01(f00(x0,h0(h0(h0(h1(z1))))),a)	(25)
      f#00(f10(a,f10(a,y_0)),h0(h0(x1)))	→	f#00(f10(a,y_0),h0(h0(h0(x1))))	(34)
      f#00(f10(a,x0),h0(h0(h0(z1))))	→	f#01(f00(x0,h0(h0(h0(h0(z1))))),a)	(24)
      f#00(f10(a,f10(a,f10(a,y_0))),h1(a))	→	f#00(f10(a,f10(a,y_0)),h0(h1(a)))	(32)
      f#00(f10(a,f10(a,f11(a,y_0))),h1(a))	→	f#00(f10(a,f11(a,y_0)),h0(h1(a)))	(33)

      and no rules could be deleted.

      1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

      There are no pairs anymore.