Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z091)

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

• The 1^st component contains the pair

  b#(ql(1(x1)))	→	b#(r1(x1))	(39)
  b#(ql(0(x1)))	→	b#(r0(x1))	(36)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [b#(x1)]	=	1 · x1
  [ql(x1)]	=	1 · x1
  [1(x1)]	=	1 + 1 · x1
  [r1(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [r0(x1)]	=	1 · x1
  [m(x1)]	=	1
  [b(x1)]	=	0
  [qr(x1)]	=	0

  together with the usable rules

  r1(0(x1))	→	0(r1(x1))	(4)
  r1(1(x1))	→	1(r1(x1))	(5)
  r1(m(x1))	→	m(r1(x1))	(6)
  r1(b(x1))	→	qr(1(b(x1)))	(8)
  r0(0(x1))	→	0(r0(x1))	(1)
  r0(1(x1))	→	1(r0(x1))	(2)
  r0(m(x1))	→	m(r0(x1))	(3)
  r0(b(x1))	→	qr(0(b(x1)))	(7)
  1(qr(x1))	→	qr(1(x1))	(10)
  1(ql(x1))	→	ql(1(x1))	(13)
  0(qr(x1))	→	qr(0(x1))	(9)
  0(ql(x1))	→	ql(0(x1))	(12)
  m(qr(x1))	→	ql(m(x1))	(11)

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

  b#(ql(1(x1)))

  →

  b#(r1(x1))

  (39)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [b#(x1)]	=	1 · x1
  [ql(x1)]	=	1 · x1
  [0(x1)]	=	1 + 1 · x1
  [r0(x1)]	=	1 · x1
  [1(x1)]	=	0
  [m(x1)]	=	1
  [b(x1)]	=	0
  [qr(x1)]	=	0
  [r1(x1)]	=	0

  together with the usable rules

  r0(0(x1))	→	0(r0(x1))	(1)
  r0(1(x1))	→	1(r0(x1))	(2)
  r0(m(x1))	→	m(r0(x1))	(3)
  r0(b(x1))	→	qr(0(b(x1)))	(7)
  1(qr(x1))	→	qr(1(x1))	(10)
  1(ql(x1))	→	ql(1(x1))	(13)
  0(qr(x1))	→	qr(0(x1))	(9)
  0(ql(x1))	→	ql(0(x1))	(12)
  m(qr(x1))	→	ql(m(x1))	(11)

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

  b#(ql(0(x1)))

  →

  b#(r0(x1))

  (36)

  could be deleted.

  1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  r0#(1(x1))	→	r0#(x1)	(19)
  r0#(0(x1))	→	r0#(x1)	(17)
  r0#(m(x1))	→	r0#(x1)	(21)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [1(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [m(x1)]	=	1 · x1
  [r0#(x1)]	=	1 · x1

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

  1.1.2.1 Size-Change Termination

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

  r0#(1(x1))	→	r0#(x1)	(19)
  1	>	1
  r0#(0(x1))	→	r0#(x1)	(17)
  1	>	1
  r0#(m(x1))	→	r0#(x1)	(21)
  1	>	1

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

• The 3^rd component contains the pair

  r1#(1(x1))	→	r1#(x1)	(25)
  r1#(0(x1))	→	r1#(x1)	(23)
  r1#(m(x1))	→	r1#(x1)	(27)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [1(x1)]	=	1 · x1
  [0(x1)]	=	1 · x1
  [m(x1)]	=	1 · x1
  [r1#(x1)]	=	1 · x1

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

  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.

  r1#(1(x1))	→	r1#(x1)	(25)
  1	>	1
  r1#(0(x1))	→	r1#(x1)	(23)
  1	>	1
  r1#(m(x1))	→	r1#(x1)	(27)
  1	>	1

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

• The 4^th component contains the pair

  0#(ql(x1))	→	0#(x1)	(33)
  0#(qr(x1))	→	0#(x1)	(30)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ql(x1)]	=	1 · x1
  [qr(x1)]	=	1 · x1
  [0#(x1)]	=	1 · x1

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

  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.

  0#(ql(x1))	→	0#(x1)	(33)
  1	>	1
  0#(qr(x1))	→	0#(x1)	(30)
  1	>	1

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

• The 5^th component contains the pair

  1#(ql(x1))	→	1#(x1)	(34)
  1#(qr(x1))	→	1#(x1)	(31)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ql(x1)]	=	1 · x1
  [qr(x1)]	=	1 · x1
  [1#(x1)]	=	1 · x1

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

  1.1.5.1 Size-Change Termination

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

  1#(ql(x1))	→	1#(x1)	(34)
  1	>	1
  1#(qr(x1))	→	1#(x1)	(31)
  1	>	1

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

• The 6^th component contains the pair

  m#(qr(x1))

  →

  m#(x1)

  (32)

  1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [qr(x1)]	=	1 · x1
  [m#(x1)]	=	1 · x1

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

  1.1.6.1 Size-Change Termination

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

  m#(qr(x1))	→	m#(x1)	(32)
  1	>	1

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