Certification Problem

Input (TPDB TRS_Standard/Endrullis_06/quadruple2)

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

  p#(p(b(a(x0)),x1),p(x2,x3))	→	p#(x3,x0)	(4)
  p#(p(b(a(x0)),x1),p(x2,x3))	→	p#(p(b(x2),a(a(b(x1)))),p(x3,x0))	(2)

  1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [p(x1, x2)]	=	1 + 2 · x1 + 2 · x2
  [b(x1)]	=	1 · x1
  [a(x1)]	=	1 · x1
  [p#(x1, x2)]	=	2 · x1 + 2 · x2

  the pair

  p#(p(b(a(x0)),x1),p(x2,x3))

  →

  p#(x3,x0)

  (4)

  and no rules could be deleted.

  1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  p#(p(b(a(x0)),a(a(b(y_1)))),p(x2,x3))

  →

  p#(p(b(x2),a(a(b(a(a(b(y_1))))))),p(x3,x0))

  (5)

  1.1.1.1.1 Instantiation Processor

  We instantiate the pair to the following set of pairs

  p#(p(b(a(x0)),a(a(b(a(a(b(y_1))))))),p(x2,x3))

  →

  p#(p(b(x2),a(a(b(a(a(b(a(a(b(y_1)))))))))),p(x3,x0))

  (6)

  1.1.1.1.1.1 Forward Instantiation Processor

  We instantiate the pair to the following set of pairs

  p#(p(b(a(x0)),a(a(b(a(a(b(x1))))))),p(a(y_0),x3))

  →

  p#(p(b(a(y_0)),a(a(b(a(a(b(a(a(b(x1)))))))))),p(x3,x0))

  (7)

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

  We obtain the set of labeled pairs

  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p10(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p00(x3,x0))	(8)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p11(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p10(x3,x0))	(9)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p10(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p00(x3,x0))	(10)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p11(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p10(x3,x0))	(11)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p10(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p00(x3,x0))	(12)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p10(x3,x0))	(13)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p10(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p00(x3,x0))	(14)
  p#00(p01(b1(a0(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p10(x3,x0))	(15)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p10(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p01(x3,x0))	(16)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p11(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p11(x3,x0))	(17)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p10(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p01(x3,x0))	(18)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b0(x1))))))),p11(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b0(x1)))))))))),p11(x3,x0))	(19)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p10(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p01(x3,x0))	(20)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a0(y_0),x3))	→	p#00(p01(b1(a0(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p11(x3,x0))	(21)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p10(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p01(x3,x0))	(22)
  p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a1(y_0),x3))	→	p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p11(x3,x0))	(23)

  and the set of labeled rules:

  p00(p00(b1(a0(x0)),x1),p00(x2,x3))	→	p00(p01(b0(x2),a1(a0(b0(x1)))),p00(x3,x0))	(24)
  p00(p00(b1(a0(x0)),x1),p01(x2,x3))	→	p00(p01(b0(x2),a1(a0(b0(x1)))),p10(x3,x0))	(25)
  p00(p00(b1(a0(x0)),x1),p10(x2,x3))	→	p00(p01(b1(x2),a1(a0(b0(x1)))),p00(x3,x0))	(26)
  p00(p00(b1(a0(x0)),x1),p11(x2,x3))	→	p00(p01(b1(x2),a1(a0(b0(x1)))),p10(x3,x0))	(27)
  p00(p01(b1(a0(x0)),x1),p00(x2,x3))	→	p00(p01(b0(x2),a1(a0(b1(x1)))),p00(x3,x0))	(28)
  p00(p01(b1(a0(x0)),x1),p01(x2,x3))	→	p00(p01(b0(x2),a1(a0(b1(x1)))),p10(x3,x0))	(29)
  p00(p01(b1(a0(x0)),x1),p10(x2,x3))	→	p00(p01(b1(x2),a1(a0(b1(x1)))),p00(x3,x0))	(30)
  p00(p01(b1(a0(x0)),x1),p11(x2,x3))	→	p00(p01(b1(x2),a1(a0(b1(x1)))),p10(x3,x0))	(31)
  p00(p00(b1(a1(x0)),x1),p00(x2,x3))	→	p00(p01(b0(x2),a1(a0(b0(x1)))),p01(x3,x0))	(32)
  p00(p00(b1(a1(x0)),x1),p01(x2,x3))	→	p00(p01(b0(x2),a1(a0(b0(x1)))),p11(x3,x0))	(33)
  p00(p00(b1(a1(x0)),x1),p10(x2,x3))	→	p00(p01(b1(x2),a1(a0(b0(x1)))),p01(x3,x0))	(34)
  p00(p00(b1(a1(x0)),x1),p11(x2,x3))	→	p00(p01(b1(x2),a1(a0(b0(x1)))),p11(x3,x0))	(35)
  p00(p01(b1(a1(x0)),x1),p00(x2,x3))	→	p00(p01(b0(x2),a1(a0(b1(x1)))),p01(x3,x0))	(36)
  p00(p01(b1(a1(x0)),x1),p01(x2,x3))	→	p00(p01(b0(x2),a1(a0(b1(x1)))),p11(x3,x0))	(37)
  p00(p01(b1(a1(x0)),x1),p10(x2,x3))	→	p00(p01(b1(x2),a1(a0(b1(x1)))),p01(x3,x0))	(38)
  p00(p01(b1(a1(x0)),x1),p11(x2,x3))	→	p00(p01(b1(x2),a1(a0(b1(x1)))),p11(x3,x0))	(39)

  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

    p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a1(y_0),x3))

    →

    p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p11(x3,x0))

    (23)

    1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [p#00(x1, x2)]	=	1 · x1 + 1 · x2
    [p01(x1, x2)]	=	1 · x1 + 1 · x2
    [b1(x1)]	=	1 · x1
    [a1(x1)]	=	1 · x1
    [a0(x1)]	=	1 · x1
    [p11(x1, x2)]	=	1 · x1 + 1 · x2

    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 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [p#00(x1, x2)]	=	1 · x1 + 1 · x2
    [p01(x1, x2)]	=	1 · x1 + 1 · x2
    [b1(x1)]	=	1 + 1 · x1
    [a1(x1)]	=	1 + 1 · x1
    [a0(x1)]	=	1
    [p11(x1, x2)]	=	1 · x1 + 1 · x2

    the pair

    p#00(p01(b1(a1(x0)),a1(a0(b1(a1(a0(b1(x1))))))),p11(a1(y_0),x3))

    →

    p#00(p01(b1(a1(y_0)),a1(a0(b1(a1(a0(b1(a1(a0(b1(x1)))))))))),p11(x3,x0))

    (23)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.