Certification Problem

Input (TPDB TRS_Standard/Der95/30)

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

  :#(:(:(:(C,x),y),z),u)	→	:#(:(x,y),z)	(6)
  :#(:(:(:(C,x),y),z),u)	→	:#(:(x,z),:(:(:(x,y),z),u))	(5)
  :#(:(:(:(C,x),y),z),u)	→	:#(:(:(x,y),z),u)	(4)
  :#(:(:(:(C,x),y),z),u)	→	:#(x,y)	(3)
  :#(:(:(:(C,x),y),z),u)	→	:#(x,z)	(2)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [:#(x1, x2)]	=	max(x1 + 28959, x2 + 28958, 0)
  [C]	=	38
  [:(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)

  together with the usable rule

  :(:(:(:(C,x),y),z),u)

  →

  :(:(x,z),:(:(:(x,y),z),u))

  (1)

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

  :#(:(:(:(C,x),y),z),u)	→	:#(:(x,y),z)	(6)
  :#(:(:(:(C,x),y),z),u)	→	:#(x,y)	(3)
  :#(:(:(:(C,x),y),z),u)	→	:#(x,z)	(2)

  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

    :#(:(:(:(C,x),y),z),u)	→	:#(:(:(x,y),z),u)	(4)
    :#(:(:(:(C,x),y),z),u)	→	:#(:(x,z),:(:(:(x,y),z),u))	(5)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the argument filter
    in combination with the following Weighted Path Order with the following precedence and status

    prec(:#)	=	1		status(:#)	=	[1]		list-extension(:#)	=	Lex
    prec(C)	=	0		status(C)	=	[]		list-extension(C)	=	Lex
    prec(:)	=	2		status(:)	=	[1, 2]		list-extension(:)	=	Lex

    and the following Max-polynomial interpretation

    [:#(x1, x2)]	=	max(x1 + 0, 0)
    [C]	=	0
    [:(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)

    together with the usable rule

    :(:(:(:(C,x),y),z),u)

    →

    :(:(x,z),:(:(:(x,y),z),u))

    (1)

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

    :#(:(:(:(C,x),y),z),u)	→	:#(:(:(x,y),z),u)	(4)
    :#(:(:(:(C,x),y),z),u)	→	:#(:(x,z),:(:(:(x,y),z),u))	(5)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.