Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_iGM)

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 Dependency Pair Transformation

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

• The 1^st component contains the pair

  mark#(isNeList(X))	→	active#(isNeList(X))	(83)
  active#(isNeList(__(V1,V2)))	→	mark#(and(isNeList(V1),isList(V2)))	(66)
  mark#(and(X1,X2))	→	mark#(X1)	(78)
  mark#(isList(X))	→	active#(isList(X))	(82)
  active#(isList(__(V1,V2)))	→	mark#(and(isList(V1),isList(V2)))	(58)
  mark#(__(X1,X2))	→	active#(__(mark(X1),mark(X2)))	(76)
  active#(__(__(X,Y),Z))	→	mark#(__(X,__(Y,Z)))	(54)
  mark#(__(X1,X2))	→	mark#(X1)	(74)
  mark#(__(X1,X2))	→	mark#(X2)	(73)
  active#(isNeList(__(V1,V2)))	→	mark#(and(isList(V1),isNeList(V2)))	(62)

  1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(mark#)	=	0		stat(mark#)	=	lex
  prec(active#)	=	0		stat(active#)	=	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)	=	0		stat(isPal)	=	lex
  prec(isNePal)	=	0		stat(isNePal)	=	lex
  prec(isQid)	=	1		stat(isQid)	=	lex
  prec(isNeList)	=	1		stat(isNeList)	=	lex
  prec(isList)	=	0		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(__)	=	0		stat(__)	=	lex

  π(mark#)	=	1
  π(active#)	=	1
  π(u)	=	[]
  π(o)	=	[]
  π(i)	=	[]
  π(e)	=	[]
  π(a)	=	[]
  π(isPal)	=	1
  π(isNePal)	=	1
  π(isQid)	=	[]
  π(isNeList)	=	[]
  π(isList)	=	[]
  π(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(__(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(i))	→	mark(tt)	(17)
  active(isQid(o))	→	mark(tt)	(18)
  active(isQid(u))	→	mark(tt)	(19)
  mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
  mark(nil)	→	active(nil)	(21)
  mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
  mark(tt)	→	active(tt)	(23)
  mark(isList(X))	→	active(isList(X))	(24)
  mark(isNeList(X))	→	active(isNeList(X))	(25)
  mark(isQid(X))	→	active(isQid(X))	(26)
  mark(isNePal(X))	→	active(isNePal(X))	(27)
  mark(isPal(X))	→	active(isPal(X))	(28)
  mark(a)	→	active(a)	(29)
  mark(e)	→	active(e)	(30)
  mark(i)	→	active(i)	(31)
  mark(o)	→	active(o)	(32)
  mark(u)	→	active(u)	(33)
  __(mark(X1),X2)	→	__(X1,X2)	(34)
  __(X1,mark(X2))	→	__(X1,X2)	(35)
  __(active(X1),X2)	→	__(X1,X2)	(36)
  __(X1,active(X2))	→	__(X1,X2)	(37)
  and(mark(X1),X2)	→	and(X1,X2)	(38)
  and(X1,mark(X2))	→	and(X1,X2)	(39)
  and(active(X1),X2)	→	and(X1,X2)	(40)
  and(X1,active(X2))	→	and(X1,X2)	(41)
  isList(mark(X))	→	isList(X)	(42)
  isList(active(X))	→	isList(X)	(43)
  isNeList(mark(X))	→	isNeList(X)	(44)
  isNeList(active(X))	→	isNeList(X)	(45)
  isQid(mark(X))	→	isQid(X)	(46)
  isQid(active(X))	→	isQid(X)	(47)
  isNePal(mark(X))	→	isNePal(X)	(48)
  isNePal(active(X))	→	isNePal(X)	(49)
  isPal(mark(X))	→	isPal(X)	(50)
  isPal(active(X))	→	isPal(X)	(51)

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

  active#(__(__(X,Y),Z))	→	mark#(__(X,__(Y,Z)))	(54)
  mark#(__(X1,X2))	→	mark#(X1)	(74)
  mark#(__(X1,X2))	→	mark#(X2)	(73)
  active#(isNeList(__(V1,V2)))	→	mark#(and(isList(V1),isNeList(V2)))	(62)

  could be deleted.

  1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    mark#(isNeList(X))	→	active#(isNeList(X))	(83)
    active#(isNeList(__(V1,V2)))	→	mark#(and(isNeList(V1),isList(V2)))	(66)
    mark#(and(X1,X2))	→	mark#(X1)	(78)
    mark#(isList(X))	→	active#(isList(X))	(82)
    active#(isList(__(V1,V2)))	→	mark#(and(isList(V1),isList(V2)))	(58)

    1.1.1.1.1.1.1.1 Subterm Criterion Processor

    We use the projection to multisets

    π(mark#)	=	{ 1 }
    π(active#)	=	{ 1 }
    π(isNeList)	=	{ 1 }
    π(isList)	=	{ 1 }
    π(and)	=	{ 1 }

    to remove the pairs:

    active#(isNeList(__(V1,V2)))	→	mark#(and(isNeList(V1),isList(V2)))	(66)
    active#(isList(__(V1,V2)))	→	mark#(and(isList(V1),isList(V2)))	(58)

    1.1.1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      mark#(and(X1,X2))

      →

      mark#(X1)

      (78)

      1.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.

      mark#(and(X1,X2))	→	mark#(X1)	(78)
      1	>	1

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

• The 2^nd component contains the pair

  __#(X1,active(X2))	→	__#(X1,X2)	(95)
  __#(active(X1),X2)	→	__#(X1,X2)	(94)
  __#(X1,mark(X2))	→	__#(X1,X2)	(93)
  __#(mark(X1),X2)	→	__#(X1,X2)	(92)

  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.

  __#(X1,active(X2))	→	__#(X1,X2)	(95)
  2	>	2
  1	≥	1
  __#(active(X1),X2)	→	__#(X1,X2)	(94)
  2	≥	2
  1	>	1
  __#(X1,mark(X2))	→	__#(X1,X2)	(93)
  2	>	2
  1	≥	1
  __#(mark(X1),X2)	→	__#(X1,X2)	(92)
  2	≥	2
  1	>	1

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

• The 3^rd component contains the pair

  isList#(mark(X))	→	isList#(X)	(100)
  isList#(active(X))	→	isList#(X)	(101)

  1.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.

  isList#(mark(X))	→	isList#(X)	(100)
  1	>	1
  isList#(active(X))	→	isList#(X)	(101)
  1	>	1

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

• The 4^th component contains the pair

  and#(mark(X1),X2)	→	and#(X1,X2)	(96)
  and#(X1,active(X2))	→	and#(X1,X2)	(99)
  and#(active(X1),X2)	→	and#(X1,X2)	(98)
  and#(X1,mark(X2))	→	and#(X1,X2)	(97)

  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.

  and#(mark(X1),X2)	→	and#(X1,X2)	(96)
  2	≥	2
  1	>	1
  and#(X1,active(X2))	→	and#(X1,X2)	(99)
  2	>	2
  1	≥	1
  and#(active(X1),X2)	→	and#(X1,X2)	(98)
  2	≥	2
  1	>	1
  and#(X1,mark(X2))	→	and#(X1,X2)	(97)
  2	>	2
  1	≥	1

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

• The 5^th component contains the pair

  isNeList#(mark(X))	→	isNeList#(X)	(102)
  isNeList#(active(X))	→	isNeList#(X)	(103)

  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.

  isNeList#(mark(X))	→	isNeList#(X)	(102)
  1	>	1
  isNeList#(active(X))	→	isNeList#(X)	(103)
  1	>	1

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

• The 6^th component contains the pair

  isNePal#(mark(X))	→	isNePal#(X)	(106)
  isNePal#(active(X))	→	isNePal#(X)	(107)

  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.

  isNePal#(mark(X))	→	isNePal#(X)	(106)
  1	>	1
  isNePal#(active(X))	→	isNePal#(X)	(107)
  1	>	1

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

• The 7^th component contains the pair

  isQid#(mark(X))	→	isQid#(X)	(104)
  isQid#(active(X))	→	isQid#(X)	(105)

  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.

  isQid#(mark(X))	→	isQid#(X)	(104)
  1	>	1
  isQid#(active(X))	→	isQid#(X)	(105)
  1	>	1

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

• The 8^th component contains the pair

  isPal#(mark(X))	→	isPal#(X)	(108)
  isPal#(active(X))	→	isPal#(X)	(109)

  1.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.

  isPal#(mark(X))	→	isPal#(X)	(108)
  1	>	1
  isPal#(active(X))	→	isPal#(X)	(109)
  1	>	1

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