Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_2_Luc02c_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Reduction Pair Processor

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  mark#(2nd(X))	→	mark#(X)	(12)
  mark#(from(X))	→	a__from#(mark(X))	(13)
  a__from#(X)	→	mark#(X)	(10)
  mark#(from(X))	→	mark#(X)	(14)
  mark#(cons(X1,X2))	→	mark#(X1)	(15)
  mark#(s(X))	→	mark#(X)	(16)

  1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

  [mark#(x1)]	=	1 + 1 · x1
  [2nd(x1)]	=	1 + 1 · x1
  [from(x1)]	=	-∞ + 0 · x1
  [a__from#(x1)]	=	1 + 1 · x1
  [mark(x1)]	=	0 + 0 · x1
  [cons(x1, x2)]	=	-∞ + 0 · x1 + 0 · x2
  [s(x1)]	=	-∞ + 0 · x1
  [a__2nd(x1)]	=	1 + 1 · x1
  [a__from(x1)]	=	0 + 0 · x1

  the pair

  mark#(2nd(X))

  →

  mark#(X)

  (12)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

  [mark#(x1)]	=	0 + 0 · x1
  [from(x1)]	=	1 + 1 · x1
  [a__from#(x1)]	=	0 + 1 · x1
  [mark(x1)]	=	0 + 0 · x1
  [cons(x1, x2)]	=	-∞ + 0 · x1 + 0 · x2
  [s(x1)]	=	-∞ + 0 · x1
  [2nd(x1)]	=	1 + 1 · x1
  [a__2nd(x1)]	=	1 + 1 · x1
  [a__from(x1)]	=	1 + 1 · x1

  the pair

  mark#(from(X))

  →

  mark#(X)

  (14)

  could be deleted.

  1.1.1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

  [mark#(x1)]	=	-∞ + 1 · x1
  [from(x1)]	=	-∞ + 1 · x1
  [a__from#(x1)]	=	-∞ + 1 · x1
  [mark(x1)]	=	-∞ + 0 · x1
  [cons(x1, x2)]	=	-∞ + 0 · x1 + 0 · x2
  [s(x1)]	=	-∞ + 0 · x1
  [2nd(x1)]	=	0 + 0 · x1
  [a__2nd(x1)]	=	0 + 0 · x1
  [a__from(x1)]	=	-∞ + 1 · x1

  the pair

  mark#(from(X))

  →

  a__from#(mark(X))

  (13)

  could be deleted.

  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

    mark#(s(X))	→	mark#(X)	(16)
    mark#(cons(X1,X2))	→	mark#(X1)	(15)

    1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [s(x1)]	=	1 · x1
    [cons(x1, x2)]	=	1 · x1 + 1 · x2
    [mark#(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 Size-Change Termination

    Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

    mark#(s(X))	→	mark#(X)	(16)
    1	>	1
    mark#(cons(X1,X2))	→	mark#(X1)	(15)
    1	>	1

    As there is no critical graph in the transitive closure, there are no infinite chains.