Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z03)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  a#(f,a(g,a(f,x)))	→	a#(g,a(g,a(f,x)))	(6)
  a#(g,a(f,a(g,x)))	→	a#(g,a(f,a(f,a(g,x))))	(5)
  a#(f,a(g,a(f,x)))	→	a#(f,a(g,a(g,a(f,x))))	(4)
  a#(g,a(f,a(g,x)))	→	a#(f,a(f,a(g,x)))	(3)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [a(x1, x2)]	=	max(x1 + 1, 0)
  [f]	=	0
  [a#(x1, x2)]	=	max(x1 + 11293, x2 + 11294, 0)
  [g]	=	3

  together with the usable rules

  a(f,a(g,a(f,x)))	→	a(f,a(g,a(g,a(f,x))))	(1)
  a(g,a(f,a(g,x)))	→	a(g,a(f,a(f,a(g,x))))	(2)

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

  a#(g,a(f,a(g,x)))

  →

  a#(f,a(f,a(g,x)))

  (3)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    a#(f,a(g,a(f,x)))

    →

    a#(f,a(g,a(g,a(f,x))))

    (4)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

    [a(x1, x2)]	=	0 0 1 0 · x1 + 0 1 0 0 · x2 + 1 43730
    [f]	=	2 1
    [a#(x1, x2)]	=	1 1 0 1 · x2 + 0 0
    [g]	=	1 1

    together with the usable rules

    a(f,a(g,a(f,x)))	→	a(f,a(g,a(g,a(f,x))))	(1)
    a(g,a(f,a(g,x)))	→	a(g,a(f,a(f,a(g,x))))	(2)

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

    a#(f,a(g,a(f,x)))

    →

    a#(f,a(g,a(g,a(f,x))))

    (4)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 2^nd component contains the pair

    a#(g,a(f,a(g,x)))

    →

    a#(g,a(f,a(f,a(g,x))))

    (5)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

    [a(x1, x2)]	=	0 0 1 0 · x1 + 0 1 0 0 · x2 + 30808 0
    [f]	=	1 1
    [a#(x1, x2)]	=	1 1 0 1 · x2 + 0 0
    [g]	=	14023 1

    together with the usable rules

    a(f,a(g,a(f,x)))	→	a(f,a(g,a(g,a(f,x))))	(1)
    a(g,a(f,a(g,x)))	→	a(g,a(f,a(f,a(g,x))))	(2)

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

    a#(g,a(f,a(g,x)))

    →

    a#(g,a(f,a(f,a(g,x))))

    (5)

    could be deleted.

    1.1.1.1.2.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.