Certification Problem

Input (TPDB TRS_Standard/AG01/#3.41)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

1.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)))

  (4)

  1.1.1.1 Usable Rules Processor

  We restrict the rewrite rules to the following usable rules of the DP problem.

  p(s(x))

  →

  x

  (1)

  1.1.1.1.1 Innermost Lhss Removal Processor

  We restrict the innermost strategy to the following left hand sides.

  p(s(x0))

  1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

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

  the rules

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

  could be deleted.

  1.1.1.1.1.1.1 Switch to TRS Processor

  We merge the DPs and rules into one TRS.

  1.1.1.1.1.1.1.1 Bounds

  The given TRS is match-(raise)-bounded by 1. This is shown by the following automaton.

  • final states:

    {0, 1, 2}

  • transitions:

    fac#0(0)	→	0
    fac#0(1)	→	0
    fac#0(2)	→	0
    s0(0)	→	1
    s0(1)	→	1
    s0(2)	→	1
    p0(0)	→	2
    p0(1)	→	2
    p0(2)	→	2
    s1(0)	→	4
    p1(4)	→	3
    fac#1(3)	→	0
    s1(1)	→	4
    s1(2)	→	4