Certification Problem

Input (TPDB TRS_Standard/Various_04/14)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

1.1 Rule Removal

1.1.1 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

• The 1^st component contains the pair

  -#(I(x),I(y))	→	-#(x,y)	(58)
  -#(I(x),O(y))	→	-#(x,y)	(57)
  -#(O(x),I(y))	→	-#(-(x,y),I(1))	(56)
  -#(O(x),I(y))	→	-#(x,y)	(55)
  -#(O(x),O(y))	→	-#(x,y)	(53)

  1.1.1.1.1 Subterm Criterion Processor

  We use the projection to multisets

  π(-#)	=	{ 1, 1 }
  π(N)	=	{ 2 }
  π(L)	=	{ 1 }
  π(-)	=	{ 1 }
  π(I)	=	{ 1, 1 }
  π(O)	=	{ 1, 1 }

  to remove the pairs:

  -#(I(x),I(y))	→	-#(x,y)	(58)
  -#(I(x),O(y))	→	-#(x,y)	(57)
  -#(O(x),I(y))	→	-#(-(x,y),I(1))	(56)
  -#(O(x),I(y))	→	-#(x,y)	(55)
  -#(O(x),O(y))	→	-#(x,y)	(53)

  1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  Log'#(O(x))	→	Log'#(x)	(68)
  Log'#(I(x))	→	Log'#(x)	(66)

  1.1.1.1.2 Size-Change Termination

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

  Log'#(O(x))	→	Log'#(x)	(68)
  1	>	1
  Log'#(I(x))	→	Log'#(x)	(66)
  1	>	1

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

• The 3^rd component contains the pair

  +#(I(x),I(y))	→	+#(+(x,y),I(0))	(49)
  +#(I(x),I(y))	→	+#(x,y)	(48)
  +#(x,+(y,z))	→	+#(+(x,y),z)	(52)
  +#(x,+(y,z))	→	+#(x,y)	(51)
  +#(I(x),O(y))	→	+#(x,y)	(47)
  +#(O(x),I(y))	→	+#(x,y)	(46)
  +#(O(x),O(y))	→	+#(x,y)	(44)

  1.1.1.1.3 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [O(x1)]	=	0 · x1 + 0
  [I(x1)]	=	0 · x1 + -∞
  [0]	=	0
  [+#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [+(x1, x2)]	=	0 · x1 + 1 · x2 + 6

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

  +#(x,+(y,z))

  →

  +#(+(x,y),z)

  (52)

  could be deleted.

  1.1.1.1.3.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [O(x1)]	=	1 · x1 + 4
  [I(x1)]	=	0 · x1 + -∞
  [0]	=	0
  [+#(x1, x2)]	=	-∞ · x1 + 0 · x2 + 0
  [+(x1, x2)]	=	2 · x1 + 0 · x2 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

  +#(I(x),O(y))	→	+#(x,y)	(47)
  +#(O(x),O(y))	→	+#(x,y)	(44)

  could be deleted.

  1.1.1.1.3.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [O(x1)]	=	0 · x1 + 4
  [I(x1)]	=	1 · x1 + 1
  [0]	=	0
  [+#(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [+(x1, x2)]	=	0 · x1 + -∞ · x2 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

  +#(I(x),I(y))	→	+#(x,y)	(48)
  +#(O(x),I(y))	→	+#(x,y)	(46)

  could be deleted.

  1.1.1.1.3.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    +#(x,+(y,z))

    →

    +#(x,y)

    (51)

    1.1.1.1.3.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.

    +#(x,+(y,z))	→	+#(x,y)	(51)
    2	>	2
    1	≥	1

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

  • The 2^nd component contains the pair

    +#(I(x),I(y))

    →

    +#(+(x,y),I(0))

    (49)

    1.1.1.1.3.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the rationals with delta = 1/64

    [O(x1)]	=	1 · x1 + 0
    [I(x1)]	=	1 · x1 + 1
    [0]	=	0
    [+#(x1, x2)]	=	1/2 · x1 + 1 · x2 + 0
    [+(x1, x2)]	=	1 · x1 + 2 · x2 + 0

    together with the usable rules

    +(0,x)	→	x	(2)
    +(x,0)	→	x	(3)
    +(O(x),O(y))	→	O(+(x,y))	(4)
    +(O(x),I(y))	→	I(+(x,y))	(5)
    +(I(x),O(y))	→	I(+(x,y))	(6)
    +(I(x),I(y))	→	O(+(+(x,y),I(0)))	(7)
    +(x,+(y,z))	→	+(+(x,y),z)	(8)
    O(0)	→	0	(1)

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

    +#(I(x),I(y))

    →

    +#(+(x,y),I(0))

    (49)

    could be deleted.

    1.1.1.1.3.1.1.1.2.1 P is empty

    There are no pairs anymore.

• The 4^th component contains the pair

  ge#(I(x),I(y))	→	ge#(x,y)	(64)
  ge#(I(x),O(y))	→	ge#(x,y)	(63)
  ge#(O(x),I(y))	→	ge#(y,x)	(61)
  ge#(O(x),O(y))	→	ge#(x,y)	(60)

  1.1.1.1.4 Size-Change Termination

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

  ge#(I(x),I(y))	→	ge#(x,y)	(64)
  2	>	2
  1	>	1
  ge#(I(x),O(y))	→	ge#(x,y)	(63)
  2	>	2
  1	>	1
  ge#(O(x),I(y))	→	ge#(y,x)	(61)
  2	>	1
  1	>	2
  ge#(O(x),O(y))	→	ge#(x,y)	(60)
  2	>	2
  1	>	1

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

• The 5^th component contains the pair

  ge#(0,O(x))

  →

  ge#(0,x)

  (65)

  1.1.1.1.5 Size-Change Termination

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

  ge#(0,O(x))	→	ge#(0,x)	(65)
  2	>	2
  1	≥	1

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