Certification Problem

Input (TPDB SRS_Standard/Secret_05_SRS/aprove4)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  log#(s(x1))

  →

  log#(half(s(x1)))

  (10)

  1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [p(x1)]	=	1 · x1
  [half(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [log#(x1)]	=	1 · x1

  together with the usable rules

  s(s(p(s(x1))))	→	s(s(x1))	(7)
  half(0(x1))	→	0(s(s(half(x1))))	(2)
  half(s(0(x1)))	→	0(x1)	(3)
  half(s(s(x1)))	→	s(half(p(s(s(x1)))))	(4)
  half(half(s(s(s(s(x1))))))	→	s(s(half(half(x1))))	(5)
  p(s(s(s(x1))))	→	s(p(s(s(x1))))	(6)

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

  1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [log#(x1)]	=	2 + x1
  [s(x1)]	=	1 + x1
  [p(x1)]	=	-1 + x1
  [half(x1)]	=	-1 + x1
  [0(x1)]	=	-2

  the pair

  log#(s(x1))

  →

  log#(half(s(x1)))

  (10)

  could be deleted.

  1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  half#(s(s(x1)))	→	half#(p(s(s(x1))))	(16)
  half#(0(x1))	→	half#(x1)	(14)
  half#(half(s(s(s(s(x1))))))	→	half#(half(x1))	(20)
  half#(half(s(s(s(s(x1))))))	→	half#(x1)	(21)

  1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [half(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [p(x1)]	=	1 · x1
  [half#(x1)]	=	1 · x1

  together with the usable rules

  half(0(x1))	→	0(s(s(half(x1))))	(2)
  half(s(0(x1)))	→	0(x1)	(3)
  half(s(s(x1)))	→	s(half(p(s(s(x1)))))	(4)
  half(half(s(s(s(s(x1))))))	→	s(s(half(half(x1))))	(5)
  s(s(p(s(x1))))	→	s(s(x1))	(7)
  p(s(s(s(x1))))	→	s(p(s(s(x1))))	(6)

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

  1.1.1.2.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [half#(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [p(x1)]	=	1 · x1
  [0(x1)]	=	1 + 1 · x1
  [half(x1)]	=	1 · x1

  the pair

  half#(0(x1))

  →

  half#(x1)

  (14)

  could be deleted.

  1.1.1.2.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    half#(half(s(s(s(s(x1))))))	→	half#(x1)	(21)
    half#(half(s(s(s(s(x1))))))	→	half#(half(x1))	(20)

    1.1.1.2.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [half#(x1)]	=	1 · x1
    [half(x1)]	=	1 + 1 · x1
    [s(x1)]	=	1 · x1
    [0(x1)]	=	1 + 1 · x1
    [p(x1)]	=	1 · x1

    the pair

    half#(half(s(s(s(s(x1))))))

    →

    half#(x1)

    (21)

    could be deleted.

    1.1.1.2.1.1.1.1 Monotonic Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [half(x1)]	=	2 · x1
    [0(x1)]	=	1 + 2 · x1
    [s(x1)]	=	1 · x1
    [p(x1)]	=	1 · x1
    [half#(x1)]	=	1 · x1

    the rules

    half(0(x1))	→	0(s(s(half(x1))))	(2)
    half(s(0(x1)))	→	0(x1)	(3)

    could be deleted.

    1.1.1.2.1.1.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [half#(x1)]	=	-2 + 2 · x1
    [half(x1)]	=	-2 + 2 · x1
    [s(x1)]	=	2 + x1
    [p(x1)]	=	-2 + x1

    the pair

    half#(half(s(s(s(s(x1))))))

    →

    half#(half(x1))

    (20)

    could be deleted.

    1.1.1.2.1.1.1.1.1.1 P is empty

    There are no pairs anymore.

  • The 2^nd component contains the pair

    half#(s(s(x1)))

    →

    half#(p(s(s(x1))))

    (16)

    1.1.1.2.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [s(x1)]	=	1 · x1
    [p(x1)]	=	1 · x1
    [half#(x1)]	=	1 · x1

    together with the usable rules

    s(s(p(s(x1))))	→	s(s(x1))	(7)
    p(s(s(s(x1))))	→	s(p(s(s(x1))))	(6)

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

    1.1.1.2.1.1.2.1 Monotonic Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [s(x1)]	=	2 + 2 · x1
    [p(x1)]	=	1 · x1
    [half#(x1)]	=	1 · x1

    the rule

    s(s(p(s(x1))))

    →

    s(s(x1))

    (7)

    could be deleted.

    1.1.1.2.1.1.2.1.1 Switch to Innermost Termination

    The TRS does not have overlaps with the pairs and is locally confluent:

    20

    Hence, it suffices to show innermost termination in the following.

    1.1.1.2.1.1.2.1.1.1 Reduction Pair Processor

    Using the linear polynomial interpretation over the naturals

    [half#(x1)]	=	-2 + 2 · x1
    [p(x1)]	=	-2 + x1
    [s(x1)]	=	1 + 2 · x1

    the pair

    half#(s(s(x1)))

    →

    half#(p(s(s(x1))))

    (16)

    could be deleted.

    1.1.1.2.1.1.2.1.1.1.1 P is empty

    There are no pairs anymore.

• The 3^rd component contains the pair

  p#(s(s(s(x1))))

  →

  p#(s(s(x1)))

  (23)

  1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [p(x1)]	=	1 · x1
  [p#(x1)]	=	1 · x1

  together with the usable rule

  s(s(p(s(x1))))

  →

  s(s(x1))

  (7)

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

  1.1.1.3.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  p#(s(s(s(x1))))	→	p#(s(s(x1)))	(23)
  1	>	1

  As there is no critical graph in the transitive closure, there are no infinite chains.

• The 4^th component contains the pair

  s#(s(p(s(x1))))

  →

  s#(s(x1))

  (24)

  1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [s(x1)]	=	1 · x1
  [p(x1)]	=	1 · x1
  [s#(x1)]	=	1 · x1

  together with the usable rule

  s(s(p(s(x1))))

  →

  s(s(x1))

  (7)

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

  1.1.1.4.1 Size-Change Termination

  Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

  s#(s(p(s(x1))))	→	s#(s(x1))	(24)
  1	>	1

  As there is no critical graph in the transitive closure, there are no infinite chains.