Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwtpa1)

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

  1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

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

  →

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

  (6)

  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#00(f10(a,x),y)	→	f#00(y,f00(x,f10(a,f01(h1(a),a))))	(7)
  f#01(f10(a,x),y)	→	f#10(y,f00(x,f10(a,f01(h1(a),a))))	(8)
  f#00(f11(a,x),y)	→	f#00(y,f10(x,f10(a,f01(h1(a),a))))	(9)
  f#01(f11(a,x),y)	→	f#10(y,f10(x,f10(a,f01(h1(a),a))))	(10)
  f#00(f10(a,f10(a,y_0)),x1)	→	f#00(f10(a,y_0),f10(a,f01(h1(a),a)))	(11)
  f#01(f10(a,f10(a,y_0)),x1)	→	f#00(f10(a,y_0),f10(a,f01(h1(a),a)))	(12)
  f#00(f10(a,f11(a,y_0)),x1)	→	f#00(f11(a,y_0),f10(a,f01(h1(a),a)))	(13)
  f#01(f10(a,f11(a,y_0)),x1)	→	f#00(f11(a,y_0),f10(a,f01(h1(a),a)))	(14)

  and the set of labeled rules:

  f00(f10(a,x),y)	→	f00(y,f00(x,f10(a,f01(h1(a),a))))	(15)
  f01(f10(a,x),y)	→	f10(y,f00(x,f10(a,f01(h1(a),a))))	(16)
  f00(f11(a,x),y)	→	f00(y,f10(x,f10(a,f01(h1(a),a))))	(17)
  f01(f11(a,x),y)	→	f10(y,f10(x,f10(a,f01(h1(a),a))))	(18)

  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 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    f#00(f10(a,x),y)	→	f#00(y,f00(x,f10(a,f01(h1(a),a))))	(7)
    f#00(f11(a,x),y)	→	f#00(y,f10(x,f10(a,f01(h1(a),a))))	(9)
    f#00(f10(a,f10(a,y_0)),x1)	→	f#00(f10(a,y_0),f10(a,f01(h1(a),a)))	(11)
    f#00(f10(a,f11(a,y_0)),x1)	→	f#00(f11(a,y_0),f10(a,f01(h1(a),a)))	(13)

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

    together with the usable rules

    f00(f11(a,x),y)	→	f00(y,f10(x,f10(a,f01(h1(a),a))))	(17)
    f00(f10(a,x),y)	→	f00(y,f00(x,f10(a,f01(h1(a),a))))	(15)

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

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

    the pair

    f#00(f11(a,x),y)

    →

    f#00(y,f10(x,f10(a,f01(h1(a),a))))

    (9)

    and the rule

    f00(f11(a,x),y)

    →

    f00(y,f10(x,f10(a,f01(h1(a),a))))

    (17)

    could be deleted.

    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(f10(a,x),y)	→	f#00(y,f00(x,f10(a,f01(h1(a),a))))	(7)
      f#00(f10(a,f10(a,y_0)),x1)	→	f#00(f10(a,y_0),f10(a,f01(h1(a),a)))	(11)

      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
      [f10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [a]	=	1
      [f00(x1, x2)]	=	1
      [f01(x1, x2)]	=	0
      [h1(x1)]	=	0

      the pair

      f#00(f10(a,x),y)

      →

      f#00(y,f00(x,f10(a,f01(h1(a),a))))

      (7)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

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

      having no usable rules (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.1.1.1 Reduction Pair Processor

      Using the linear polynomial interpretation over the naturals

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

      the pair

      f#00(f10(a,f10(a,y_0)),x1)

      →

      f#00(f10(a,y_0),f10(a,f01(h1(a),a)))

      (11)

      could be deleted.

      1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

      There are no pairs anymore.