Certification Problem

Input (TPDB TRS_Equational/Mixed_C/AC46)

The rewrite relation of the following equational TRS is considered.

Commutative symbols: eq

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 AC Dependency Pair Transformation

• The following set of (strict) dependency pairs is constructed for the TRS.

  app#(add(n,x),y)	→	app#(x,y)	(24)
  if_minsort#(true,add(n,x),y)	→	minsort#(app(rm(n,x),y),nil)	(25)
  minsort#(add(n,x),y)	→	eq#(n,min(add(n,x)))	(26)
  le#(s(x),s(y))	→	le#(x,y)	(27)
  if_rm#(false,n,add(m,x))	→	rm#(n,x)	(28)
  minsort#(add(n,x),y)	→	if_minsort#(eq(n,min(add(n,x))),add(n,x),y)	(29)
  minsort#(add(n,x),y)	→	min#(add(n,x))	(30)
  if_minsort#(true,add(n,x),y)	→	app#(rm(n,x),y)	(31)
  if_min#(true,add(n,add(m,x)))	→	min#(add(n,x))	(32)
  rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(33)
  eq#(s(x),s(y))	→	eq#(x,y)	(34)
  if_rm#(true,n,add(m,x))	→	rm#(n,x)	(35)
  min#(add(n,add(m,x)))	→	if_min#(le(n,m),add(n,add(m,x)))	(36)
  if_min#(false,add(n,add(m,x)))	→	min#(add(m,x))	(37)
  if_minsort#(true,add(n,x),y)	→	rm#(n,x)	(38)
  if_minsort#(false,add(n,x),y)	→	minsort#(x,add(n,y))	(39)
  min#(add(n,add(m,x)))	→	le#(n,m)	(40)
  rm#(n,add(m,x))	→	eq#(n,m)	(41)

  Finiteness for these DPs in combination with the equational DPs is proven as follows.

  1.1 Dependency Graph Processor

  The dependency pairs are split into 6 components.

  • The 1^st component contains the pair

    if_minsort#(false,add(n,x),y)	→	minsort#(x,add(n,y))	(39)
    minsort#(add(n,x),y)	→	if_minsort#(eq(n,min(add(n,x))),add(n,x),y)	(29)
    if_minsort#(true,add(n,x),y)	→	minsort#(app(rm(n,x),y),nil)	(25)

    1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 1
    [s(x1)]	=	1
    [le#(x1, x2)]	=	0
    [if_rm#(x1, x2, x3)]	=	0
    [if_min#(x1, x2)]	=	0
    [eq(x1, x2)]	=	1
    [false]	=	4
    [min#(x1)]	=	0
    [true]	=	3
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	1
    [app#(x1, x2)]	=	0
    [if_minsort#(x1, x2, x3)]	=	x2 + x3 + 0
    [min(x1)]	=	1
    [minsort#(x1, x2)]	=	x1 + x2 + 0
    [add(x1, x2)]	=	x2 + 3
    [if_min(x1, x2)]	=	0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 1
    [rm#(x1, x2)]	=	0
    [app(x1, x2)]	=	x1 + x2 + 0

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    if_minsort#(true,add(n,x),y)

    →

    minsort#(app(rm(n,x),y),nil)

    (25)

    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_minsort#(false,add(n,x),y)	→	minsort#(x,add(n,y))	(39)
      minsort#(add(n,x),y)	→	if_minsort#(eq(n,min(add(n,x))),add(n,x),y)	(29)

      1.1.1.1.1 AC Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [le(x1, x2)]	=	x1 + x2 + 1
      [if_rm(x1, x2, x3)]	=	x3 + 1
      [s(x1)]	=	1
      [le#(x1, x2)]	=	0
      [if_rm#(x1, x2, x3)]	=	0
      [if_min#(x1, x2)]	=	0
      [eq(x1, x2)]	=	1
      [false]	=	4
      [min#(x1)]	=	0
      [true]	=	3
      [eq#(x1, x2)]	=	0
      [0]	=	1
      [nil]	=	1
      [app#(x1, x2)]	=	0
      [if_minsort#(x1, x2, x3)]	=	x2 + 0
      [min(x1)]	=	1
      [minsort#(x1, x2)]	=	x1 + 1
      [add(x1, x2)]	=	x2 + 2
      [if_min(x1, x2)]	=	0
      [if_minsort(x1, x2, x3)]	=	0
      [minsort(x1, x2)]	=	0
      [rm(x1, x2)]	=	x2 + 1
      [rm#(x1, x2)]	=	0
      [app(x1, x2)]	=	x1 + x2 + 0

      together with the usable rules

      rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
      app(nil,y)	→	y	(8)
      if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
      if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
      rm(n,nil)	→	nil	(14)
      app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

      minsort#(add(n,x),y)	→	if_minsort#(eq(n,min(add(n,x))),add(n,x),y)	(29)
      if_minsort#(false,add(n,x),y)	→	minsort#(x,add(n,y))	(39)

      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

    if_rm#(true,n,add(m,x))	→	rm#(n,x)	(35)
    if_rm#(false,n,add(m,x))	→	rm#(n,x)	(28)
    rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(33)

    1.1.2 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 1
    [s(x1)]	=	1
    [le#(x1, x2)]	=	0
    [if_rm#(x1, x2, x3)]	=	x2 + x3 + 0
    [if_min#(x1, x2)]	=	0
    [eq(x1, x2)]	=	1
    [false]	=	4
    [min#(x1)]	=	0
    [true]	=	3
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	1
    [app#(x1, x2)]	=	0
    [if_minsort#(x1, x2, x3)]	=	0
    [min(x1)]	=	1
    [minsort#(x1, x2)]	=	x1 + 1
    [add(x1, x2)]	=	x2 + 2
    [if_min(x1, x2)]	=	0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 1
    [rm#(x1, x2)]	=	x1 + x2 + 1
    [app(x1, x2)]	=	x1 + x2 + 0

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(33)
    if_rm#(false,n,add(m,x))	→	rm#(n,x)	(28)
    if_rm#(true,n,add(m,x))	→	rm#(n,x)	(35)

    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

    if_min#(false,add(n,add(m,x)))	→	min#(add(m,x))	(37)
    min#(add(n,add(m,x)))	→	if_min#(le(n,m),add(n,add(m,x)))	(36)
    if_min#(true,add(n,add(m,x)))	→	min#(add(n,x))	(32)

    1.1.3 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 3
    [s(x1)]	=	1
    [le#(x1, x2)]	=	0
    [if_rm#(x1, x2, x3)]	=	0
    [if_min#(x1, x2)]	=	x2 + 0
    [eq(x1, x2)]	=	0
    [false]	=	25158
    [min#(x1)]	=	x1 + 1
    [true]	=	1
    [eq#(x1, x2)]	=	0
    [0]	=	25155
    [nil]	=	1
    [app#(x1, x2)]	=	0
    [if_minsort#(x1, x2, x3)]	=	0
    [min(x1)]	=	5
    [minsort#(x1, x2)]	=	x1 + 1
    [add(x1, x2)]	=	x2 + 2
    [if_min(x1, x2)]	=	x2 + 0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 3
    [rm#(x1, x2)]	=	1
    [app(x1, x2)]	=	x1 + x2 + 36718

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    if_min#(true,add(n,add(m,x)))	→	min#(add(n,x))	(32)
    min#(add(n,add(m,x)))	→	if_min#(le(n,m),add(n,add(m,x)))	(36)
    if_min#(false,add(n,add(m,x)))	→	min#(add(m,x))	(37)

    could be deleted.

    1.1.3.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 4^th component contains the pair

    le#(s(x),s(y))

    →

    le#(x,y)

    (27)

    1.1.4 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 35333
    [s(x1)]	=	x1 + 1
    [le#(x1, x2)]	=	x1 + x2 + 0
    [if_rm#(x1, x2, x3)]	=	0
    [if_min#(x1, x2)]	=	0
    [eq(x1, x2)]	=	0
    [false]	=	25158
    [min#(x1)]	=	1
    [true]	=	1
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	35789
    [app#(x1, x2)]	=	0
    [if_minsort#(x1, x2, x3)]	=	0
    [min(x1)]	=	3
    [minsort#(x1, x2)]	=	x1 + 1
    [add(x1, x2)]	=	x2 + 1
    [if_min(x1, x2)]	=	x2 + 0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 35333
    [rm#(x1, x2)]	=	1
    [app(x1, x2)]	=	x1 + x2 + 25440

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    le#(s(x),s(y))

    →

    le#(x,y)

    (27)

    could be deleted.

    1.1.4.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 5^th component contains the pair

    eq#(s(x),s(y))	→	eq#(x,y)	(34)
    eq#(x,y)	→	eq#(y,x)	(23)

    1.1.5 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 37986
    [s(x1)]	=	x1 + 1
    [le#(x1, x2)]	=	0
    [if_rm#(x1, x2, x3)]	=	0
    [if_min#(x1, x2)]	=	0
    [eq(x1, x2)]	=	0
    [false]	=	25158
    [min#(x1)]	=	1
    [true]	=	1
    [eq#(x1, x2)]	=	x1 + x2 + 0
    [0]	=	1
    [nil]	=	10282
    [app#(x1, x2)]	=	0
    [if_minsort#(x1, x2, x3)]	=	0
    [min(x1)]	=	3
    [minsort#(x1, x2)]	=	x1 + 1
    [add(x1, x2)]	=	x2 + 1
    [if_min(x1, x2)]	=	x2 + 0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 37986
    [rm#(x1, x2)]	=	1
    [app(x1, x2)]	=	x1 + x2 + 30801

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    eq#(s(x),s(y))

    →

    eq#(x,y)

    (34)

    could be deleted.

    1.1.5.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      eq#(x,y)

      →

      eq#(y,x)

      (23)

      1.1.5.1.1 AC Dependency Pair Problem is trivial

      There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
  • The 6^th component contains the pair

    app#(add(n,x),y)

    →

    app#(x,y)

    (24)

    1.1.6 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [le(x1, x2)]	=	x1 + x2 + 1
    [if_rm(x1, x2, x3)]	=	x3 + 31619
    [s(x1)]	=	x1 + 1
    [le#(x1, x2)]	=	0
    [if_rm#(x1, x2, x3)]	=	0
    [if_min#(x1, x2)]	=	0
    [eq(x1, x2)]	=	0
    [false]	=	25158
    [min#(x1)]	=	1
    [true]	=	1
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	1
    [app#(x1, x2)]	=	x1 + 0
    [if_minsort#(x1, x2, x3)]	=	0
    [min(x1)]	=	3
    [minsort#(x1, x2)]	=	x1 + 1
    [add(x1, x2)]	=	x2 + 1
    [if_min(x1, x2)]	=	x2 + 0
    [if_minsort(x1, x2, x3)]	=	0
    [minsort(x1, x2)]	=	0
    [rm(x1, x2)]	=	x2 + 31619
    [rm#(x1, x2)]	=	1
    [app(x1, x2)]	=	x1 + x2 + 45380

    together with the usable rules

    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
    app(nil,y)	→	y	(8)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
    rm(n,nil)	→	nil	(14)
    app(add(n,x),y)	→	add(n,app(x,y))	(9)

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

    app#(add(n,x),y)

    →

    app#(x,y)

    (24)

    could be deleted.

    1.1.6.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.