Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nosorts_noand_C)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

1.1 Rule Removal

1.1.1 Rule Removal

1.1.1.1 Rule Removal

1.1.1.1.1 Dependency Pair Transformation

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(62)
  top#(mark(X))	→	top#(proper(X))	(60)

  1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(top#)	=	0		stat(top#)	=	lex
  prec(ok)	=	0		stat(ok)	=	lex
  prec(proper)	=	0		stat(proper)	=	lex
  prec(isNePal)	=	0		stat(isNePal)	=	lex
  prec(U12)	=	0		stat(U12)	=	lex
  prec(U11)	=	8		stat(U11)	=	lex
  prec(tt)	=	0		stat(tt)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(__)	=	1		stat(__)	=	lex

  π(top#)	=	1
  π(ok)	=	1
  π(proper)	=	1
  π(isNePal)	=	1
  π(U12)	=	1
  π(U11)	=	[1]
  π(tt)	=	[]
  π(nil)	=	[]
  π(mark)	=	[1]
  π(active)	=	1
  π(__)	=	[1,2]

  together with the usable rules

  active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
  active(__(X1,X2))	→	__(active(X1),X2)	(7)
  active(__(X1,X2))	→	__(X1,active(X2))	(8)
  active(U11(X))	→	U11(active(X))	(9)
  active(U12(X))	→	U12(active(X))	(10)
  active(isNePal(X))	→	isNePal(active(X))	(11)
  __(mark(X1),X2)	→	mark(__(X1,X2))	(12)
  __(X1,mark(X2))	→	mark(__(X1,X2))	(13)
  __(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
  U11(mark(X))	→	mark(U11(X))	(14)
  U11(ok(X))	→	ok(U11(X))	(24)
  U12(mark(X))	→	mark(U12(X))	(15)
  U12(ok(X))	→	ok(U12(X))	(25)
  isNePal(mark(X))	→	mark(isNePal(X))	(16)
  isNePal(ok(X))	→	ok(isNePal(X))	(26)
  proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(17)
  proper(nil)	→	ok(nil)	(18)
  proper(U11(X))	→	U11(proper(X))	(19)
  proper(tt)	→	ok(tt)	(20)
  proper(U12(X))	→	U12(proper(X))	(21)
  proper(isNePal(X))	→	isNePal(proper(X))	(22)

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

  top#(mark(X))

  →

  top#(proper(X))

  (60)

  could be deleted.

  1.1.1.1.1.1.1.1 Subterm Criterion Processor

  We use the projection to multisets

  π(top#)	=	{ 1 }
  π(ok)	=	{ 1, 1, 1 }
  π(isNePal)	=	{ 1, 1 }
  π(U12)	=	{ 1, 1 }
  π(U11)	=	{ 1, 1 }
  π(mark)	=	{ 1 }
  π(active)	=	{ 1, 1 }
  π(__)	=	{ 2 }

  to remove the pairs:

  top#(ok(X))

  →

  top#(active(X))

  (62)

  1.1.1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  active#(__(X1,X2))	→	active#(X1)	(31)
  active#(__(X1,X2))	→	active#(X2)	(33)
  active#(U11(X))	→	active#(X)	(35)
  active#(U12(X))	→	active#(X)	(37)
  active#(isNePal(X))	→	active#(X)	(39)

  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.

  active#(__(X1,X2))	→	active#(X1)	(31)
  1	>	1
  active#(__(X1,X2))	→	active#(X2)	(33)
  1	>	1
  active#(U11(X))	→	active#(X)	(35)
  1	>	1
  active#(U12(X))	→	active#(X)	(37)
  1	>	1
  active#(isNePal(X))	→	active#(X)	(39)
  1	>	1

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

• The 3^rd component contains the pair

  proper#(__(X1,X2))	→	proper#(X2)	(46)
  proper#(__(X1,X2))	→	proper#(X1)	(47)
  proper#(U11(X))	→	proper#(X)	(49)
  proper#(U12(X))	→	proper#(X)	(51)
  proper#(isNePal(X))	→	proper#(X)	(53)

  1.1.1.1.1.1.3 Subterm Criterion Processor

  We use the projection

  π(proper#)

  =

  1

  and remove the pairs:

  proper#(__(X1,X2))	→	proper#(X2)	(46)
  proper#(__(X1,X2))	→	proper#(X1)	(47)
  proper#(U11(X))	→	proper#(X)	(49)
  proper#(U12(X))	→	proper#(X)	(51)
  proper#(isNePal(X))	→	proper#(X)	(53)

  1.1.1.1.1.1.3.1 P is empty

  There are no pairs anymore.

• The 4^th component contains the pair

  isNePal#(mark(X))	→	isNePal#(X)	(45)
  isNePal#(ok(X))	→	isNePal#(X)	(58)

  1.1.1.1.1.1.4 Size-Change Termination

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

  isNePal#(mark(X))	→	isNePal#(X)	(45)
  1	>	1
  isNePal#(ok(X))	→	isNePal#(X)	(58)
  1	>	1

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

• The 5^th component contains the pair

  U12#(mark(X))	→	U12#(X)	(44)
  U12#(ok(X))	→	U12#(X)	(57)

  1.1.1.1.1.1.5 Size-Change Termination

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

  U12#(mark(X))	→	U12#(X)	(44)
  1	>	1
  U12#(ok(X))	→	U12#(X)	(57)
  1	>	1

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

• The 6^th component contains the pair

  U11#(mark(X))	→	U11#(X)	(43)
  U11#(ok(X))	→	U11#(X)	(56)

  1.1.1.1.1.1.6 Size-Change Termination

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

  U11#(mark(X))	→	U11#(X)	(43)
  1	>	1
  U11#(ok(X))	→	U11#(X)	(56)
  1	>	1

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

• The 7^th component contains the pair

  __#(mark(X1),X2)	→	__#(X1,X2)	(41)
  __#(X1,mark(X2))	→	__#(X1,X2)	(42)
  __#(ok(X1),ok(X2))	→	__#(X1,X2)	(55)

  1.1.1.1.1.1.7 Size-Change Termination

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

  __#(mark(X1),X2)	→	__#(X1,X2)	(41)
  2	≥	2
  1	>	1
  __#(X1,mark(X2))	→	__#(X1,X2)	(42)
  2	>	2
  1	≥	1
  __#(ok(X1),ok(X2))	→	__#(X1,X2)	(55)
  2	>	2
  1	>	1

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