Certification Problem

Input (TPDB TRS_Standard/AG01/#3.17)

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 4 components.

• The 1^st component contains the pair

  sum#(app(l,cons(x,cons(y,k))))

  →

  sum#(app(l,sum(cons(x,cons(y,k)))))

  (14)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	1
  [plus#(x1, x2)]	=	0
  [sum(x1)]	=	3
  [0]	=	1
  [nil]	=	1
  [app#(x1, x2)]	=	0
  [plus(x1, x2)]	=	x1 + 1
  [cons(x1, x2)]	=	x2 + 2
  [sum#(x1)]	=	x1 + 0
  [app(x1, x2)]	=	x1 + x2 + 20163

  together with the usable rules

  sum(cons(x,nil))	→	cons(x,nil)	(4)
  app(nil,k)	→	k	(1)
  app(cons(x,l),k)	→	cons(x,app(l,k))	(3)
  sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(5)
  sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(6)
  app(l,nil)	→	l	(2)

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

  sum#(app(l,cons(x,cons(y,k))))

  →

  sum#(app(l,sum(cons(x,cons(y,k)))))

  (14)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  sum#(cons(x,cons(y,l)))

  →

  sum#(cons(plus(x,y),l))

  (15)

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	1
  [plus#(x1, x2)]	=	0
  [sum(x1)]	=	17065
  [0]	=	1
  [nil]	=	17064
  [app#(x1, x2)]	=	0
  [plus(x1, x2)]	=	x1 + 1
  [cons(x1, x2)]	=	x2 + 1
  [sum#(x1)]	=	x1 + 0
  [app(x1, x2)]	=	x1 + x2 + 20819

  together with the usable rules

  sum(cons(x,nil))	→	cons(x,nil)	(4)
  app(nil,k)	→	k	(1)
  app(cons(x,l),k)	→	cons(x,app(l,k))	(3)
  sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(5)
  sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(6)
  app(l,nil)	→	l	(2)

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

  sum#(cons(x,cons(y,l)))

  →

  sum#(cons(plus(x,y),l))

  (15)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 3^rd component contains the pair

  plus#(s(x),y)

  →

  plus#(x,y)

  (11)

  1.1.3 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [plus#(x1, x2)]	=	x1 + 0
  [sum(x1)]	=	98764
  [0]	=	1
  [nil]	=	58177
  [app#(x1, x2)]	=	0
  [plus(x1, x2)]	=	x1 + 2998
  [cons(x1, x2)]	=	x2 + 40587
  [sum#(x1)]	=	x1 + 0
  [app(x1, x2)]	=	x1 + x2 + 42632

  together with the usable rules

  sum(cons(x,nil))	→	cons(x,nil)	(4)
  app(nil,k)	→	k	(1)
  app(cons(x,l),k)	→	cons(x,app(l,k))	(3)
  sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(5)
  sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(6)
  app(l,nil)	→	l	(2)

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

  plus#(s(x),y)

  →

  plus#(x,y)

  (11)

  could be deleted.

  1.1.3.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 4^th component contains the pair

  app#(cons(x,l),k)

  →

  app#(l,k)

  (10)

  1.1.4 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [plus#(x1, x2)]	=	0
  [sum(x1)]	=	2
  [0]	=	1
  [nil]	=	1
  [app#(x1, x2)]	=	x1 + 0
  [plus(x1, x2)]	=	x1 + 2998
  [cons(x1, x2)]	=	x2 + 1
  [sum#(x1)]	=	x1 + 0
  [app(x1, x2)]	=	x1 + x2 + 1

  together with the usable rules

  sum(cons(x,nil))	→	cons(x,nil)	(4)
  app(nil,k)	→	k	(1)
  app(cons(x,l),k)	→	cons(x,app(l,k))	(3)
  sum(cons(x,cons(y,l)))	→	sum(cons(plus(x,y),l))	(5)
  sum(app(l,cons(x,cons(y,k))))	→	sum(app(l,sum(cons(x,cons(y,k)))))	(6)
  app(l,nil)	→	l	(2)

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

  app#(cons(x,l),k)

  →

  app#(l,k)

  (10)

  could be deleted.

  1.1.4.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.