Certification Problem

Input (TPDB TRS_Standard/AG01/#3.21)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ 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

  times#(x,plus(y,1))

  →

  times#(x,plus(y,times(1,0)))

  (7)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(times#)	=	0		stat(times#)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(times)	=	4		stat(times)	=	lex
  prec(plus)	=	5		stat(plus)	=	lex
  prec(1)	=	5		stat(1)	=	lex

  π(times#)	=	2
  π(0)	=	[]
  π(times)	=	[]
  π(plus)	=	[1,2]
  π(1)	=	[]

  together with the usable rules

  times(x,0)	→	0	(4)
  plus(x,0)	→	x	(3)

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

  times#(x,plus(y,1))

  →

  times#(x,plus(y,times(1,0)))

  (7)

  could be deleted.

  1.1.1.1 P is empty

  There are no pairs anymore.