Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z02)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ 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#(x,g)	→	a#(f,a(g,a(f,x)))	(4)
  a#(f,a(f,x))	→	a#(x,g)	(3)
  a#(x,g)	→	a#(f,x)	(6)

  1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 2 to get the following set of pairs

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

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    a#(x,g)	→	a#(f,x)	(6)
    a#(f,a(f,x))	→	a#(x,g)	(3)
    a#(a(f,x0),g)	→	a#(f,a(g,a(x0,g)))	(7)

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

    We obtain the set of labeled pairs

    a#01(x,g)	→	a#00(f,x)	(9)
    a#00(f,a00(f,x))	→	a#01(x,g)	(10)
    a#00(f,a01(f,x))	→	a#11(x,g)	(11)
    a#11(x,g)	→	a#01(f,x)	(12)
    a#01(a00(f,x0),g)	→	a#00(f,a10(g,a01(x0,g)))	(13)
    a#01(a01(f,x0),g)	→	a#00(f,a10(g,a11(x0,g)))	(14)

    and the set of labeled rules:

    a00(f,a00(f,x))	→	a01(x,g)	(15)
    a00(f,a01(f,x))	→	a11(x,g)	(16)
    a01(x,g)	→	a00(f,a10(g,a00(f,x)))	(17)
    a11(x,g)	→	a00(f,a10(g,a01(f,x)))	(18)

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      a#00(f,a00(f,x))	→	a#01(x,g)	(10)
      a#01(x,g)	→	a#00(f,x)	(9)
      a#00(f,a01(f,x))	→	a#11(x,g)	(11)
      a#11(x,g)	→	a#01(f,x)	(12)

      1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the naturals

      [a#00(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [f]	=	1
      [a00(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [a#01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [g]	=	1
      [a01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
      [a#11(x1, x2)]	=	1 + 1 · x1 + 1 · x2

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

      a#00(f,a00(f,x))	→	a#01(x,g)	(10)
      a#00(f,a01(f,x))	→	a#11(x,g)	(11)

      and no rules could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.