Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/turing_add)

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

  1#(q0(1(x1)))	→	0#(1(q1(x1)))	(17)
  1#(q0(0(x1)))	→	0#(0(q1(x1)))	(16)
  1#(q2(x1))	→	1#(x1)	(15)
  1#(q1(0(x1)))	→	0#(q1(x1))	(11)
  1#(q0(1(x1)))	→	1#(q1(x1))	(10)
  1#(q1(1(x1)))	→	1#(1(q1(x1)))	(9)
  0#(q1(x1))	→	1#(x1)	(14)
  1#(q1(0(x1)))	→	1#(0(q1(x1)))	(13)
  1#(q1(1(x1)))	→	1#(q1(x1))	(12)
  1#(q0(0(x1)))	→	0#(q1(x1))	(8)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [0#(x1)]	=	x1 + 26958
  [1(x1)]	=	x1 + 1
  [0(x1)]	=	x1 + 26960
  [q1(x1)]	=	x1 + 1143
  [q2(x1)]	=	x1 + 28102
  [1#(x1)]	=	x1 + 0
  [q0(x1)]	=	x1 + 28102

  together with the usable rules

  1(q1(0(x1)))	→	1(0(q1(x1)))	(4)
  1(q0(1(x1)))	→	0(1(q1(x1)))	(1)
  1(q1(1(x1)))	→	1(1(q1(x1)))	(3)
  0(q1(x1))	→	q2(1(x1))	(5)
  0(q2(x1))	→	0(q0(x1))	(7)
  1(q2(x1))	→	q2(1(x1))	(6)
  1(q0(0(x1)))	→	0(0(q1(x1)))	(2)

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

  1#(q0(1(x1)))	→	0#(1(q1(x1)))	(17)
  1#(q0(0(x1)))	→	0#(0(q1(x1)))	(16)
  1#(q2(x1))	→	1#(x1)	(15)
  1#(q1(0(x1)))	→	0#(q1(x1))	(11)
  1#(q0(1(x1)))	→	1#(q1(x1))	(10)
  0#(q1(x1))	→	1#(x1)	(14)
  1#(q1(1(x1)))	→	1#(q1(x1))	(12)
  1#(q0(0(x1)))	→	0#(q1(x1))	(8)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    1#(q1(0(x1)))	→	1#(0(q1(x1)))	(13)
    1#(q1(1(x1)))	→	1#(1(q1(x1)))	(9)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [0#(x1)]	=	x1 + 26958
    [1(x1)]	=	x1 + 1
    [0(x1)]	=	2998
    [q1(x1)]	=	x1 + 8946
    [q2(x1)]	=	2998
    [1#(x1)]	=	x1 + 0
    [q0(x1)]	=	26286

    together with the usable rules

    1(q1(0(x1)))	→	1(0(q1(x1)))	(4)
    1(q0(1(x1)))	→	0(1(q1(x1)))	(1)
    1(q1(1(x1)))	→	1(1(q1(x1)))	(3)
    0(q1(x1))	→	q2(1(x1))	(5)
    0(q2(x1))	→	0(q0(x1))	(7)
    1(q2(x1))	→	q2(1(x1))	(6)
    1(q0(0(x1)))	→	0(0(q1(x1)))	(2)

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

    1#(q1(0(x1)))

    →

    1#(0(q1(x1)))

    (13)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      1#(q1(1(x1)))

      →

      1#(1(q1(x1)))

      (9)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [0#(x1)]	=	x1 + 26958
      [1(x1)]	=	8006
      [0(x1)]	=	8006
      [q1(x1)]	=	x1 + 3938
      [q2(x1)]	=	8006
      [1#(x1)]	=	x1 + 0
      [q0(x1)]	=	26286

      together with the usable rules

      1(q1(0(x1)))	→	1(0(q1(x1)))	(4)
      1(q0(1(x1)))	→	0(1(q1(x1)))	(1)
      1(q1(1(x1)))	→	1(1(q1(x1)))	(3)
      0(q1(x1))	→	q2(1(x1))	(5)
      0(q2(x1))	→	0(q0(x1))	(7)
      1(q2(x1))	→	q2(1(x1))	(6)
      1(q0(0(x1)))	→	0(0(q1(x1)))	(2)

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

      1#(q1(1(x1)))

      →

      1#(1(q1(x1)))

      (9)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 0 components.