Certification Problem

Input (TPDB TRS_Equational/Mixed_C/AC45)

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.

  rm#(n,add(m,x))	→	eq#(n,m)	(13)
  purge#(add(n,x))	→	rm#(n,x)	(14)
  if_rm#(false,n,add(m,x))	→	rm#(n,x)	(15)
  purge#(add(n,x))	→	purge#(rm(n,x))	(16)
  rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(17)
  eq#(s(x),s(y))	→	eq#(x,y)	(18)
  if_rm#(true,n,add(m,x))	→	rm#(n,x)	(19)

  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 3 components.

  • The 1^st component contains the pair

    purge#(add(n,x))

    →

    purge#(rm(n,x))

    (16)

    1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [if_rm(x1, x2, x3)]	=	x1 + x2 + x3 + 20652
    [s(x1)]	=	1
    [if_rm#(x1, x2, x3)]	=	0
    [purge#(x1)]	=	x1 + 0
    [eq(x1, x2)]	=	1
    [false]	=	1
    [true]	=	1
    [purge(x1)]	=	0
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	10803
    [add(x1, x2)]	=	x1 + x2 + 20654
    [rm(x1, x2)]	=	x1 + x2 + 20653
    [rm#(x1, x2)]	=	0

    together with the usable rules

    eq(s(x),s(y))	→	eq(x,y)	(4)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(8)
    eq(0,0)	→	true	(1)
    eq(s(x),0)	→	false	(3)
    rm(n,nil)	→	nil	(5)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(7)
    eq(x,y)	→	eq(y,x)	(11)
    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(6)
    eq(0,s(x))	→	false	(2)

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

    purge#(add(n,x))

    →

    purge#(rm(n,x))

    (16)

    could be deleted.

    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)	(19)
    rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(17)
    if_rm#(false,n,add(m,x))	→	rm#(n,x)	(15)

    1.1.2 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [if_rm(x1, x2, x3)]	=	x1 + x2 + x3 + 20652
    [s(x1)]	=	1
    [if_rm#(x1, x2, x3)]	=	x1 + x2 + x3 + 0
    [purge#(x1)]	=	x1 + 0
    [eq(x1, x2)]	=	1
    [false]	=	1
    [true]	=	1
    [purge(x1)]	=	0
    [eq#(x1, x2)]	=	0
    [0]	=	1
    [nil]	=	33954
    [add(x1, x2)]	=	x2 + 3
    [rm(x1, x2)]	=	x1 + x2 + 20653
    [rm#(x1, x2)]	=	x1 + x2 + 3

    together with the usable rules

    eq(s(x),s(y))	→	eq(x,y)	(4)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(8)
    eq(0,0)	→	true	(1)
    eq(s(x),0)	→	false	(3)
    rm(n,nil)	→	nil	(5)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(7)
    eq(x,y)	→	eq(y,x)	(11)
    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(6)
    eq(0,s(x))	→	false	(2)

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

    if_rm#(false,n,add(m,x))	→	rm#(n,x)	(15)
    rm#(n,add(m,x))	→	if_rm#(eq(n,m),n,add(m,x))	(17)
    if_rm#(true,n,add(m,x))	→	rm#(n,x)	(19)

    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

    eq#(s(x),s(y))	→	eq#(x,y)	(18)
    eq#(x,y)	→	eq#(y,x)	(12)

    1.1.3 AC Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [if_rm(x1, x2, x3)]	=	x1 + x2 + x3 + 20652
    [s(x1)]	=	x1 + 1
    [if_rm#(x1, x2, x3)]	=	x1 + 0
    [purge#(x1)]	=	x1 + 0
    [eq(x1, x2)]	=	1
    [false]	=	1
    [true]	=	1
    [purge(x1)]	=	0
    [eq#(x1, x2)]	=	x1 + x2 + 0
    [0]	=	1
    [nil]	=	33954
    [add(x1, x2)]	=	x2 + 3
    [rm(x1, x2)]	=	x1 + x2 + 20653
    [rm#(x1, x2)]	=	3

    together with the usable rules

    eq(s(x),s(y))	→	eq(x,y)	(4)
    if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(8)
    eq(0,0)	→	true	(1)
    eq(s(x),0)	→	false	(3)
    rm(n,nil)	→	nil	(5)
    if_rm(true,n,add(m,x))	→	rm(n,x)	(7)
    eq(x,y)	→	eq(y,x)	(11)
    rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(6)
    eq(0,s(x))	→	false	(2)

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

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

    →

    eq#(x,y)

    (18)

    could be deleted.

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

      (12)

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