Certification Problem

Input (TPDB TRS_Equational/Mixed_C/AC42)

The rewrite relation of the following equational TRS is considered.

Commutative symbols: gcd

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

• The 1^st component contains the pair

  gcd#(s(x),s(y))	→	if_gcd#(le(y,x),s(x),s(y))	(17)
  if_gcd#(true,s(x),s(y))	→	gcd#(minus(x,y),s(y))	(19)
  gcd#(x,y)	→	gcd#(y,x)	(13)
  if_gcd#(false,s(x),s(y))	→	gcd#(minus(y,x),s(x))	(21)

  1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [if_gcd#(x1, x2, x3)]	=	1 · x2 + 1 · x3
  [false]	=	0
  [s(x1)]	=	1 + 1 · x1
  [gcd#(x1, x2)]	=	1 · x1 + 1 · x2
  [minus(x1, x2)]	=	1 · x1
  [le(x1, x2)]	=	0
  [true]	=	0
  [pred(x1)]	=	1 · x1
  [0]	=	0

  together with the usable rules

  minus(x,s(y))	→	pred(minus(x,y))	(6)
  minus(x,0)	→	x	(5)
  pred(s(x))	→	x	(4)

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

  if_gcd#(false,s(x),s(y))	→	gcd#(minus(y,x),s(x))	(21)
  if_gcd#(true,s(x),s(y))	→	gcd#(minus(x,y),s(y))	(19)

  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

    gcd#(x,y)

    →

    gcd#(y,x)

    (13)

    1.1.1.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 2^nd component contains the pair

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

  →

  le#(x,y)

  (14)

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

  (14)

  and the rules

  le(0,y)	→	true	(1)
  le(s(x),0)	→	false	(2)
  le(s(x),s(y))	→	le(x,y)	(3)
  pred(s(x))	→	x	(4)
  minus(x,0)	→	x	(5)
  minus(x,s(y))	→	pred(minus(x,y))	(6)
  gcd(0,y)	→	y	(7)
  gcd(s(x),0)	→	s(x)	(8)
  gcd(s(x),s(y))	→	if_gcd(le(y,x),s(x),s(y))	(9)
  if_gcd(true,s(x),s(y))	→	gcd(minus(x,y),s(y))	(10)
  if_gcd(false,s(x),s(y))	→	gcd(minus(y,x),s(x))	(11)

  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

  minus#(x,s(y))

  →

  minus#(x,y)

  (16)

  1.1.3 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  minus#(x,s(y))

  →

  minus#(x,y)

  (16)

  and the rules

  le(0,y)	→	true	(1)
  le(s(x),0)	→	false	(2)
  le(s(x),s(y))	→	le(x,y)	(3)
  pred(s(x))	→	x	(4)
  minus(x,0)	→	x	(5)
  minus(x,s(y))	→	pred(minus(x,y))	(6)
  gcd(0,y)	→	y	(7)
  gcd(s(x),0)	→	s(x)	(8)
  gcd(s(x),s(y))	→	if_gcd(le(y,x),s(x),s(y))	(9)
  if_gcd(true,s(x),s(y))	→	gcd(minus(x,y),s(y))	(10)
  if_gcd(false,s(x),s(y))	→	gcd(minus(y,x),s(x))	(11)

  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.