Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwaprove1)

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#(x,f(y,a))	→	f#(h(x),y)	(4)
  f#(x,f(y,a))	→	f#(a,f(h(x),y))	(3)

  1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(h(z0),f(x1,a))	→	f#(h(h(z0)),x1)	(5)
  f#(a,f(x1,a))	→	f#(h(a),x1)	(6)

  1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(a,f(x1,a))	→	f#(a,f(h(a),x1))	(7)
  f#(h(h(z0)),f(x1,a))	→	f#(a,f(h(h(h(z0))),x1))	(8)
  f#(h(a),f(x1,a))	→	f#(a,f(h(h(a)),x1))	(9)

  1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(h(h(z0)),f(x1,a))	→	f#(h(h(h(z0))),x1)	(10)
  f#(h(a),f(x1,a))	→	f#(h(h(a)),x1)	(11)

  1.1.1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(h(h(h(z0))),f(x1,a))	→	f#(a,f(h(h(h(h(z0)))),x1))	(12)
  f#(h(h(a)),f(x1,a))	→	f#(a,f(h(h(h(a))),x1))	(13)

  1.1.1.1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

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

  →

  f#(h(a),f(y_0,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#(h(h(x0)),f(f(y_1,a),a))

  →

  f#(h(h(h(x0))),f(y_1,a))

  (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#(h(a),f(f(y_0,a),a))	→	f#(h(h(a)),f(y_0,a))	(16)
  f#(h(a),f(f(f(y_1,a),a),a))	→	f#(h(h(a)),f(f(y_1,a),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#10(a,f01(x1,a))	→	f#10(a,f00(h1(a),x1))	(18)
  f#10(a,f11(x1,a))	→	f#10(a,f01(h1(a),x1))	(19)
  f#10(a,f01(f01(y_0,a),a))	→	f#00(h1(a),f01(y_0,a))	(20)
  f#10(a,f01(f11(y_0,a),a))	→	f#00(h1(a),f11(y_0,a))	(21)
  f#00(h1(a),f01(x1,a))	→	f#10(a,f00(h0(h1(a)),x1))	(22)
  f#00(h1(a),f11(x1,a))	→	f#10(a,f01(h0(h1(a)),x1))	(23)
  f#00(h0(h0(h0(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h0(z0)))),x1))	(24)
  f#00(h0(h0(h0(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h0(z0)))),x1))	(25)
  f#00(h0(h0(h1(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h1(z0)))),x1))	(26)
  f#00(h0(h0(h1(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h1(z0)))),x1))	(27)
  f#00(h0(h1(a)),f01(x1,a))	→	f#10(a,f00(h0(h0(h1(a))),x1))	(28)
  f#00(h0(h1(a)),f11(x1,a))	→	f#10(a,f01(h0(h0(h1(a))),x1))	(29)
  f#00(h1(a),f01(f01(y_0,a),a))	→	f#00(h0(h1(a)),f01(y_0,a))	(30)
  f#00(h1(a),f01(f11(y_0,a),a))	→	f#00(h0(h1(a)),f11(y_0,a))	(31)
  f#00(h1(a),f01(f01(f01(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f01(y_1,a),a))	(32)
  f#00(h1(a),f01(f01(f11(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f11(y_1,a),a))	(33)
  f#00(h0(h0(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f01(y_1,a))	(34)
  f#00(h0(h0(x0)),f01(f11(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f11(y_1,a))	(35)
  f#00(h0(h1(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f01(y_1,a))	(36)
  f#00(h0(h1(x0)),f01(f11(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f11(y_1,a))	(37)

  and the set of labeled rules:

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

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

  f00(x0,f01(x1,a))

  f00(x0,f11(x1,a))

  f10(x0,f01(x1,a))

  f10(x0,f11(x1,a))

  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#10(a,f01(x1,a))	→	f#10(a,f00(h1(a),x1))	(18)
    f#10(a,f01(f01(y_0,a),a))	→	f#00(h1(a),f01(y_0,a))	(20)
    f#00(h1(a),f01(x1,a))	→	f#10(a,f00(h0(h1(a)),x1))	(22)
    f#00(h1(a),f01(f01(y_0,a),a))	→	f#00(h0(h1(a)),f01(y_0,a))	(30)
    f#00(h0(h1(a)),f01(x1,a))	→	f#10(a,f00(h0(h0(h1(a))),x1))	(28)
    f#00(h0(h1(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f01(y_1,a))	(36)
    f#00(h0(h0(h1(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h1(z0)))),x1))	(26)
    f#00(h0(h0(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f01(y_1,a))	(34)
    f#00(h0(h0(h0(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h0(z0)))),x1))	(24)
    f#00(h0(h0(x0)),f01(f11(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f11(y_1,a))	(35)
    f#00(h0(h0(h0(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h0(z0)))),x1))	(25)
    f#00(h0(h1(x0)),f01(f11(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f11(y_1,a))	(37)
    f#00(h0(h0(h1(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h1(z0)))),x1))	(27)
    f#00(h1(a),f01(f11(y_0,a),a))	→	f#00(h0(h1(a)),f11(y_0,a))	(31)
    f#00(h0(h1(a)),f11(x1,a))	→	f#10(a,f01(h0(h0(h1(a))),x1))	(29)
    f#00(h1(a),f01(f01(f01(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f01(y_1,a),a))	(32)
    f#00(h1(a),f01(f01(f11(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f11(y_1,a),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
    [f01(x1, x2)]	=	1 · x1 + 1 · x2
    [a]	=	0
    [f10(x1, x2)]	=	1 · x1 + 1 · x2
    [h0(x1)]	=	1 · x1
    [f11(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [h1(x1)]	=	1 · x1
    [f#10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f#00(x1, x2)]	=	1 + 1 · x1 + 1 · x2

    the pairs

    f#00(h0(h0(h0(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h0(z0)))),x1))	(25)
    f#00(h0(h0(h1(z0))),f11(x1,a))	→	f#10(a,f01(h0(h0(h0(h1(z0)))),x1))	(27)
    f#00(h0(h1(a)),f11(x1,a))	→	f#10(a,f01(h0(h0(h1(a))),x1))	(29)

    and the rules

    f00(x,f11(y,a))	→	f01(f10(a,f01(h0(x),y)),a)	(39)
    f10(x,f11(y,a))	→	f01(f10(a,f01(h1(x),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#10(a,f01(x1,a))	→	f#10(a,f00(h1(a),x1))	(18)
      f#10(a,f01(f01(y_0,a),a))	→	f#00(h1(a),f01(y_0,a))	(20)
      f#00(h1(a),f01(x1,a))	→	f#10(a,f00(h0(h1(a)),x1))	(22)
      f#00(h1(a),f01(f01(y_0,a),a))	→	f#00(h0(h1(a)),f01(y_0,a))	(30)
      f#00(h0(h1(a)),f01(x1,a))	→	f#10(a,f00(h0(h0(h1(a))),x1))	(28)
      f#00(h0(h1(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f01(y_1,a))	(36)
      f#00(h0(h0(h1(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h1(z0)))),x1))	(26)
      f#00(h0(h0(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f01(y_1,a))	(34)
      f#00(h0(h0(h0(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h0(z0)))),x1))	(24)
      f#00(h1(a),f01(f01(f01(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f01(y_1,a),a))	(32)
      f#00(h1(a),f01(f01(f11(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f11(y_1,a),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
      [f01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [a]	=	0
      [f10(x1, x2)]	=	1 · x1 + 1 · x2
      [h0(x1)]	=	1 · x1
      [h1(x1)]	=	1 · x1
      [f#10(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#10(a,f01(x1,a))	→	f#10(a,f00(h1(a),x1))	(18)
      f#10(a,f01(f01(y_0,a),a))	→	f#00(h1(a),f01(y_0,a))	(20)
      f#00(h1(a),f01(x1,a))	→	f#10(a,f00(h0(h1(a)),x1))	(22)
      f#00(h1(a),f01(f01(y_0,a),a))	→	f#00(h0(h1(a)),f01(y_0,a))	(30)
      f#00(h0(h1(a)),f01(x1,a))	→	f#10(a,f00(h0(h0(h1(a))),x1))	(28)
      f#00(h0(h1(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h1(x0))),f01(y_1,a))	(36)
      f#00(h0(h0(h1(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h1(z0)))),x1))	(26)
      f#00(h0(h0(x0)),f01(f01(y_1,a),a))	→	f#00(h0(h0(h0(x0))),f01(y_1,a))	(34)
      f#00(h0(h0(h0(z0))),f01(x1,a))	→	f#10(a,f00(h0(h0(h0(h0(z0)))),x1))	(24)
      f#00(h1(a),f01(f01(f01(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f01(y_1,a),a))	(32)
      f#00(h1(a),f01(f01(f11(y_1,a),a),a))	→	f#00(h0(h1(a)),f01(f11(y_1,a),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.