Certification Problem

Input (TPDB TRS_Standard/AProVE_04/JFP_Ex51)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ 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#(div(x,y))	→	div_active#(mark(x),y)	(31)
  mark#(div(x,y))	→	mark#(x)	(23)
  mark#(s(x))	→	mark#(x)	(22)
  mark#(if(x,y,z))	→	mark#(x)	(21)
  mark#(if(x,y,z))	→	if_active#(mark(x),y,z)	(28)
  if_active#(false,x,y)	→	mark#(y)	(27)
  if_active#(true,x,y)	→	mark#(x)	(26)
  div_active#(s(x),s(y))	→	if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(20)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [minus(x1, x2)]	=	0
  [false]	=	0
  [div(x1, x2)]	=	x1 + x2 + 41065
  [ge_active(x1, x2)]	=	0
  [true]	=	0
  [minus_active#(x1, x2)]	=	0
  [mark#(x1)]	=	x1 + 0
  [0]	=	0
  [if(x1, x2, x3)]	=	x1 + x2 + x3 + 0
  [ge(x1, x2)]	=	0
  [ge_active#(x1, x2)]	=	0
  [mark(x1)]	=	x1 + 0
  [if_active(x1, x2, x3)]	=	x1 + x2 + x3 + 0
  [minus_active(x1, x2)]	=	0
  [if_active#(x1, x2, x3)]	=	x2 + x3 + 0
  [div_active(x1, x2)]	=	x1 + x2 + 41065
  [div_active#(x1, x2)]	=	x1 + x2 + 41065

  together with the usable rules

  if_active(x,y,z)	→	if(x,y,z)	(18)
  mark(s(x))	→	s(mark(x))	(4)
  minus_active(x,y)	→	minus(x,y)	(15)
  mark(ge(x,y))	→	ge_active(x,y)	(8)
  minus_active(0,y)	→	0	(1)
  minus_active(s(x),s(y))	→	minus_active(x,y)	(3)
  if_active(false,x,y)	→	mark(y)	(16)
  div_active(x,y)	→	div(x,y)	(19)
  ge_active(x,y)	→	ge(x,y)	(17)
  ge_active(x,0)	→	true	(5)
  mark(div(x,y))	→	div_active(mark(x),y)	(10)
  ge_active(0,s(y))	→	false	(7)
  if_active(true,x,y)	→	mark(x)	(14)
  mark(if(x,y,z))	→	if_active(mark(x),y,z)	(12)
  div_active(0,s(y))	→	0	(11)
  ge_active(s(x),s(y))	→	ge_active(x,y)	(9)
  div_active(s(x),s(y))	→	if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(13)
  mark(minus(x,y))	→	minus_active(x,y)	(6)
  mark(0)	→	0	(2)

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

  mark#(div(x,y))	→	mark#(x)	(23)
  mark#(s(x))	→	mark#(x)	(22)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    if_active#(false,x,y)	→	mark#(y)	(27)
    mark#(div(x,y))	→	div_active#(mark(x),y)	(31)
    if_active#(true,x,y)	→	mark#(x)	(26)
    mark#(if(x,y,z))	→	mark#(x)	(21)
    mark#(if(x,y,z))	→	if_active#(mark(x),y,z)	(28)
    div_active#(s(x),s(y))	→	if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(20)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [s(x1)]	=	1
    [minus(x1, x2)]	=	0
    [false]	=	1
    [div(x1, x2)]	=	x1 + 4
    [ge_active(x1, x2)]	=	1
    [true]	=	0
    [minus_active#(x1, x2)]	=	0
    [mark#(x1)]	=	x1 + 0
    [0]	=	0
    [if(x1, x2, x3)]	=	x1 + x2 + x3 + 2
    [ge(x1, x2)]	=	0
    [ge_active#(x1, x2)]	=	0
    [mark(x1)]	=	x1 + 1
    [if_active(x1, x2, x3)]	=	x1 + x2 + x3 + 2
    [minus_active(x1, x2)]	=	0
    [if_active#(x1, x2, x3)]	=	x2 + x3 + 1
    [div_active(x1, x2)]	=	x1 + 4
    [div_active#(x1, x2)]	=	x1 + 2

    together with the usable rules

    if_active(x,y,z)	→	if(x,y,z)	(18)
    mark(s(x))	→	s(mark(x))	(4)
    minus_active(x,y)	→	minus(x,y)	(15)
    mark(ge(x,y))	→	ge_active(x,y)	(8)
    minus_active(0,y)	→	0	(1)
    minus_active(s(x),s(y))	→	minus_active(x,y)	(3)
    if_active(false,x,y)	→	mark(y)	(16)
    div_active(x,y)	→	div(x,y)	(19)
    ge_active(x,y)	→	ge(x,y)	(17)
    ge_active(x,0)	→	true	(5)
    mark(div(x,y))	→	div_active(mark(x),y)	(10)
    ge_active(0,s(y))	→	false	(7)
    if_active(true,x,y)	→	mark(x)	(14)
    mark(if(x,y,z))	→	if_active(mark(x),y,z)	(12)
    div_active(0,s(y))	→	0	(11)
    ge_active(s(x),s(y))	→	ge_active(x,y)	(9)
    div_active(s(x),s(y))	→	if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(13)
    mark(minus(x,y))	→	minus_active(x,y)	(6)
    mark(0)	→	0	(2)

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

    if_active#(false,x,y)	→	mark#(y)	(27)
    mark#(div(x,y))	→	div_active#(mark(x),y)	(31)
    if_active#(true,x,y)	→	mark#(x)	(26)
    mark#(if(x,y,z))	→	mark#(x)	(21)
    mark#(if(x,y,z))	→	if_active#(mark(x),y,z)	(28)
    div_active#(s(x),s(y))	→	if_active#(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(20)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  minus_active#(s(x),s(y))

  →

  minus_active#(x,y)

  (24)

  1.1.2 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 2
  [minus(x1, x2)]	=	0
  [false]	=	1
  [div(x1, x2)]	=	x1 + 28938
  [ge_active(x1, x2)]	=	6991
  [true]	=	1
  [minus_active#(x1, x2)]	=	x1 + 0
  [mark#(x1)]	=	0
  [0]	=	0
  [if(x1, x2, x3)]	=	x2 + x3 + 0
  [ge(x1, x2)]	=	6991
  [ge_active#(x1, x2)]	=	0
  [mark(x1)]	=	x1 + 0
  [if_active(x1, x2, x3)]	=	x2 + x3 + 0
  [minus_active(x1, x2)]	=	0
  [if_active#(x1, x2, x3)]	=	1
  [div_active(x1, x2)]	=	x1 + 28938
  [div_active#(x1, x2)]	=	x1 + 2

  together with the usable rules

  if_active(x,y,z)	→	if(x,y,z)	(18)
  mark(s(x))	→	s(mark(x))	(4)
  minus_active(x,y)	→	minus(x,y)	(15)
  mark(ge(x,y))	→	ge_active(x,y)	(8)
  minus_active(0,y)	→	0	(1)
  minus_active(s(x),s(y))	→	minus_active(x,y)	(3)
  if_active(false,x,y)	→	mark(y)	(16)
  div_active(x,y)	→	div(x,y)	(19)
  ge_active(x,y)	→	ge(x,y)	(17)
  ge_active(x,0)	→	true	(5)
  mark(div(x,y))	→	div_active(mark(x),y)	(10)
  ge_active(0,s(y))	→	false	(7)
  if_active(true,x,y)	→	mark(x)	(14)
  mark(if(x,y,z))	→	if_active(mark(x),y,z)	(12)
  div_active(0,s(y))	→	0	(11)
  ge_active(s(x),s(y))	→	ge_active(x,y)	(9)
  div_active(s(x),s(y))	→	if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(13)
  mark(minus(x,y))	→	minus_active(x,y)	(6)
  mark(0)	→	0	(2)

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

  minus_active#(s(x),s(y))

  →

  minus_active#(x,y)

  (24)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 3^rd component contains the pair

  ge_active#(s(x),s(y))

  →

  ge_active#(x,y)

  (32)

  1.1.3 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [s(x1)]	=	x1 + 1
  [minus(x1, x2)]	=	0
  [false]	=	11575
  [div(x1, x2)]	=	x1 + 54921
  [ge_active(x1, x2)]	=	11575
  [true]	=	1
  [minus_active#(x1, x2)]	=	0
  [mark#(x1)]	=	0
  [0]	=	0
  [if(x1, x2, x3)]	=	x2 + x3 + 0
  [ge(x1, x2)]	=	11575
  [ge_active#(x1, x2)]	=	x1 + x2 + 0
  [mark(x1)]	=	x1 + 0
  [if_active(x1, x2, x3)]	=	x2 + x3 + 0
  [minus_active(x1, x2)]	=	0
  [if_active#(x1, x2, x3)]	=	1
  [div_active(x1, x2)]	=	x1 + 54921
  [div_active#(x1, x2)]	=	x1 + 2

  together with the usable rules

  if_active(x,y,z)	→	if(x,y,z)	(18)
  mark(s(x))	→	s(mark(x))	(4)
  minus_active(x,y)	→	minus(x,y)	(15)
  mark(ge(x,y))	→	ge_active(x,y)	(8)
  minus_active(0,y)	→	0	(1)
  minus_active(s(x),s(y))	→	minus_active(x,y)	(3)
  if_active(false,x,y)	→	mark(y)	(16)
  div_active(x,y)	→	div(x,y)	(19)
  ge_active(x,y)	→	ge(x,y)	(17)
  ge_active(x,0)	→	true	(5)
  mark(div(x,y))	→	div_active(mark(x),y)	(10)
  ge_active(0,s(y))	→	false	(7)
  if_active(true,x,y)	→	mark(x)	(14)
  mark(if(x,y,z))	→	if_active(mark(x),y,z)	(12)
  div_active(0,s(y))	→	0	(11)
  ge_active(s(x),s(y))	→	ge_active(x,y)	(9)
  div_active(s(x),s(y))	→	if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0)	(13)
  mark(minus(x,y))	→	minus_active(x,y)	(6)
  mark(0)	→	0	(2)

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

  ge_active#(s(x),s(y))

  →

  ge_active#(x,y)

  (32)

  could be deleted.

  1.1.3.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.