Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwcime1)

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

  1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(f(y_1,a),f(x1,a))

  →

  f#(a,f(y_1,a))

  (6)

  1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  f#(x0,f(f(y_1,a),a))	→	f#(f(a,x0),f(y_1,a))	(7)
  f#(a,f(f(y_1,a),a))	→	f#(f(a,a),f(y_1,a))	(8)

  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]	=	0
  [f(x1, x2)]	=	0
  [h(x1)]	=	1
  [f#(x1, x2)]	=	0

  We obtain the set of labeled pairs

  f#00(f00(y_1,a),f00(x1,a))	→	f#00(a,f00(y_1,a))	(9)
  f#00(x0,f00(f00(y_1,a),a))	→	f#00(f00(a,x0),f00(y_1,a))	(10)
  f#00(x0,f00(f10(y_1,a),a))	→	f#00(f00(a,x0),f10(y_1,a))	(11)
  f#10(x0,f00(f00(y_1,a),a))	→	f#00(f01(a,x0),f00(y_1,a))	(12)
  f#10(x0,f00(f10(y_1,a),a))	→	f#00(f01(a,x0),f10(y_1,a))	(13)
  f#00(f00(y_1,a),f10(x1,a))	→	f#00(a,f00(y_1,a))	(14)
  f#00(f10(y_1,a),f00(x1,a))	→	f#00(a,f10(y_1,a))	(15)
  f#00(f10(y_1,a),f10(x1,a))	→	f#00(a,f10(y_1,a))	(16)
  f#00(a,f00(f00(y_1,a),a))	→	f#00(f00(a,a),f00(y_1,a))	(17)
  f#00(a,f00(f10(y_1,a),a))	→	f#00(f00(a,a),f10(y_1,a))	(18)

  and the set of labeled rules:

  f00(x,f00(y,a))	→	f01(f00(f00(f00(a,x),y),a),h0(a))	(19)
  f00(x,f10(y,a))	→	f01(f00(f01(f00(a,x),y),a),h0(a))	(20)
  f10(x,f00(y,a))	→	f01(f00(f00(f01(a,x),y),a),h0(a))	(21)
  f10(x,f10(y,a))	→	f01(f00(f01(f01(a,x),y),a),h0(a))	(22)

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

  f00(x0,f00(x1,a))

  f00(x0,f10(x1,a))

  f10(x0,f00(x1,a))

  f10(x0,f10(x1,a))

  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#00(x0,f00(f00(y_1,a),a))	→	f#00(f00(a,x0),f00(y_1,a))	(10)
    f#00(f00(y_1,a),f00(x1,a))	→	f#00(a,f00(y_1,a))	(9)
    f#00(x0,f00(f10(y_1,a),a))	→	f#00(f00(a,x0),f10(y_1,a))	(11)
    f#00(f00(y_1,a),f10(x1,a))	→	f#00(a,f00(y_1,a))	(14)
    f#00(a,f00(f00(y_1,a),a))	→	f#00(f00(a,a),f00(y_1,a))	(17)
    f#00(a,f00(f10(y_1,a),a))	→	f#00(f00(a,a),f10(y_1,a))	(18)

    1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

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

    together with the usable rules

    f00(x,f00(y,a))	→	f01(f00(f00(f00(a,x),y),a),h0(a))	(19)
    f00(x,f10(y,a))	→	f01(f00(f01(f00(a,x),y),a),h0(a))	(20)

    (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

    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
    [a]	=	0
    [f01(x1, x2)]	=	1 · x1 + 1 · x2
    [h0(x1)]	=	1 · x1
    [f10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f#00(x1, x2)]	=	1 · x1 + 1 · x2

    the pair

    f#00(f00(y_1,a),f10(x1,a))

    →

    f#00(a,f00(y_1,a))

    (14)

    and the rule

    f00(x,f10(y,a))

    →

    f01(f00(f01(f00(a,x),y),a),h0(a))

    (20)

    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

      f#00(f00(y_1,a),f00(x1,a))	→	f#00(a,f00(y_1,a))	(9)
      f#00(x0,f00(f00(y_1,a),a))	→	f#00(f00(a,x0),f00(y_1,a))	(10)
      f#00(a,f00(f00(y_1,a),a))	→	f#00(f00(a,a),f00(y_1,a))	(17)

      1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

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

      the pair

      f#00(f00(y_1,a),f00(x1,a))

      →

      f#00(a,f00(y_1,a))

      (9)

      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

        f#00(x0,f00(f00(y_1,a),a))

        →

        f#00(f00(a,x0),f00(y_1,a))

        (10)

        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 naturals

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

        having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

        f#00(x0,f00(f00(y_1,a),a))

        →

        f#00(f00(a,x0),f00(y_1,a))

        (10)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

        There are no pairs anymore.