Certification Problem

Input (TPDB TRS_Standard/CiME_04/append-hard)

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

  ifappend#(l1,l2,false)	→	append#(tl(l1),l2)	(11)
  append#(l1,l2)	→	ifappend#(l1,l2,is_empty(l1))	(8)

  1.1.1.1 Usable Rules Processor

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

  is_empty(nil)	→	true	(1)
  is_empty(cons(x,l))	→	false	(2)
  tl(cons(x,l))	→	l	(4)

  1.1.1.1.1 Innermost Lhss Removal Processor

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

  is_empty(nil)

  is_empty(cons(x0,x1))

  tl(cons(x0,x1))

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the rationals with delta = 7/16

  [ifappend#(x1, x2, x3)]	=	0 + 1 · x1 + 0 · x2 + 1/4 · x3
  [false]	=	4
  [append#(x1, x2)]	=	1/2 + 2 · x1 + 0 · x2
  [tl(x1)]	=	1/4 + 1/2 · x1
  [is_empty(x1)]	=	1/4 + 4 · x1
  [cons(x1, x2)]	=	2 + 0 · x1 + 2 · x2
  [nil]	=	2
  [true]	=	2

  the pair

  append#(l1,l2)

  →

  ifappend#(l1,l2,is_empty(l1))

  (8)

  could be deleted.

  1.1.1.1.1.1.1 Usable Rules Processor

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

  tl(cons(x,l))

  →

  l

  (4)

  1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor

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

  tl(cons(x0,x1))

  1.1.1.1.1.1.1.1.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  ifappend#(l1,l2,false)	→	append#(tl(l1),l2)	(11)
  2	≥	2

  As there is no critical graph in the transitive closure, there are no infinite chains.