Certification Problem

Input (TPDB TRS_Standard/CiME_04/filliatre3)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  fold#(t,x,s(n))

  →

  fold#(t,x,n)

  (29)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [fold#(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  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.

  fold#(t,x,s(n))	→	fold#(t,x,n)	(29)
  1	≥	1
  2	≥	2
  3	>	3

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

• The 2^nd component contains the pair

  f#(t,x)	→	f'#(t,g(x))	(22)
  f'#(triple(a,b,c),B)	→	f#(triple(a,b,c),A)	(24)
  f'#(triple(a,b,c),A)	→	f''#(foldB(triple(s(a),0,c),b))	(25)
  f''#(triple(a,b,c))	→	foldC#(triple(a,b,0),c)	(27)
  foldC#(t,s(n))	→	f#(foldC(t,n),C)	(20)
  foldC#(t,s(n))	→	foldC#(t,n)	(21)
  f'#(triple(a,b,c),A)	→	foldB#(triple(s(a),0,c),b)	(26)
  foldB#(t,s(n))	→	f#(foldB(t,n),B)	(18)
  foldB#(t,s(n))	→	foldB#(t,n)	(19)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [foldB(x1, x2)]	=	1 · x1 + 1 · x2
  [0]	=	0
  [s(x1)]	=	1 · x1
  [f(x1, x2)]	=	1 · x1 + 1 · x2
  [B]	=	0
  [foldC(x1, x2)]	=	1 · x1 + 1 · x2
  [C]	=	0
  [f'(x1, x2)]	=	1 · x1 + 1 · x2
  [g(x1)]	=	1 · x1
  [triple(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [A]	=	0
  [f''(x1)]	=	1 · x1
  [f'#(x1, x2)]	=	1 · x1 + 1 · x2
  [f#(x1, x2)]	=	1 · x1 + 1 · x2
  [f''#(x1)]	=	1 · x1
  [foldC#(x1, x2)]	=	1 · x1 + 1 · x2
  [foldB#(x1, x2)]	=	1 · x1 + 1 · x2

  together with the usable rules

  foldB(t,0)	→	t	(7)
  foldB(t,s(n))	→	f(foldB(t,n),B)	(8)
  foldC(t,s(n))	→	f(foldC(t,n),C)	(10)
  f(t,x)	→	f'(t,g(x))	(11)
  f'(triple(a,b,c),B)	→	f(triple(a,b,c),A)	(13)
  f'(triple(a,b,c),A)	→	f''(foldB(triple(s(a),0,c),b))	(14)
  f''(triple(a,b,c))	→	foldC(triple(a,b,0),c)	(15)
  foldC(t,0)	→	t	(9)
  g(A)	→	A	(1)
  g(B)	→	A	(2)
  g(B)	→	B	(3)
  g(C)	→	A	(4)
  g(C)	→	B	(5)
  g(C)	→	C	(6)
  f'(triple(a,b,c),C)	→	triple(a,b,s(c))	(12)

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

  1.1.2.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [foldB(x1, x2)]	=	1 · x1 + 2 · x2
  [0]	=	0
  [s(x1)]	=	2 + 1 · x1
  [f(x1, x2)]	=	1 · x1 + 2 · x2
  [B]	=	2
  [foldC(x1, x2)]	=	1 · x1 + 2 · x2
  [C]	=	2
  [f'(x1, x2)]	=	1 · x1 + 2 · x2
  [g(x1)]	=	1 · x1
  [triple(x1, x2, x3)]	=	1 · x1 + 2 · x2 + 2 · x3
  [A]	=	2
  [f''(x1)]	=	1 + 1 · x1
  [f#(x1, x2)]	=	1 · x1 + 2 · x2
  [f'#(x1, x2)]	=	1 · x1 + 2 · x2
  [f''#(x1)]	=	2 + 1 · x1
  [foldC#(x1, x2)]	=	1 · x1 + 2 · x2
  [foldB#(x1, x2)]	=	1 + 1 · x1 + 2 · x2

  the pairs

  f''#(triple(a,b,c))	→	foldC#(triple(a,b,0),c)	(27)
  foldC#(t,s(n))	→	foldC#(t,n)	(21)
  f'#(triple(a,b,c),A)	→	foldB#(triple(s(a),0,c),b)	(26)
  foldB#(t,s(n))	→	f#(foldB(t,n),B)	(18)
  foldB#(t,s(n))	→	foldB#(t,n)	(19)

  and the rules

  f'(triple(a,b,c),A)	→	f''(foldB(triple(s(a),0,c),b))	(14)
  f''(triple(a,b,c))	→	foldC(triple(a,b,0),c)	(15)

  could be deleted.

  1.1.2.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    f'#(triple(a,b,c),B)	→	f#(triple(a,b,c),A)	(24)
    f#(t,x)	→	f'#(t,g(x))	(22)

    1.1.2.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [g(x1)]	=	1 · x1
    [A]	=	0
    [B]	=	0
    [C]	=	0
    [triple(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
    [f#(x1, x2)]	=	1 · x1 + 1 · x2
    [f'#(x1, x2)]	=	1 · x1 + 1 · x2

    together with the usable rules

    g(A)	→	A	(1)
    g(B)	→	A	(2)
    g(B)	→	B	(3)
    g(C)	→	A	(4)
    g(C)	→	B	(5)
    g(C)	→	C	(6)

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

    1.1.2.1.1.1.1 Monotonic Reduction Pair Processor

    Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

    prec(A)	=	0		weight(A)	=	1
    prec(B)	=	1		weight(B)	=	2
    prec(C)	=	2		weight(C)	=	2
    prec(g)	=	6		weight(g)	=	0
    prec(f'#)	=	3		weight(f'#)	=	0
    prec(f#)	=	5		weight(f#)	=	0
    prec(triple)	=	4		weight(triple)	=	0

    the pairs

    f'#(triple(a,b,c),B)	→	f#(triple(a,b,c),A)	(24)
    f#(t,x)	→	f'#(t,g(x))	(22)

    and the rules

    g(A)	→	A	(1)
    g(B)	→	A	(2)
    g(B)	→	B	(3)
    g(C)	→	A	(4)
    g(C)	→	B	(5)
    g(C)	→	C	(6)

    could be deleted.

    1.1.2.1.1.1.1.1 P is empty

    There are no pairs anymore.