Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_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 Dependency Pair Transformation

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(97)
  top#(mark(X))	→	top#(proper(X))	(95)

  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(u)	=	0		stat(u)	=	lex
  prec(o)	=	0		stat(o)	=	lex
  prec(i)	=	0		stat(i)	=	lex
  prec(e)	=	0		stat(e)	=	lex
  prec(a)	=	0		stat(a)	=	lex
  prec(isPal)	=	1		stat(isPal)	=	lex
  prec(isNePal)	=	0		stat(isNePal)	=	lex
  prec(isQid)	=	1		stat(isQid)	=	lex
  prec(isNeList)	=	0		stat(isNeList)	=	lex
  prec(isList)	=	1		stat(isList)	=	lex
  prec(and)	=	0		stat(and)	=	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(__)	=	3		stat(__)	=	lex

  π(top#)	=	1
  π(ok)	=	1
  π(proper)	=	1
  π(u)	=	[]
  π(o)	=	[]
  π(i)	=	[]
  π(e)	=	[]
  π(a)	=	[]
  π(isPal)	=	[1]
  π(isNePal)	=	1
  π(isQid)	=	[]
  π(isNeList)	=	1
  π(isList)	=	[1]
  π(and)	=	1
  π(tt)	=	[]
  π(nil)	=	[]
  π(mark)	=	[1]
  π(active)	=	1
  π(__)	=	[1,2]

  together with the usable rules

  active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
  active(isList(V))	→	mark(isNeList(V))	(5)
  active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
  active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
  active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
  active(isPal(V))	→	mark(isNePal(V))	(13)
  active(isQid(a))	→	mark(tt)	(15)
  active(isQid(e))	→	mark(tt)	(16)
  active(isQid(i))	→	mark(tt)	(17)
  active(isQid(u))	→	mark(tt)	(19)
  active(__(X1,X2))	→	__(active(X1),X2)	(20)
  active(__(X1,X2))	→	__(X1,active(X2))	(21)
  active(and(X1,X2))	→	and(active(X1),X2)	(22)
  __(mark(X1),X2)	→	mark(__(X1,X2))	(23)
  __(X1,mark(X2))	→	mark(__(X1,X2))	(24)
  __(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
  isNeList(ok(X))	→	ok(isNeList(X))	(43)
  isList(ok(X))	→	ok(isList(X))	(42)
  and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
  and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
  isNePal(ok(X))	→	ok(isNePal(X))	(45)
  proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
  proper(nil)	→	ok(nil)	(27)
  proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
  proper(tt)	→	ok(tt)	(29)
  proper(isList(X))	→	isList(proper(X))	(30)
  proper(isNeList(X))	→	isNeList(proper(X))	(31)
  proper(isQid(X))	→	isQid(proper(X))	(32)
  proper(isNePal(X))	→	isNePal(proper(X))	(33)
  proper(isPal(X))	→	isPal(proper(X))	(34)
  proper(a)	→	ok(a)	(35)
  proper(e)	→	ok(e)	(36)
  proper(i)	→	ok(i)	(37)
  proper(o)	→	ok(o)	(38)
  proper(u)	→	ok(u)	(39)
  isQid(ok(X))	→	ok(isQid(X))	(44)
  isPal(ok(X))	→	ok(isPal(X))	(46)

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

  top#(mark(X))

  →

  top#(proper(X))

  (95)

  could be deleted.

  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(u)	=	0		stat(u)	=	lex
  prec(i)	=	0		stat(i)	=	lex
  prec(e)	=	0		stat(e)	=	lex
  prec(a)	=	0		stat(a)	=	lex
  prec(isPal)	=	0		stat(isPal)	=	lex
  prec(isNePal)	=	0		stat(isNePal)	=	lex
  prec(isQid)	=	1		stat(isQid)	=	lex
  prec(isNeList)	=	0		stat(isNeList)	=	lex
  prec(isList)	=	0		stat(isList)	=	lex
  prec(and)	=	0		stat(and)	=	lex
  prec(tt)	=	0		stat(tt)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(__)	=	0		stat(__)	=	lex

  π(top#)	=	1
  π(ok)	=	[1]
  π(u)	=	[]
  π(i)	=	[]
  π(e)	=	[]
  π(a)	=	[]
  π(isPal)	=	1
  π(isNePal)	=	1
  π(isQid)	=	[]
  π(isNeList)	=	1
  π(isList)	=	1
  π(and)	=	1
  π(tt)	=	[]
  π(mark)	=	1
  π(active)	=	1
  π(__)	=	1

  together with the usable rules

  active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
  active(isList(V))	→	mark(isNeList(V))	(5)
  active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
  active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
  active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
  active(isPal(V))	→	mark(isNePal(V))	(13)
  active(isQid(a))	→	mark(tt)	(15)
  active(isQid(e))	→	mark(tt)	(16)
  active(isQid(i))	→	mark(tt)	(17)
  active(isQid(u))	→	mark(tt)	(19)
  active(__(X1,X2))	→	__(active(X1),X2)	(20)
  active(__(X1,X2))	→	__(X1,active(X2))	(21)
  active(and(X1,X2))	→	and(active(X1),X2)	(22)
  __(mark(X1),X2)	→	mark(__(X1,X2))	(23)
  __(X1,mark(X2))	→	mark(__(X1,X2))	(24)
  __(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
  isNeList(ok(X))	→	ok(isNeList(X))	(43)
  isList(ok(X))	→	ok(isList(X))	(42)
  and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
  and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
  isNePal(ok(X))	→	ok(isNePal(X))	(45)

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

  top#(ok(X))

  →

  top#(active(X))

  (97)

  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

  proper#(isPal(X))	→	proper#(X)	(85)
  proper#(isNePal(X))	→	proper#(X)	(83)
  proper#(isQid(X))	→	proper#(X)	(81)
  proper#(isNeList(X))	→	proper#(X)	(79)
  proper#(isList(X))	→	proper#(X)	(77)
  proper#(and(X1,X2))	→	proper#(X1)	(75)
  proper#(and(X1,X2))	→	proper#(X2)	(74)
  proper#(__(X1,X2))	→	proper#(X1)	(72)
  proper#(__(X1,X2))	→	proper#(X2)	(71)

  1.1.1.1.2 Subterm Criterion Processor

  We use the projection

  π(proper#)

  =

  1

  and remove the pairs:

  proper#(isPal(X))	→	proper#(X)	(85)
  proper#(isNePal(X))	→	proper#(X)	(83)
  proper#(isQid(X))	→	proper#(X)	(81)
  proper#(isNeList(X))	→	proper#(X)	(79)
  proper#(isList(X))	→	proper#(X)	(77)
  proper#(and(X1,X2))	→	proper#(X1)	(75)
  proper#(and(X1,X2))	→	proper#(X2)	(74)
  proper#(__(X1,X2))	→	proper#(X1)	(72)
  proper#(__(X1,X2))	→	proper#(X2)	(71)

  1.1.1.1.2.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  isQid#(ok(X))

  →

  isQid#(X)

  (91)

  1.1.1.1.3 Size-Change Termination

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

  isQid#(ok(X))	→	isQid#(X)	(91)
  1	>	1

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

• The 4^th component contains the pair

  isPal#(ok(X))

  →

  isPal#(X)

  (93)

  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.

  isPal#(ok(X))	→	isPal#(X)	(93)
  1	>	1

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

• The 5^th component contains the pair

  active#(and(X1,X2))	→	active#(X1)	(66)
  active#(__(X1,X2))	→	active#(X2)	(64)
  active#(__(X1,X2))	→	active#(X1)	(62)

  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.

  active#(and(X1,X2))	→	active#(X1)	(66)
  1	>	1
  active#(__(X1,X2))	→	active#(X2)	(64)
  1	>	1
  active#(__(X1,X2))	→	active#(X1)	(62)
  1	>	1

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

• The 6^th component contains the pair

  isList#(ok(X))

  →

  isList#(X)

  (89)

  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.

  isList#(ok(X))	→	isList#(X)	(89)
  1	>	1

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

• The 7^th component contains the pair

  isNeList#(ok(X))

  →

  isNeList#(X)

  (90)

  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.

  isNeList#(ok(X))	→	isNeList#(X)	(90)
  1	>	1

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

• The 8^th component contains the pair

  isNePal#(ok(X))

  →

  isNePal#(X)

  (92)

  1.1.1.1.8 Size-Change Termination

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

  isNePal#(ok(X))	→	isNePal#(X)	(92)
  1	>	1

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

• The 9^th component contains the pair

  __#(ok(X1),ok(X2))	→	__#(X1,X2)	(87)
  __#(X1,mark(X2))	→	__#(X1,X2)	(69)
  __#(mark(X1),X2)	→	__#(X1,X2)	(68)

  1.1.1.1.9 Size-Change Termination

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

  __#(ok(X1),ok(X2))	→	__#(X1,X2)	(87)
  2	>	2
  1	>	1
  __#(X1,mark(X2))	→	__#(X1,X2)	(69)
  2	>	2
  1	≥	1
  __#(mark(X1),X2)	→	__#(X1,X2)	(68)
  2	≥	2
  1	>	1

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

• The 10^th component contains the pair

  and#(ok(X1),ok(X2))	→	and#(X1,X2)	(88)
  and#(mark(X1),X2)	→	and#(X1,X2)	(70)

  1.1.1.1.10 Size-Change Termination

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

  and#(ok(X1),ok(X2))	→	and#(X1,X2)	(88)
  2	>	2
  1	>	1
  and#(mark(X1),X2)	→	and#(X1,X2)	(70)
  2	≥	2
  1	>	1

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