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 AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

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

There are no rules.

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

• The 1^st component contains the pair

  if_minsort#(true,add(n,x),y)	→	minsort#(app(rm(n,x),y),nil)	(38)
  minsort#(add(n,x),y)	→	if_minsort#(eq(n,min(add(n,x))),add(n,x),y)	(35)
  if_minsort#(false,add(n,x),y)	→	minsort#(x,add(n,y))	(41)

  1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  together with the usable rules

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

  (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)

  (38)

  could be deleted.

  1.1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

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

  →

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

  (41)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(31)
  if_rm#(true,n,add(m,x))	→	rm#(n,x)	(33)
  if_rm#(false,n,add(m,x))	→	rm#(n,x)	(34)

  1.1.2 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [if_rm#(x1, x2, x3)]	=	3 · x2 + 2 · x3
  [true]	=	0
  [add(x1, x2)]	=	2 + 1 · x2
  [rm#(x1, x2)]	=	3 + 3 · x1 + 2 · x2
  [eq(x1, x2)]	=	0
  [false]	=	0
  [0]	=	0
  [s(x1)]	=	0

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

  if_rm#(true,n,add(m,x))	→	rm#(n,x)	(33)
  rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(31)
  if_rm#(false,n,add(m,x))	→	rm#(n,x)	(34)

  could be deleted.

  1.1.2.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 3^rd component contains the pair

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

  1.1.3 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [eq#(x1, x2)]	=	3 · x1 + 3 · x2
  [s(x1)]	=	3 · x1

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

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

  →

  eq#(x,y)

  (24)

  and the rules

  eq(0,0)	→	true	(1)
  eq(0,s(x))	→	false	(2)
  eq(s(x),0)	→	false	(3)
  eq(s(x),s(y))	→	eq(x,y)	(4)
  le(0,y)	→	true	(5)
  le(s(x),0)	→	false	(6)
  le(s(x),s(y))	→	le(x,y)	(7)
  app(nil,y)	→	y	(8)
  app(add(n,x),y)	→	add(n,app(x,y))	(9)
  min(add(n,nil))	→	n	(10)
  min(add(n,add(m,x)))	→	if_min(le(n,m),add(n,add(m,x)))	(11)
  if_min(true,add(n,add(m,x)))	→	min(add(n,x))	(12)
  if_min(false,add(n,add(m,x)))	→	min(add(m,x))	(13)
  rm(n,nil)	→	nil	(14)
  rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
  if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
  if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
  minsort(nil,nil)	→	nil	(18)
  minsort(add(n,x),y)	→	if_minsort(eq(n,min(add(n,x))),add(n,x),y)	(19)
  if_minsort(true,add(n,x),y)	→	add(n,minsort(app(rm(n,x),y),nil))	(20)
  if_minsort(false,add(n,x),y)	→	minsort(x,add(n,y))	(21)

  could be deleted.

  1.1.3.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 4^th component contains the pair

  min#(add(n,add(m,x)))	→	if_min#(le(n,m),add(n,add(m,x)))	(27)
  if_min#(true,add(n,add(m,x)))	→	min#(add(n,x))	(29)
  if_min#(false,add(n,add(m,x)))	→	min#(add(m,x))	(30)

  1.1.4 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [if_min#(x1, x2)]	=	2 · x2
  [true]	=	0
  [add(x1, x2)]	=	3 + 3 · x2
  [min#(x1)]	=	3 + 3 · x1
  [false]	=	0
  [le(x1, x2)]	=	0
  [s(x1)]	=	3 · x1
  [0]	=	0

  having no usable rules (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))	(29)
  if_min#(false,add(n,add(m,x)))	→	min#(add(m,x))	(30)
  min#(add(n,add(m,x)))	→	if_min#(le(n,m),add(n,add(m,x)))	(27)

  could be deleted.

  1.1.4.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 5^th component contains the pair

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

  →

  le#(x,y)

  (25)

  1.1.5 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [le#(x1, x2)]	=	3 · x1 + 3 · x2
  [s(x1)]	=	1 · x1

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

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

  →

  le#(x,y)

  (25)

  and the rules

  eq(0,0)	→	true	(1)
  eq(0,s(x))	→	false	(2)
  eq(s(x),0)	→	false	(3)
  eq(s(x),s(y))	→	eq(x,y)	(4)
  le(0,y)	→	true	(5)
  le(s(x),0)	→	false	(6)
  le(s(x),s(y))	→	le(x,y)	(7)
  app(nil,y)	→	y	(8)
  app(add(n,x),y)	→	add(n,app(x,y))	(9)
  min(add(n,nil))	→	n	(10)
  min(add(n,add(m,x)))	→	if_min(le(n,m),add(n,add(m,x)))	(11)
  if_min(true,add(n,add(m,x)))	→	min(add(n,x))	(12)
  if_min(false,add(n,add(m,x)))	→	min(add(m,x))	(13)
  rm(n,nil)	→	nil	(14)
  rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
  if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
  if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
  minsort(nil,nil)	→	nil	(18)
  minsort(add(n,x),y)	→	if_minsort(eq(n,min(add(n,x))),add(n,x),y)	(19)
  if_minsort(true,add(n,x),y)	→	add(n,minsort(app(rm(n,x),y),nil))	(20)
  if_minsort(false,add(n,x),y)	→	minsort(x,add(n,y))	(21)

  could be deleted.

  1.1.5.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)

  (26)

  1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [app#(x1, x2)]	=	3 · x1 + 1 · x2
  [add(x1, x2)]	=	1 · x1 + 3 · x2

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

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

  →

  app#(x,y)

  (26)

  and the rules

  eq(0,0)	→	true	(1)
  eq(0,s(x))	→	false	(2)
  eq(s(x),0)	→	false	(3)
  eq(s(x),s(y))	→	eq(x,y)	(4)
  le(0,y)	→	true	(5)
  le(s(x),0)	→	false	(6)
  le(s(x),s(y))	→	le(x,y)	(7)
  app(nil,y)	→	y	(8)
  app(add(n,x),y)	→	add(n,app(x,y))	(9)
  min(add(n,nil))	→	n	(10)
  min(add(n,add(m,x)))	→	if_min(le(n,m),add(n,add(m,x)))	(11)
  if_min(true,add(n,add(m,x)))	→	min(add(n,x))	(12)
  if_min(false,add(n,add(m,x)))	→	min(add(m,x))	(13)
  rm(n,nil)	→	nil	(14)
  rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
  if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
  if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
  minsort(nil,nil)	→	nil	(18)
  minsort(add(n,x),y)	→	if_minsort(eq(n,min(add(n,x))),add(n,x),y)	(19)
  if_minsort(true,add(n,x),y)	→	add(n,minsort(app(rm(n,x),y),nil))	(20)
  if_minsort(false,add(n,x),y)	→	minsort(x,add(n,y))	(21)

  could be deleted.

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