Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex49_GM04_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

• The 1^st component contains the pair

  mark#(if(X1,X2,X3))	→	mark#(X1)	(32)
  mark#(div(X1,X2))	→	mark#(X1)	(30)
  mark#(div(X1,X2))	→	a__div#(mark(X1),X2)	(31)
  a__div#(s(X),s(Y))	→	a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)	(25)
  a__if#(true,X,Y)	→	mark#(X)	(26)
  mark#(if(X1,X2,X3))	→	a__if#(mark(X1),X2,X3)	(33)
  a__if#(false,X,Y)	→	mark#(Y)	(27)
  mark#(s(X))	→	mark#(X)	(34)

  1.1.1 Reduction Pair Processor with Usable Rules

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

  [true]	=	2
  [a__div#(x1, x2)]	=	-∞ · x1 + 5 · x2 + 6
  [div(x1, x2)]	=	4 · x1 + 5 · x2 + 0
  [a__minus(x1, x2)]	=	2 · x1 + 2 · x2 + 0
  [a__geq(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [a__if#(x1, x2, x3)]	=	-∞ · x1 + 0 · x2 + 5 · x3 + 6
  [mark#(x1)]	=	0 · x1 + 6
  [false]	=	0
  [mark(x1)]	=	0 · x1 + -∞
  [0]	=	0
  [minus(x1, x2)]	=	-∞ · x1 + -∞ · x2 + 0
  [if(x1, x2, x3)]	=	0 · x1 + 1 · x2 + 6 · x3 + 7
  [geq(x1, x2)]	=	0 · x1 + -∞ · x2 + 6
  [a__if(x1, x2, x3)]	=	0 · x1 + 0 · x2 + -∞ · x3 + 8
  [a__div(x1, x2)]	=	-∞ · x1 + 0 · x2 + -∞
  [s(x1)]	=	0 · x1 + 0

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

  mark#(if(X1,X2,X3))

  →

  a__if#(mark(X1),X2,X3)

  (33)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [true]	=	0
  [a__div#(x1, x2)]	=	6 · x1 + 0 · x2 + 7
  [div(x1, x2)]	=	3 · x1 + 0 · x2 + 3
  [a__minus(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__geq(x1, x2)]	=	0 · x1 + 0 · x2 + 1
  [a__if#(x1, x2, x3)]	=	1 · x1 + 2 · x2 + 4 · x3 + 1
  [mark#(x1)]	=	2 · x1 + 1
  [false]	=	1
  [mark(x1)]	=	1 · x1 + 0
  [0]	=	0
  [minus(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [if(x1, x2, x3)]	=	2 · x1 + 1 · x2 + 1 · x3 + 0
  [geq(x1, x2)]	=	0 · x1 + 0 · x2 + 1
  [a__if(x1, x2, x3)]	=	2 · x1 + 1 · x2 + 1 · x3 + 0
  [a__div(x1, x2)]	=	3 · x1 + 0 · x2 + 3
  [s(x1)]	=	2 · x1 + 3

  together with the usable rules

  a__minus(0,Y)	→	0	(1)
  a__minus(s(X),s(Y))	→	a__minus(X,Y)	(2)
  a__geq(X,0)	→	true	(3)
  a__geq(0,s(Y))	→	false	(4)
  a__geq(s(X),s(Y))	→	a__geq(X,Y)	(5)
  a__div(0,s(Y))	→	0	(6)
  a__div(s(X),s(Y))	→	a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)	(7)
  a__if(true,X,Y)	→	mark(X)	(8)
  a__if(false,X,Y)	→	mark(Y)	(9)
  mark(minus(X1,X2))	→	a__minus(X1,X2)	(10)
  mark(geq(X1,X2))	→	a__geq(X1,X2)	(11)
  mark(div(X1,X2))	→	a__div(mark(X1),X2)	(12)
  mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(13)
  mark(0)	→	0	(14)
  mark(s(X))	→	s(mark(X))	(15)
  mark(true)	→	true	(16)
  mark(false)	→	false	(17)
  a__minus(X1,X2)	→	minus(X1,X2)	(18)
  a__geq(X1,X2)	→	geq(X1,X2)	(19)
  a__div(X1,X2)	→	div(X1,X2)	(20)
  a__if(X1,X2,X3)	→	if(X1,X2,X3)	(21)

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

  mark#(div(X1,X2))	→	mark#(X1)	(30)
  a__div#(s(X),s(Y))	→	a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)	(25)
  a__if#(false,X,Y)	→	mark#(Y)	(27)
  mark#(s(X))	→	mark#(X)	(34)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    mark#(if(X1,X2,X3))

    →

    mark#(X1)

    (32)

    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.

    mark#(if(X1,X2,X3))	→	mark#(X1)	(32)
    1	>	1

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

• The 2^nd component contains the pair

  a__geq#(s(X),s(Y))

  →

  a__geq#(X,Y)

  (23)

  1.1.2 Subterm Criterion Processor

  We use the projection

  π(a__geq#)

  =

  1

  and remove the pairs:

  a__geq#(s(X),s(Y))

  →

  a__geq#(X,Y)

  (23)

  1.1.2.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  a__minus#(s(X),s(Y))

  →

  a__minus#(X,Y)

  (22)

  1.1.3 Size-Change Termination

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

  a__minus#(s(X),s(Y))	→	a__minus#(X,Y)	(22)
  2	>	2
  1	>	1

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