Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/3)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ 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

  f#(g(s(x),y))	→	f#(g(x,s(y)))	(14)
  f#(s(x))	→	f#(h(s(x)))	(12)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [h(x1)]	=	1 · x1
  [g(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	1 · x1
  [f(x1)]	=	1 · x1
  [a]	=	0
  [b]	=	0
  [i(x1, x2)]	=	1 · x1 + 1 · x2
  [c]	=	0
  [f#(x1)]	=	1 · x1

  together with the usable rules

  h(g(x,s(y)))	→	h(g(s(x),y))	(6)
  h(s(f(x)))	→	h(f(x))	(3)
  g(x,x)	→	g(a,b)	(2)
  h(i(x,y))	→	i(i(c,h(h(y))),x)	(7)
  f(s(x))	→	s(s(f(h(s(x)))))	(4)
  f(g(s(x),y))	→	f(g(x,s(y)))	(5)
  i(x,x)	→	i(a,b)	(1)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

  prec(g)	=	3		weight(g)	=	2
  prec(s)	=	2		weight(s)	=	1
  prec(h)	=	1		weight(h)	=	1
  prec(i)	=	0		weight(i)	=	1

  in combination with the following argument filter

  π(f#)	=	1
  π(g)	=	[]
  π(s)	=	[]
  π(h)	=	[]
  π(i)	=	[]

  together with the usable rules

  g(x,x)	→	g(a,b)	(2)
  h(s(f(x)))	→	h(f(x))	(3)
  h(g(x,s(y)))	→	h(g(s(x),y))	(6)
  h(i(x,y))	→	i(i(c,h(h(y))),x)	(7)
  i(x,x)	→	i(a,b)	(1)

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

  f#(s(x))

  →

  f#(h(s(x)))

  (12)

  could be deleted.

  1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [g(x1, x2)]	=	1 · x1 + 1 · x2
  [a]	=	0
  [b]	=	0
  [s(x1)]	=	1 · x1
  [f#(x1)]	=	1 · x1

  together with the usable rule

  g(x,x)

  →

  g(a,b)

  (2)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [g(x1, x2)]	=	2 · x1 + 1 · x2
  [a]	=	0
  [b]	=	0
  [f#(x1)]	=	1 · x1
  [s(x1)]	=	1 + 1 · x1

  the pair

  f#(g(s(x),y))

  →

  f#(g(x,s(y)))

  (14)

  and no rules could be deleted.

  1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  h#(g(x,s(y)))	→	h#(g(s(x),y))	(16)
  h#(s(f(x)))	→	h#(f(x))	(11)
  h#(i(x,y))	→	h#(h(y))	(20)
  h#(i(x,y))	→	h#(y)	(21)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [h(x1)]	=	1 · x1
  [g(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	1 · x1
  [f(x1)]	=	1 · x1
  [i(x1, x2)]	=	1 · x1 + 1 · x2
  [c]	=	0
  [a]	=	0
  [b]	=	0
  [h#(x1)]	=	1 · x1

  together with the usable rules

  h(g(x,s(y)))	→	h(g(s(x),y))	(6)
  h(s(f(x)))	→	h(f(x))	(3)
  h(i(x,y))	→	i(i(c,h(h(y))),x)	(7)
  i(x,x)	→	i(a,b)	(1)
  g(x,x)	→	g(a,b)	(2)
  f(s(x))	→	s(s(f(h(s(x)))))	(4)
  f(g(s(x),y))	→	f(g(x,s(y)))	(5)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.2.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the rationals with delta = 1

  [h#(x1)]	=	0 + 4 · x1
  [g(x1, x2)]	=	0 + 0 · x1 + 0 · x2
  [s(x1)]	=	1/4 + 1 · x1
  [f(x1)]	=	0 + 4 · x1
  [i(x1, x2)]	=	0 + 4 · x1 + 1 · x2
  [h(x1)]	=	0 + 1/4 · x1
  [a]	=	0
  [b]	=	0
  [c]	=	0

  the pair

  h#(s(f(x)))

  →

  h#(f(x))

  (11)

  could be deleted.

  1.1.2.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

  [h#(x1)]	=	0 0 + 1 0 0 0 · x1
  [g(x1, x2)]	=	0 0 + 0 0 0 0 · x1 + 1 1 0 0 · x2
  [s(x1)]	=	0 1 + 0 1 1 0 · x1
  [i(x1, x2)]	=	0 0 + 0 0 1 1 · x1 + 1 1 0 0 · x2
  [h(x1)]	=	0 0 + 0 1 0 0 · x1
  [a]	=	0 0
  [b]	=	0 0
  [f(x1)]	=	0 0 + 0 1 0 1 · x1
  [c]	=	0 0

  the pair

  h#(g(x,s(y)))

  →

  h#(g(s(x),y))

  (16)

  could be deleted.

  1.1.2.1.1.1 Narrowing Processor

  We consider all narrowings of the pair below position 1 to get the following set of pairs

  h#(i(y0,g(x0,s(x1))))	→	h#(h(g(s(x0),x1)))	(28)
  h#(i(y0,s(f(x0))))	→	h#(h(f(x0)))	(29)
  h#(i(y0,i(x0,x1)))	→	h#(i(i(c,h(h(x1))),x0))	(30)

  1.1.2.1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

  [h#(x1)]	=	-∞ + 0 · x1
  [i(x1, x2)]	=	5 + 0 · x1 + 0 · x2
  [g(x1, x2)]	=	5 + -∞ · x1 + -∞ · x2
  [s(x1)]	=	0 + -∞ · x1
  [h(x1)]	=	4 + 0 · x1
  [f(x1)]	=	1 + -∞ · x1
  [c]	=	0
  [a]	=	0
  [b]	=	0

  the pair

  h#(i(y0,s(f(x0))))

  →

  h#(h(f(x0)))

  (29)

  could be deleted.

  1.1.2.1.1.1.1.1 Reduction Pair Processor

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals

  [h#(x1)]	=	-∞ + 0 · x1
  [i(x1, x2)]	=	2 + 0 · x1 + 0 · x2
  [g(x1, x2)]	=	0 + -∞ · x1 + -∞ · x2
  [s(x1)]	=	-∞ + 0 · x1
  [h(x1)]	=	-∞ + 0 · x1
  [c]	=	0
  [a]	=	0
  [b]	=	0
  [f(x1)]	=	-∞ + 0 · x1

  the pair

  h#(i(y0,g(x0,s(x1))))

  →

  h#(h(g(s(x0),x1)))

  (28)

  could be deleted.

  1.1.2.1.1.1.1.1.1 Split

  We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD

  There are no rules.

  and the rules RD

  g(x,x)

  →

  g(a,b)

  (2)

  are deleted.

  1.1.2.1.1.1.1.1.1.1 Semantic Labeling Processor

  The following interpretations form a model of the rules.

  As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):

  [s(x1)]	=	0
  [a]	=	1
  [b]	=	1
  [c]	=	0
  [h#(x1)]	=	0
  [f(x1)]	=	0
  [i(x1, x2)]	=	0
  [h(x1)]	=	0
  [g(x1, x2)]	=	0

  We obtain the set of labeled pairs

  h#0(i00(x,y))	→	h#0(y)	(31)
  h#0(i01(x,y))	→	h#1(y)	(32)
  h#0(i10(x,y))	→	h#0(y)	(33)
  h#0(i11(x,y))	→	h#1(y)	(34)
  h#0(i00(y0,i00(x0,x1)))	→	h#0(i00(i00(c,h0(h0(x1))),x0))	(35)
  h#0(i00(y0,i01(x0,x1)))	→	h#0(i00(i00(c,h0(h1(x1))),x0))	(36)
  h#0(i00(y0,i10(x0,x1)))	→	h#0(i01(i00(c,h0(h0(x1))),x0))	(37)
  h#0(i00(y0,i11(x0,x1)))	→	h#0(i01(i00(c,h0(h1(x1))),x0))	(38)
  h#0(i10(y0,i00(x0,x1)))	→	h#0(i00(i00(c,h0(h0(x1))),x0))	(39)
  h#0(i10(y0,i01(x0,x1)))	→	h#0(i00(i00(c,h0(h1(x1))),x0))	(40)
  h#0(i10(y0,i10(x0,x1)))	→	h#0(i01(i00(c,h0(h0(x1))),x0))	(41)
  h#0(i10(y0,i11(x0,x1)))	→	h#0(i01(i00(c,h0(h1(x1))),x0))	(42)

  and the set of labeled rules:

  h0(g00(x,s0(y)))	→	h0(g00(s0(x),y))	(43)
  h0(g00(x,s1(y)))	→	h0(g01(s0(x),y))	(44)
  h0(g10(x,s0(y)))	→	h0(g00(s1(x),y))	(45)
  h0(g10(x,s1(y)))	→	h0(g01(s1(x),y))	(46)
  h0(s0(f0(x)))	→	h0(f0(x))	(47)
  h0(s0(f1(x)))	→	h0(f1(x))	(48)
  h0(i00(x,y))	→	i00(i00(c,h0(h0(y))),x)	(49)
  h0(i01(x,y))	→	i00(i00(c,h0(h1(y))),x)	(50)
  h0(i10(x,y))	→	i01(i00(c,h0(h0(y))),x)	(51)
  h0(i11(x,y))	→	i01(i00(c,h0(h1(y))),x)	(52)
  i00(x,x)	→	i11(a,b)	(53)
  i11(x,x)	→	i11(a,b)	(54)
  g00(x,x)	→	g11(a,b)	(55)
  g11(x,x)	→	g11(a,b)	(56)
  f0(s0(x))	→	s0(s0(f0(h0(s0(x)))))	(57)
  f0(s1(x))	→	s0(s0(f0(h0(s1(x)))))	(58)
  f0(g00(s0(x),y))	→	f0(g00(x,s0(y)))	(59)
  f0(g01(s0(x),y))	→	f0(g00(x,s1(y)))	(60)
  f0(g00(s1(x),y))	→	f0(g10(x,s0(y)))	(61)
  f0(g01(s1(x),y))	→	f0(g10(x,s1(y)))	(62)

  1.1.2.1.1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    h#0(i00(x,y))	→	h#0(y)	(31)
    h#0(i10(x,y))	→	h#0(y)	(33)
    h#0(i00(y0,i00(x0,x1)))	→	h#0(i00(i00(c,h0(h0(x1))),x0))	(35)
    h#0(i00(y0,i01(x0,x1)))	→	h#0(i00(i00(c,h0(h1(x1))),x0))	(36)
    h#0(i10(y0,i00(x0,x1)))	→	h#0(i00(i00(c,h0(h0(x1))),x0))	(39)
    h#0(i10(y0,i01(x0,x1)))	→	h#0(i00(i00(c,h0(h1(x1))),x0))	(40)

    1.1.2.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [i00(x1, x2)]	=	1 · x1 + 1 · x2
    [i11(x1, x2)]	=	1 · x1 + 1 · x2
    [a]	=	0
    [b]	=	0
    [h0(x1)]	=	1 · x1
    [g10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [s0(x1)]	=	1 · x1
    [g00(x1, x2)]	=	1 · x1 + 1 · x2
    [s1(x1)]	=	1 + 1 · x1
    [f0(x1)]	=	1 · x1
    [g01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f1(x1)]	=	1 · x1
    [c]	=	0
    [i01(x1, x2)]	=	1 · x1 + 1 · x2
    [h1(x1)]	=	1 · x1
    [i10(x1, x2)]	=	1 · x1 + 1 · x2
    [g11(x1, x2)]	=	1 · x1 + 1 · x2
    [h#0(x1)]	=	1 · x1

    together with the usable rules

    i00(x,x)	→	i11(a,b)	(53)
    h0(g10(x,s0(y)))	→	h0(g00(s1(x),y))	(45)
    h0(g00(x,s0(y)))	→	h0(g00(s0(x),y))	(43)
    h0(s0(f0(x)))	→	h0(f0(x))	(47)
    h0(g00(x,s1(y)))	→	h0(g01(s0(x),y))	(44)
    h0(g10(x,s1(y)))	→	h0(g01(s1(x),y))	(46)
    h0(s0(f1(x)))	→	h0(f1(x))	(48)
    h0(i00(x,y))	→	i00(i00(c,h0(h0(y))),x)	(49)
    h0(i01(x,y))	→	i00(i00(c,h0(h1(y))),x)	(50)
    h0(i10(x,y))	→	i01(i00(c,h0(h0(y))),x)	(51)
    h0(i11(x,y))	→	i01(i00(c,h0(h1(y))),x)	(52)
    g00(x,x)	→	g11(a,b)	(55)
    f0(s0(x))	→	s0(s0(f0(h0(s0(x)))))	(57)
    f0(s1(x))	→	s0(s0(f0(h0(s1(x)))))	(58)
    f0(g01(s0(x),y))	→	f0(g00(x,s1(y)))	(60)
    f0(g00(s0(x),y))	→	f0(g00(x,s0(y)))	(59)
    f0(g00(s1(x),y))	→	f0(g10(x,s0(y)))	(61)
    f0(g01(s1(x),y))	→	f0(g10(x,s1(y)))	(62)

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

    h#0(i10(x,y))	→	h#0(y)	(33)
    h#0(i10(y0,i00(x0,x1)))	→	h#0(i00(i00(c,h0(h0(x1))),x0))	(39)
    h#0(i10(y0,i01(x0,x1)))	→	h#0(i00(i00(c,h0(h1(x1))),x0))	(40)

    and the rule

    h0(i10(x,y))

    →

    i01(i00(c,h0(h0(y))),x)

    (51)

    could be deleted.

    1.1.2.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [i00(x1, x2)]	=	1 · x1 + 1 · x2
    [i11(x1, x2)]	=	1 · x1 + 1 · x2
    [a]	=	0
    [b]	=	0
    [h0(x1)]	=	1 · x1
    [g10(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [s0(x1)]	=	1 · x1
    [g00(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [s1(x1)]	=	1 · x1
    [f0(x1)]	=	1 · x1
    [g01(x1, x2)]	=	1 + 1 · x1 + 1 · x2
    [f1(x1)]	=	1 · x1
    [c]	=	0
    [i01(x1, x2)]	=	1 · x1 + 1 · x2
    [h1(x1)]	=	1 · x1
    [g11(x1, x2)]	=	1 · x1 + 1 · x2
    [h#0(x1)]	=	1 · x1

    the rule

    g00(x,x)

    →

    g11(a,b)

    (55)

    could be deleted.

    1.1.2.1.1.1.1.1.1.1.1.1.1.1 P is empty

    There are no pairs anymore.

  1.1.2.1.1.1.1.1.1.2 Reduction Pair Processor

  Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers

  [h#(x1)]	=	2 0 + 1 0 0 0 · x1
  [i(x1, x2)]	=	2 2 + 0 0 1 1 · x1 + 1 1 0 0 · x2
  [c]	=	0 0
  [h(x1)]	=	0 0 + 0 1 3 0 · x1
  [g(x1, x2)]	=	0 0 + 0 0 0 0 · x1 + 2 3 1 2 · x2
  [s(x1)]	=	0 0 + 0 2 2 3 · x1
  [f(x1)]	=	0 0 + 0 0 0 0 · x1
  [a]	=	0 0
  [b]	=	0 0

  the pairs

  h#(i(x,y))	→	h#(y)	(21)
  h#(i(y0,i(x0,x1)))	→	h#(i(i(c,h(h(x1))),x0))	(30)

  could be deleted.

  1.1.2.1.1.1.1.1.1.2.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(a,g(x,g(b,g(b,y))))	(24)
  g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(a,g(a,g(x,g(b,g(b,y)))))	(23)
  g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(x,g(b,g(b,y)))	(25)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [g(x1, x2)]	=	1 · x1 + 1 · x2
  [a]	=	0
  [b]	=	0
  [g#(x1, x2)]	=	1 · x1 + 1 · x2

  together with the usable rules

  g(x,x)	→	g(a,b)	(2)
  g(a,g(x,g(b,g(a,g(x,y)))))	→	g(a,g(a,g(a,g(x,g(b,g(b,y))))))	(8)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.3.1 Narrowing Processor

  We consider all narrowings of the pair below position 2 to get the following set of pairs

  g#(a,g(g(b,g(b,y1)),g(b,g(a,g(g(b,g(b,y1)),y1)))))	→	g#(a,g(a,b))	(63)
  g#(a,g(a,g(b,g(a,g(a,g(a,g(b,x1)))))))	→	g#(a,g(a,g(a,g(a,g(b,g(b,g(b,x1)))))))	(64)
  g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(y0,g(b,g(a,b))))	(65)

  1.1.3.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(x,g(b,g(b,y)))	(25)
    g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(a,g(a,g(x,g(b,g(b,y)))))	(23)
    g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(y0,g(b,g(a,b))))	(65)

    1.1.3.1.1.1 Narrowing Processor

    We consider all narrowings of the pair below position 2 to get the following set of pairs

    g#(a,g(g(b,g(b,y1)),g(b,g(a,g(g(b,g(b,y1)),y1)))))	→	g#(a,g(a,g(a,b)))	(66)
    g#(a,g(a,g(b,g(a,g(a,g(a,g(b,x1)))))))	→	g#(a,g(a,g(a,g(a,g(a,g(b,g(b,g(b,x1))))))))	(67)
    g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(a,g(y0,g(b,g(a,b)))))	(68)

    1.1.3.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      g#(a,g(x,g(b,g(a,g(x,y)))))	→	g#(x,g(b,g(b,y)))	(25)
      g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(y0,g(b,g(a,b))))	(65)
      g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(a,g(y0,g(b,g(a,b)))))	(68)

      1.1.3.1.1.1.1.1 Forward Instantiation Processor

      We instantiate the pair to the following set of pairs

      g#(a,g(a,g(b,g(a,g(a,x1)))))

      →

      g#(a,g(b,g(b,x1)))

      (69)

      1.1.3.1.1.1.1.1.1 Forward Instantiation Processor

      We instantiate the pair to the following set of pairs

      g#(a,g(b,g(b,g(a,g(b,b)))))

      →

      g#(a,g(a,g(b,g(b,g(a,b)))))

      (70)

      1.1.3.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(y0,g(b,g(a,b))))	(65)
        g#(a,g(a,g(b,g(a,g(a,x1)))))	→	g#(a,g(b,g(b,x1)))	(69)

        1.1.3.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

        Using the linear polynomial interpretation over the naturals

        [g(x1, x2)]	=	1 · x1 + 1 · x2
        [a]	=	0
        [b]	=	0
        [g#(x1, x2)]	=	1 · x1 + 1 · x2

        together with the usable rule

        g(x,x)

        →

        g(a,b)

        (2)

        (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

        1.1.3.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

        Using the linear polynomial interpretation over the naturals

        [g(x1, x2)]	=	2 + 1 · x1 + 2 · x2
        [a]	=	0
        [b]	=	0
        [g#(x1, x2)]	=	1 · x1 + 1 · x2

        the pairs

        g#(a,g(y0,g(b,g(a,g(y0,b)))))	→	g#(a,g(y0,g(b,g(a,b))))	(65)
        g#(a,g(a,g(b,g(a,g(a,x1)))))	→	g#(a,g(b,g(b,x1)))	(69)

        and no rules could be deleted.

        1.1.3.1.1.1.1.1.1.1.1.1.1 P is empty

        There are no pairs anymore.