Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/Ex9_Luc04_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 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  a__f#(a,b,X)	→	mark#(X)	(11)
  mark#(f(X1,X2,X3))	→	a__f#(mark(X1),X2,mark(X3))	(12)
  a__f#(a,b,X)	→	a__f#(mark(X),X,mark(X))	(10)
  mark#(f(X1,X2,X3))	→	mark#(X1)	(13)
  mark#(f(X1,X2,X3))	→	mark#(X3)	(14)

  1.1.1 Reduction Pair Processor

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

  [a__f#(x1, x2, x3)]	=	-∞ + 0 · x1 + -∞ · x2 + 0 · x3
  [a]	=	0
  [b]	=	2
  [mark#(x1)]	=	0 + 0 · x1
  [f(x1, x2, x3)]	=	-∞ + 1 · x1 + 0 · x2 + 1 · x3
  [mark(x1)]	=	-∞ + 0 · x1
  [a__f(x1, x2, x3)]	=	-∞ + 1 · x1 + 0 · x2 + 1 · x3
  [c]	=	3
  [a__c]	=	3

  the pair

  mark#(f(X1,X2,X3))

  →

  a__f#(mark(X1),X2,mark(X3))

  (12)

  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,b,X)

    →

    a__f#(mark(X),X,mark(X))

    (10)

    1.1.1.1.1 Narrowing Processor

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

    a__f#(a,b,f(x0,x1,x2))	→	a__f#(a__f(mark(x0),x1,mark(x2)),f(x0,x1,x2),mark(f(x0,x1,x2)))	(16)
    a__f#(a,b,c)	→	a__f#(a__c,c,mark(c))	(17)
    a__f#(a,b,a)	→	a__f#(a,a,mark(a))	(18)
    a__f#(a,b,b)	→	a__f#(b,b,mark(b))	(19)

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 2^nd component contains the pair

    mark#(f(X1,X2,X3))	→	mark#(X3)	(14)
    mark#(f(X1,X2,X3))	→	mark#(X1)	(13)

    1.1.1.1.2 Usable Rules Processor

    We restrict the rewrite rules to the following usable rules of the DP problem.

    There are no rules.

    1.1.1.1.2.1 Innermost Lhss Removal Processor

    We restrict the innermost strategy to the following left hand sides.

    There are no lhss.

    1.1.1.1.2.1.1 Size-Change Termination

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

    mark#(f(X1,X2,X3))	→	mark#(X3)	(14)
    1	>	1
    mark#(f(X1,X2,X3))	→	mark#(X1)	(13)
    1	>	1

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