Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/sigma)

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

  comp#(comp(s,t),u)	→	comp#(s,comp(t,u))	(17)
  comp#(cons(s,t),u)	→	comp#(t,u)	(16)
  comp#(abs(s),t)	→	comp#(s,cons(one,comp(t,shift)))	(15)
  comp#(abs(s),t)	→	comp#(t,shift)	(14)
  comp#(comp(s,t),u)	→	comp#(t,u)	(13)
  comp#(cons(s,t),u)	→	comp#(s,u)	(12)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [cons#(x1, x2)]	=	max(0)
  [one]	=	0
  [abs(x1)]	=	x1 + 1
  [comp#(x1, x2)]	=	x1 + x2 + 0
  [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [id]	=	0
  [shift]	=	0
  [comp(x1, x2)]	=	x1 + x2 + 0

  together with the usable rules

  comp(one,cons(s,t))	→	s	(4)
  comp(id,s)	→	s	(8)
  comp(s,id)	→	s	(1)
  cons(comp(one,s),comp(shift,s))	→	s	(3)
  comp(shift,cons(s,t))	→	t	(5)
  comp(cons(s,t),u)	→	cons(comp(s,u),comp(t,u))	(7)
  comp(comp(s,t),u)	→	comp(s,comp(t,u))	(9)
  comp(abs(s),t)	→	abs(comp(s,cons(one,comp(t,shift))))	(6)
  cons(one,shift)	→	id	(2)

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

  comp#(abs(s),t)	→	comp#(s,cons(one,comp(t,shift)))	(15)
  comp#(abs(s),t)	→	comp#(t,shift)	(14)

  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

    comp#(cons(s,t),u)	→	comp#(t,u)	(16)
    comp#(cons(s,t),u)	→	comp#(s,u)	(12)
    comp#(comp(s,t),u)	→	comp#(t,u)	(13)
    comp#(comp(s,t),u)	→	comp#(s,comp(t,u))	(17)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [cons#(x1, x2)]	=	0
    [one]	=	1
    [abs(x1)]	=	x1 + 23676
    [comp#(x1, x2)]	=	x1 + 0
    [cons(x1, x2)]	=	x1 + x2 + 1
    [id]	=	4
    [shift]	=	1
    [comp(x1, x2)]	=	x1 + x2 + 1

    having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

    comp#(cons(s,t),u)	→	comp#(t,u)	(16)
    comp#(cons(s,t),u)	→	comp#(s,u)	(12)
    comp#(comp(s,t),u)	→	comp#(t,u)	(13)
    comp#(comp(s,t),u)	→	comp#(s,comp(t,u))	(17)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.