Certification Problem

Input (TPDB TRS_Equational/AProVE_AC_04/AC53)

The rewrite relation of the following equational TRS is considered.

Associative symbols: times

Commutative symbols: times

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

The following set of (strict) dependency pairs is constructed for the TRS.

There are no rules.

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  fac#(s(x))

  →

  fac#(p(s(x)))

  (6)

  1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [p(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [fac#(x1)]	=	1 · x1

  together with the usable rule

  p(s(x))

  →

  x

  (1)

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

  fac(0)	→	s(0)	(2)
  fac(s(x))	→	times(s(x),fac(p(s(x))))	(3)

  could be deleted.

  1.1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [times(x1, x2)]	=	1 · x1 + 1 · x2
  [p(x1)]	=	1 · x1
  [s(x1)]	=	1 + 1 · x1
  [fac#(x1)]	=	1 · x1

  together with the usable rules

  p(s(x))	→	x	(1)
  times(x,y)	→	times(y,x)	(4)
  times(times(x,y),z)	→	times(x,times(y,z))	(5)

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

  p(s(x))

  →

  x

  (1)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.