Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z091)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

1.1 Rule Removal

1.1.1 Rule Removal

1.1.1.1 Dependency Pair Transformation

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

• The 1^st component contains the pair

  ql#(1(x1))	→	ql#(x1)	(48)
  ql#(1(x1))	→	1#(ql(x1))	(49)
  1#(ql(b(x1)))	→	b#(1(x1))	(51)
  b#(r1(x1))	→	b#(1(qr(x1)))	(40)
  b#(r1(x1))	→	1#(qr(x1))	(39)
  1#(r1(x1))	→	1#(x1)	(34)
  1#(ql(b(x1)))	→	1#(x1)	(50)
  1#(r0(x1))	→	1#(x1)	(32)
  b#(r1(x1))	→	qr#(x1)	(38)
  qr#(m(x1))	→	ql#(x1)	(45)
  ql#(0(x1))	→	ql#(x1)	(46)
  qr#(1(x1))	→	1#(qr(x1))	(44)
  qr#(1(x1))	→	qr#(x1)	(43)
  qr#(0(x1))	→	qr#(x1)	(41)
  b#(r0(x1))	→	b#(0(qr(x1)))	(37)
  b#(r0(x1))	→	qr#(x1)	(35)

  1.1.1.1.1.1 Subterm Criterion Processor

  We use the projection to multisets

  π(ql#)	=	{ 1, 1 }
  π(qr#)	=	{ 1, 1 }
  π(b#)	=	{ 1, 1 }
  π(1#)	=	{ 1, 1 }
  π(ql)	=	{ 1 }
  π(qr)	=	{ 1 }
  π(b)	=	{ 1 }
  π(r1)	=	{ 1 }
  π(m)	=	{ 1 }
  π(1)	=	{ 1 }
  π(r0)	=	{ 1, 1, 1 }
  π(0)	=	{ 1, 1 }

  to remove the pairs:

  1#(r0(x1))	→	1#(x1)	(32)
  ql#(0(x1))	→	ql#(x1)	(46)
  qr#(0(x1))	→	qr#(x1)	(41)
  b#(r0(x1))	→	b#(0(qr(x1)))	(37)
  b#(r0(x1))	→	qr#(x1)	(35)

  1.1.1.1.1.1.1 Subterm Criterion Processor

  We use the projection to multisets

  π(ql#)	=	{ 1, 1 }
  π(qr#)	=	{ 1, 1 }
  π(b#)	=	{ 1, 1 }
  π(1#)	=	{ 1 }
  π(ql)	=	{ 1, 1 }
  π(qr)	=	{ 1, 1 }
  π(b)	=	{ 1 }
  π(r1)	=	{ 1, 1 }
  π(m)	=	{ 1 }
  π(1)	=	{ 1 }
  π(r0)	=	{ 1, 1 }
  π(0)	=	{ 1 }

  to remove the pairs:

  b#(r1(x1))	→	1#(qr(x1))	(39)
  1#(r1(x1))	→	1#(x1)	(34)
  1#(ql(b(x1)))	→	1#(x1)	(50)
  b#(r1(x1))	→	qr#(x1)	(38)

  1.1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 3 components.

  • The 1^st component contains the pair

    qr#(1(x1))

    →

    qr#(x1)

    (43)

    1.1.1.1.1.1.1.1.1 Size-Change Termination

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

    qr#(1(x1))	→	qr#(x1)	(43)
    1	>	1

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

  • The 2^nd component contains the pair

    ql#(1(x1))

    →

    ql#(x1)

    (48)

    1.1.1.1.1.1.1.1.2 Size-Change Termination

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

    ql#(1(x1))	→	ql#(x1)	(48)
    1	>	1

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

  • The 3^rd component contains the pair

    b#(r1(x1))

    →

    b#(1(qr(x1)))

    (40)

    1.1.1.1.1.1.1.1.3 Reduction Pair Processor with Usable Rules

    Using the

    prec(b#)	=	0		stat(b#)	=	lex
    prec(ql)	=	1		stat(ql)	=	lex
    prec(qr)	=	0		stat(qr)	=	lex
    prec(b)	=	0		stat(b)	=	lex
    prec(r1)	=	0		stat(r1)	=	lex
    prec(m)	=	0		stat(m)	=	lex
    prec(1)	=	0		stat(1)	=	lex
    prec(r0)	=	0		stat(r0)	=	lex
    prec(0)	=	0		stat(0)	=	lex

    π(b#)	=	1
    π(ql)	=	[]
    π(qr)	=	1
    π(b)	=	[]
    π(r1)	=	[1]
    π(m)	=	[]
    π(1)	=	1
    π(r0)	=	1
    π(0)	=	1

    together with the usable rules

    0(r0(x1))	→	r0(0(x1))	(16)
    1(r0(x1))	→	r0(1(x1))	(17)
    0(r1(x1))	→	r1(0(x1))	(19)
    1(r1(x1))	→	r1(1(x1))	(20)
    b(r0(x1))	→	b(0(qr(x1)))	(22)
    b(r1(x1))	→	b(1(qr(x1)))	(23)
    qr(0(x1))	→	0(qr(x1))	(24)
    qr(1(x1))	→	1(qr(x1))	(25)
    qr(m(x1))	→	m(ql(x1))	(26)
    1(ql(b(x1)))	→	r1(b(1(x1)))	(30)

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

    b#(r1(x1))

    →

    b#(1(qr(x1)))

    (40)

    could be deleted.

    1.1.1.1.1.1.1.1.3.1 P is empty

    There are no pairs anymore.

• The 2^nd component contains the pair

  0#(r1(x1))	→	0#(x1)	(33)
  0#(r0(x1))	→	0#(x1)	(31)

  1.1.1.1.1.2 Size-Change Termination

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

  0#(r1(x1))	→	0#(x1)	(33)
  1	>	1
  0#(r0(x1))	→	0#(x1)	(31)
  1	>	1

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