Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_DLMMU04_iGM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

• The 1^st component contains the pair

  mark#(repItems(X))	→	mark#(X)	(96)
  mark#(repItems(X))	→	active#(repItems(mark(X)))	(98)
  active#(repItems(cons(X,XS)))	→	mark#(cons(X,cons(X,repItems(XS))))	(67)
  mark#(cons(X1,X2))	→	mark#(X1)	(69)
  mark#(tail(X))	→	mark#(X)	(93)
  mark#(pair(X1,X2))	→	mark#(X1)	(90)
  mark#(pair(X1,X2))	→	mark#(X2)	(89)
  mark#(zip(X1,X2))	→	active#(zip(mark(X1),mark(X2)))	(88)
  active#(zip(cons(X,XS),cons(Y,YS)))	→	mark#(cons(pair(X,Y),zip(XS,YS)))	(63)
  mark#(zip(X1,X2))	→	mark#(X1)	(86)
  mark#(zip(X1,X2))	→	mark#(X2)	(85)
  mark#(take(X1,X2))	→	mark#(X1)	(81)
  mark#(take(X1,X2))	→	mark#(X2)	(80)
  mark#(s(X))	→	mark#(X)	(77)
  mark#(oddNs)	→	active#(oddNs)	(76)
  active#(oddNs)	→	mark#(incr(pairNs))	(52)
  mark#(incr(X))	→	active#(incr(mark(X)))	(75)
  active#(incr(cons(X,XS)))	→	mark#(cons(s(X),incr(XS)))	(56)
  mark#(incr(X))	→	mark#(X)	(73)
  mark#(pairNs)	→	active#(pairNs)	(68)
  active#(pairNs)	→	mark#(cons(0,incr(oddNs)))	(50)

  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(repItems)	=	0		stat(repItems)	=	lex
  prec(tail)	=	0		stat(tail)	=	lex
  prec(pair)	=	0		stat(pair)	=	lex
  prec(zip)	=	1		stat(zip)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(take)	=	1		stat(take)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(cons)	=	0		stat(cons)	=	lex
  prec(incr)	=	0		stat(incr)	=	lex
  prec(oddNs)	=	3		stat(oddNs)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(pairNs)	=	2		stat(pairNs)	=	lex

  π(mark#)	=	1
  π(active#)	=	1
  π(repItems)	=	1
  π(tail)	=	1
  π(pair)	=	[1,2]
  π(zip)	=	[1,2]
  π(nil)	=	[]
  π(take)	=	[1,2]
  π(s)	=	1
  π(mark)	=	1
  π(cons)	=	[1]
  π(incr)	=	1
  π(oddNs)	=	[]
  π(0)	=	[]
  π(active)	=	1
  π(pairNs)	=	[]

  together with the usable rules

  active(pairNs)	→	mark(cons(0,incr(oddNs)))	(1)
  active(oddNs)	→	mark(incr(pairNs))	(2)
  active(incr(cons(X,XS)))	→	mark(cons(s(X),incr(XS)))	(3)
  active(take(0,XS))	→	mark(nil)	(4)
  active(zip(nil,XS))	→	mark(nil)	(6)
  active(zip(X,nil))	→	mark(nil)	(7)
  active(zip(cons(X,XS),cons(Y,YS)))	→	mark(cons(pair(X,Y),zip(XS,YS)))	(8)
  active(repItems(cons(X,XS)))	→	mark(cons(X,cons(X,repItems(XS))))	(11)
  mark(pairNs)	→	active(pairNs)	(12)
  mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(13)
  mark(0)	→	active(0)	(14)
  mark(incr(X))	→	active(incr(mark(X)))	(15)
  mark(oddNs)	→	active(oddNs)	(16)
  mark(s(X))	→	active(s(mark(X)))	(17)
  mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(18)
  mark(nil)	→	active(nil)	(19)
  mark(zip(X1,X2))	→	active(zip(mark(X1),mark(X2)))	(20)
  mark(pair(X1,X2))	→	active(pair(mark(X1),mark(X2)))	(21)
  mark(tail(X))	→	active(tail(mark(X)))	(22)
  mark(repItems(X))	→	active(repItems(mark(X)))	(23)
  cons(mark(X1),X2)	→	cons(X1,X2)	(24)
  cons(X1,mark(X2))	→	cons(X1,X2)	(25)
  cons(active(X1),X2)	→	cons(X1,X2)	(26)
  cons(X1,active(X2))	→	cons(X1,X2)	(27)
  incr(mark(X))	→	incr(X)	(28)
  incr(active(X))	→	incr(X)	(29)
  s(mark(X))	→	s(X)	(30)
  s(active(X))	→	s(X)	(31)
  take(mark(X1),X2)	→	take(X1,X2)	(32)
  take(X1,mark(X2))	→	take(X1,X2)	(33)
  take(active(X1),X2)	→	take(X1,X2)	(34)
  take(X1,active(X2))	→	take(X1,X2)	(35)
  zip(mark(X1),X2)	→	zip(X1,X2)	(36)
  zip(X1,mark(X2))	→	zip(X1,X2)	(37)
  zip(active(X1),X2)	→	zip(X1,X2)	(38)
  zip(X1,active(X2))	→	zip(X1,X2)	(39)
  pair(mark(X1),X2)	→	pair(X1,X2)	(40)
  pair(X1,mark(X2))	→	pair(X1,X2)	(41)
  pair(active(X1),X2)	→	pair(X1,X2)	(42)
  pair(X1,active(X2))	→	pair(X1,X2)	(43)
  tail(mark(X))	→	tail(X)	(44)
  tail(active(X))	→	tail(X)	(45)
  repItems(mark(X))	→	repItems(X)	(46)
  repItems(active(X))	→	repItems(X)	(47)

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

  mark#(cons(X1,X2))	→	mark#(X1)	(69)
  mark#(pair(X1,X2))	→	mark#(X1)	(90)
  mark#(pair(X1,X2))	→	mark#(X2)	(89)
  active#(zip(cons(X,XS),cons(Y,YS)))	→	mark#(cons(pair(X,Y),zip(XS,YS)))	(63)
  mark#(zip(X1,X2))	→	mark#(X1)	(86)
  mark#(zip(X1,X2))	→	mark#(X2)	(85)
  mark#(take(X1,X2))	→	mark#(X1)	(81)
  mark#(take(X1,X2))	→	mark#(X2)	(80)
  active#(oddNs)	→	mark#(incr(pairNs))	(52)
  active#(pairNs)	→	mark#(cons(0,incr(oddNs)))	(50)

  could be deleted.

  1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    mark#(repItems(X))	→	mark#(X)	(96)
    mark#(tail(X))	→	mark#(X)	(93)
    mark#(s(X))	→	mark#(X)	(77)
    mark#(incr(X))	→	mark#(X)	(73)

    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#(repItems(X))	→	mark#(X)	(96)
    1	>	1
    mark#(tail(X))	→	mark#(X)	(93)
    1	>	1
    mark#(s(X))	→	mark#(X)	(77)
    1	>	1
    mark#(incr(X))	→	mark#(X)	(73)
    1	>	1

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

• The 2^nd component contains the pair

  incr#(active(X))	→	incr#(X)	(104)
  incr#(mark(X))	→	incr#(X)	(103)

  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.

  incr#(active(X))	→	incr#(X)	(104)
  1	>	1
  incr#(mark(X))	→	incr#(X)	(103)
  1	>	1

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

• The 3^rd component contains the pair

  cons#(X1,active(X2))	→	cons#(X1,X2)	(102)
  cons#(active(X1),X2)	→	cons#(X1,X2)	(101)
  cons#(X1,mark(X2))	→	cons#(X1,X2)	(100)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(99)

  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.

  cons#(X1,active(X2))	→	cons#(X1,X2)	(102)
  2	>	2
  1	≥	1
  cons#(active(X1),X2)	→	cons#(X1,X2)	(101)
  2	≥	2
  1	>	1
  cons#(X1,mark(X2))	→	cons#(X1,X2)	(100)
  2	>	2
  1	≥	1
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(99)
  2	≥	2
  1	>	1

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

• The 4^th component contains the pair

  s#(mark(X))	→	s#(X)	(105)
  s#(active(X))	→	s#(X)	(106)

  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.

  s#(mark(X))	→	s#(X)	(105)
  1	>	1
  s#(active(X))	→	s#(X)	(106)
  1	>	1

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

• The 5^th component contains the pair

  zip#(mark(X1),X2)	→	zip#(X1,X2)	(111)
  zip#(X1,active(X2))	→	zip#(X1,X2)	(114)
  zip#(active(X1),X2)	→	zip#(X1,X2)	(113)
  zip#(X1,mark(X2))	→	zip#(X1,X2)	(112)

  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.

  zip#(mark(X1),X2)	→	zip#(X1,X2)	(111)
  2	≥	2
  1	>	1
  zip#(X1,active(X2))	→	zip#(X1,X2)	(114)
  2	>	2
  1	≥	1
  zip#(active(X1),X2)	→	zip#(X1,X2)	(113)
  2	≥	2
  1	>	1
  zip#(X1,mark(X2))	→	zip#(X1,X2)	(112)
  2	>	2
  1	≥	1

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

• The 6^th component contains the pair

  pair#(mark(X1),X2)	→	pair#(X1,X2)	(115)
  pair#(X1,active(X2))	→	pair#(X1,X2)	(118)
  pair#(active(X1),X2)	→	pair#(X1,X2)	(117)
  pair#(X1,mark(X2))	→	pair#(X1,X2)	(116)

  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.

  pair#(mark(X1),X2)	→	pair#(X1,X2)	(115)
  2	≥	2
  1	>	1
  pair#(X1,active(X2))	→	pair#(X1,X2)	(118)
  2	>	2
  1	≥	1
  pair#(active(X1),X2)	→	pair#(X1,X2)	(117)
  2	≥	2
  1	>	1
  pair#(X1,mark(X2))	→	pair#(X1,X2)	(116)
  2	>	2
  1	≥	1

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

• The 7^th component contains the pair

  repItems#(mark(X))	→	repItems#(X)	(121)
  repItems#(active(X))	→	repItems#(X)	(122)

  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.

  repItems#(mark(X))	→	repItems#(X)	(121)
  1	>	1
  repItems#(active(X))	→	repItems#(X)	(122)
  1	>	1

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

• The 8^th component contains the pair

  take#(mark(X1),X2)	→	take#(X1,X2)	(107)
  take#(X1,active(X2))	→	take#(X1,X2)	(110)
  take#(active(X1),X2)	→	take#(X1,X2)	(109)
  take#(X1,mark(X2))	→	take#(X1,X2)	(108)

  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.

  take#(mark(X1),X2)	→	take#(X1,X2)	(107)
  2	≥	2
  1	>	1
  take#(X1,active(X2))	→	take#(X1,X2)	(110)
  2	>	2
  1	≥	1
  take#(active(X1),X2)	→	take#(X1,X2)	(109)
  2	≥	2
  1	>	1
  take#(X1,mark(X2))	→	take#(X1,X2)	(108)
  2	>	2
  1	≥	1

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

• The 9^th component contains the pair

  tail#(mark(X))	→	tail#(X)	(119)
  tail#(active(X))	→	tail#(X)	(120)

  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.

  tail#(mark(X))	→	tail#(X)	(119)
  1	>	1
  tail#(active(X))	→	tail#(X)	(120)
  1	>	1

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