Certification Problem

Input (TPDB TRS_Standard/CiME_04/log2)

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 Rule Removal

1.1.1.1 Rule Removal

1.1.1.1.1 Rule Removal

1.1.1.1.1.1 Dependency Pair Transformation

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  +#(1(x),1(y))	→	+#(+(x,y),1(#))	(35)
  +#(+(x,y),z)	→	+#(x,+(y,z))	(38)
  +#(+(x,y),z)	→	+#(y,z)	(37)
  +#(1(x),1(y))	→	+#(x,y)	(34)
  +#(1(x),0(y))	→	+#(x,y)	(33)
  +#(0(x),1(y))	→	+#(x,y)	(32)
  +#(0(x),0(y))	→	+#(x,y)	(30)

  1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

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

  together with the usable rules

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

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

  +#(1(x),1(y))	→	+#(x,y)	(34)
  +#(1(x),0(y))	→	+#(x,y)	(33)
  +#(0(x),1(y))	→	+#(x,y)	(32)

  could be deleted.

  1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

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

  together with the usable rules

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

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

  +#(1(x),1(y))	→	+#(+(x,y),1(#))	(35)
  +#(0(x),0(y))	→	+#(x,y)	(30)

  could be deleted.

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

  +#(+(x,y),z)	→	+#(x,+(y,z))	(38)
  1	>	1
  +#(+(x,y),z)	→	+#(y,z)	(37)
  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

  -#(1(x),1(y))	→	-#(x,y)	(44)
  -#(1(x),0(y))	→	-#(x,y)	(43)
  -#(0(x),1(y))	→	-#(-(x,y),1(#))	(42)
  -#(0(x),1(y))	→	-#(x,y)	(41)
  -#(0(x),0(y))	→	-#(x,y)	(39)

  1.1.1.1.1.1.1.2 Subterm Criterion Processor

  We use the projection to multisets

  π(-#)	=	{ 1, 1 }
  π(-)	=	{ 1 }
  π(1)	=	{ 1, 1 }
  π(0)	=	{ 1, 1 }

  to remove the pairs:

  -#(1(x),1(y))	→	-#(x,y)	(44)
  -#(1(x),0(y))	→	-#(x,y)	(43)
  -#(0(x),1(y))	→	-#(-(x,y),1(#))	(42)
  -#(0(x),1(y))	→	-#(x,y)	(41)
  -#(0(x),0(y))	→	-#(x,y)	(39)

  1.1.1.1.1.1.1.2.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  ge#(1(x),1(y))	→	ge#(x,y)	(50)
  ge#(1(x),0(y))	→	ge#(x,y)	(49)
  ge#(0(x),1(y))	→	ge#(y,x)	(47)
  ge#(0(x),0(y))	→	ge#(x,y)	(46)

  1.1.1.1.1.1.1.3 Size-Change Termination

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

  ge#(1(x),1(y))	→	ge#(x,y)	(50)
  2	>	2
  1	>	1
  ge#(1(x),0(y))	→	ge#(x,y)	(49)
  2	>	2
  1	>	1
  ge#(0(x),1(y))	→	ge#(y,x)	(47)
  2	>	1
  1	>	2
  ge#(0(x),0(y))	→	ge#(x,y)	(46)
  2	>	2
  1	>	1

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

• The 4^th component contains the pair

  ge#(#,0(x))

  →

  ge#(#,x)

  (51)

  1.1.1.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#(#,0(x))	→	ge#(#,x)	(51)
  2	>	2
  1	≥	1

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