Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex26_Luc03b_C)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 11 components.

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(120)
  top#(mark(X))	→	top#(proper(X))	(118)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [proper(x1)]	=	1 · x1
  [terms(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [0]	=	0
  [ok(x1)]	=	2 · x1
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	1 · x1
  [first(x1, x2)]	=	2 · x1 + 1 · x2
  [nil]	=	0
  [mark(x1)]	=	1 · x1
  [active(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  proper(terms(X))	→	terms(proper(X))	(28)
  proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(29)
  proper(recip(X))	→	recip(proper(X))	(30)
  proper(sqr(X))	→	sqr(proper(X))	(31)
  proper(s(X))	→	s(proper(X))	(32)
  proper(0)	→	ok(0)	(33)
  proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(34)
  proper(dbl(X))	→	dbl(proper(X))	(35)
  proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(36)
  proper(nil)	→	ok(nil)	(37)
  first(mark(X1),X2)	→	mark(first(X1,X2))	(26)
  first(X1,mark(X2))	→	mark(first(X1,X2))	(27)
  first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(45)
  dbl(mark(X))	→	mark(dbl(X))	(25)
  dbl(ok(X))	→	ok(dbl(X))	(44)
  add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
  add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(43)
  s(ok(X))	→	ok(s(X))	(42)
  sqr(mark(X))	→	mark(sqr(X))	(22)
  sqr(ok(X))	→	ok(sqr(X))	(41)
  recip(mark(X))	→	mark(recip(X))	(21)
  recip(ok(X))	→	ok(recip(X))	(40)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(20)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(39)
  terms(mark(X))	→	mark(terms(X))	(19)
  terms(ok(X))	→	ok(terms(X))	(38)
  active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
  active(sqr(0))	→	mark(0)	(2)
  active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
  active(dbl(0))	→	mark(0)	(4)
  active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
  active(add(0,X))	→	mark(X)	(6)
  active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
  active(first(0,X))	→	mark(nil)	(8)
  active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
  active(terms(X))	→	terms(active(X))	(10)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
  active(recip(X))	→	recip(active(X))	(12)
  active(sqr(X))	→	sqr(active(X))	(13)
  active(add(X1,X2))	→	add(active(X1),X2)	(14)
  active(add(X1,X2))	→	add(X1,active(X2))	(15)
  active(dbl(X))	→	dbl(active(X))	(16)
  active(first(X1,X2))	→	first(active(X1),X2)	(17)
  active(first(X1,X2))	→	first(X1,active(X2))	(18)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [top#(x1)]	=	x1
  [active(x1)]	=	x1
  [terms(x1)]	=	2 + 2 · x1
  [mark(x1)]	=	2 + x1
  [cons(x1, x2)]	=	x1
  [recip(x1)]	=	x1
  [sqr(x1)]	=	2 · x1
  [s(x1)]	=	2
  [0]	=	2
  [add(x1, x2)]	=	2 + x1 + x2
  [dbl(x1)]	=	2 + x1
  [first(x1, x2)]	=	x1 + 2 · x2
  [nil]	=	0
  [proper(x1)]	=	x1
  [ok(x1)]	=	x1

  the pair

  top#(mark(X))

  →

  top#(proper(X))

  (118)

  could be deleted.

  1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	2 · x1
  [terms(x1)]	=	2 · x1
  [mark(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	2 · x1
  [s(x1)]	=	1 · x1
  [0]	=	0
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	2 · x1
  [first(x1, x2)]	=	2 · x1 + 2 · x2
  [nil]	=	0
  [ok(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
  active(sqr(0))	→	mark(0)	(2)
  active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
  active(dbl(0))	→	mark(0)	(4)
  active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
  active(add(0,X))	→	mark(X)	(6)
  active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
  active(first(0,X))	→	mark(nil)	(8)
  active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
  active(terms(X))	→	terms(active(X))	(10)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
  active(recip(X))	→	recip(active(X))	(12)
  active(sqr(X))	→	sqr(active(X))	(13)
  active(add(X1,X2))	→	add(active(X1),X2)	(14)
  active(add(X1,X2))	→	add(X1,active(X2))	(15)
  active(dbl(X))	→	dbl(active(X))	(16)
  active(first(X1,X2))	→	first(active(X1),X2)	(17)
  active(first(X1,X2))	→	first(X1,active(X2))	(18)
  first(mark(X1),X2)	→	mark(first(X1,X2))	(26)
  first(X1,mark(X2))	→	mark(first(X1,X2))	(27)
  first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(45)
  dbl(mark(X))	→	mark(dbl(X))	(25)
  dbl(ok(X))	→	ok(dbl(X))	(44)
  add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
  add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(43)
  sqr(mark(X))	→	mark(sqr(X))	(22)
  sqr(ok(X))	→	ok(sqr(X))	(41)
  recip(mark(X))	→	mark(recip(X))	(21)
  recip(ok(X))	→	ok(recip(X))	(40)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(20)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(39)
  terms(mark(X))	→	mark(terms(X))	(19)
  terms(ok(X))	→	ok(terms(X))	(38)
  s(ok(X))	→	ok(s(X))	(42)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	2 · x1
  [terms(x1)]	=	2 · x1
  [mark(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [0]	=	1
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	1 · x1
  [first(x1, x2)]	=	1 · x1 + 2 · x2
  [nil]	=	1
  [ok(x1)]	=	2 · x1
  [top#(x1)]	=	2 · x1

  the rules

  active(sqr(0))	→	mark(0)	(2)
  active(dbl(0))	→	mark(0)	(4)
  active(add(0,X))	→	mark(X)	(6)
  active(first(0,X))	→	mark(nil)	(8)

  could be deleted.

  1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 + 2 · x1
  [terms(x1)]	=	1 + 2 · x1
  [mark(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [add(x1, x2)]	=	1 + 1 · x1 + 1 · x2
  [dbl(x1)]	=	1 · x1
  [first(x1, x2)]	=	2 + 1 · x1 + 2 · x2
  [ok(x1)]	=	1 + 2 · x1
  [top#(x1)]	=	1 · x1

  the rules

  active(terms(N))	→	mark(cons(recip(sqr(N)),terms(s(N))))	(1)
  active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(5)
  active(add(s(X),Y))	→	mark(s(add(X,Y)))	(7)
  active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(9)
  active(add(X1,X2))	→	add(active(X1),X2)	(14)
  active(add(X1,X2))	→	add(X1,active(X2))	(15)
  active(first(X1,X2))	→	first(active(X1),X2)	(17)
  active(first(X1,X2))	→	first(X1,active(X2))	(18)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(39)

  could be deleted.

  1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	2 · x1
  [sqr(x1)]	=	2 · x1
  [s(x1)]	=	2 · x1
  [mark(x1)]	=	1 · x1
  [add(x1, x2)]	=	1 · x1 + 2 · x2
  [dbl(x1)]	=	1 · x1
  [terms(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 2 · x2
  [recip(x1)]	=	1 · x1
  [ok(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
  active(terms(X))	→	terms(active(X))	(10)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
  active(recip(X))	→	recip(active(X))	(12)
  active(sqr(X))	→	sqr(active(X))	(13)
  active(dbl(X))	→	dbl(active(X))	(16)
  dbl(mark(X))	→	mark(dbl(X))	(25)
  dbl(ok(X))	→	ok(dbl(X))	(44)
  sqr(mark(X))	→	mark(sqr(X))	(22)
  sqr(ok(X))	→	ok(sqr(X))	(41)
  recip(mark(X))	→	mark(recip(X))	(21)
  recip(ok(X))	→	ok(recip(X))	(40)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(20)
  terms(mark(X))	→	mark(terms(X))	(19)
  terms(ok(X))	→	ok(terms(X))	(38)
  add(mark(X1),X2)	→	mark(add(X1,X2))	(23)
  add(X1,mark(X2))	→	mark(add(X1,X2))	(24)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(43)
  s(ok(X))	→	ok(s(X))	(42)

  (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 + 2 · x1
  [sqr(x1)]	=	1 + 2 · x1
  [s(x1)]	=	1 + 2 · x1
  [mark(x1)]	=	1 · x1
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	1 + 2 · x1
  [terms(x1)]	=	1 + 2 · x1
  [cons(x1, x2)]	=	2 + 1 · x1 + 2 · x2
  [recip(x1)]	=	1 + 2 · x1
  [ok(x1)]	=	2 + 2 · x1
  [top#(x1)]	=	1 · x1

  the pair

  top#(ok(X))

  →

  top#(active(X))

  (120)

  and the rules

  active(sqr(s(X)))	→	mark(s(add(sqr(X),dbl(X))))	(3)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(11)
  dbl(ok(X))	→	ok(dbl(X))	(44)
  sqr(ok(X))	→	ok(sqr(X))	(41)
  recip(ok(X))	→	ok(recip(X))	(40)
  terms(ok(X))	→	ok(terms(X))	(38)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(43)
  s(ok(X))	→	ok(s(X))	(42)

  could be deleted.

  1.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#(cons(X1,X2))	→	active#(X1)	(67)
  active#(terms(X))	→	active#(X)	(65)
  active#(recip(X))	→	active#(X)	(69)
  active#(sqr(X))	→	active#(X)	(71)
  active#(add(X1,X2))	→	active#(X1)	(73)
  active#(add(X1,X2))	→	active#(X2)	(75)
  active#(dbl(X))	→	active#(X)	(77)
  active#(first(X1,X2))	→	active#(X1)	(79)
  active#(first(X1,X2))	→	active#(X2)	(81)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [terms(x1)]	=	1 · x1
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	1 · x1
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	1 · x1
  [first(x1, x2)]	=	1 · x1 + 1 · x2
  [active#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.2.1 Size-Change Termination

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

  active#(cons(X1,X2))	→	active#(X1)	(67)
  1	>	1
  active#(terms(X))	→	active#(X)	(65)
  1	>	1
  active#(recip(X))	→	active#(X)	(69)
  1	>	1
  active#(sqr(X))	→	active#(X)	(71)
  1	>	1
  active#(add(X1,X2))	→	active#(X1)	(73)
  1	>	1
  active#(add(X1,X2))	→	active#(X2)	(75)
  1	>	1
  active#(dbl(X))	→	active#(X)	(77)
  1	>	1
  active#(first(X1,X2))	→	active#(X1)	(79)
  1	>	1
  active#(first(X1,X2))	→	active#(X2)	(81)
  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#(cons(X1,X2))	→	proper#(X1)	(94)
  proper#(terms(X))	→	proper#(X)	(92)
  proper#(cons(X1,X2))	→	proper#(X2)	(95)
  proper#(recip(X))	→	proper#(X)	(97)
  proper#(sqr(X))	→	proper#(X)	(99)
  proper#(s(X))	→	proper#(X)	(101)
  proper#(add(X1,X2))	→	proper#(X1)	(103)
  proper#(add(X1,X2))	→	proper#(X2)	(104)
  proper#(dbl(X))	→	proper#(X)	(106)
  proper#(first(X1,X2))	→	proper#(X1)	(108)
  proper#(first(X1,X2))	→	proper#(X2)	(109)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [terms(x1)]	=	1 · x1
  [recip(x1)]	=	1 · x1
  [sqr(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [add(x1, x2)]	=	1 · x1 + 1 · x2
  [dbl(x1)]	=	1 · x1
  [first(x1, x2)]	=	1 · x1 + 1 · x2
  [proper#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.3.1 Size-Change Termination

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

  proper#(cons(X1,X2))	→	proper#(X1)	(94)
  1	>	1
  proper#(terms(X))	→	proper#(X)	(92)
  1	>	1
  proper#(cons(X1,X2))	→	proper#(X2)	(95)
  1	>	1
  proper#(recip(X))	→	proper#(X)	(97)
  1	>	1
  proper#(sqr(X))	→	proper#(X)	(99)
  1	>	1
  proper#(s(X))	→	proper#(X)	(101)
  1	>	1
  proper#(add(X1,X2))	→	proper#(X1)	(103)
  1	>	1
  proper#(add(X1,X2))	→	proper#(X2)	(104)
  1	>	1
  proper#(dbl(X))	→	proper#(X)	(106)
  1	>	1
  proper#(first(X1,X2))	→	proper#(X1)	(108)
  1	>	1
  proper#(first(X1,X2))	→	proper#(X2)	(109)
  1	>	1

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

• The 4^th component contains the pair

  terms#(ok(X))	→	terms#(X)	(110)
  terms#(mark(X))	→	terms#(X)	(82)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [terms#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.4.1 Size-Change Termination

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

  terms#(ok(X))	→	terms#(X)	(110)
  1	>	1
  terms#(mark(X))	→	terms#(X)	(82)
  1	>	1

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

• The 5^th component contains the pair

  cons#(ok(X1),ok(X2))	→	cons#(X1,X2)	(111)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(83)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [cons#(x1, x2)]	=	1 · x1 + 1 · x2

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.5.1 Size-Change Termination

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

  cons#(ok(X1),ok(X2))	→	cons#(X1,X2)	(111)
  1	>	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(83)
  1	>	1
  2	≥	2

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

• The 6^th component contains the pair

  recip#(ok(X))	→	recip#(X)	(112)
  recip#(mark(X))	→	recip#(X)	(84)

  1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [recip#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.6.1 Size-Change Termination

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

  recip#(ok(X))	→	recip#(X)	(112)
  1	>	1
  recip#(mark(X))	→	recip#(X)	(84)
  1	>	1

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

• The 7^th component contains the pair

  sqr#(ok(X))	→	sqr#(X)	(113)
  sqr#(mark(X))	→	sqr#(X)	(85)

  1.1.7 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [sqr#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.7.1 Size-Change Termination

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

  sqr#(ok(X))	→	sqr#(X)	(113)
  1	>	1
  sqr#(mark(X))	→	sqr#(X)	(85)
  1	>	1

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

• The 8^th component contains the pair

  add#(X1,mark(X2))	→	add#(X1,X2)	(87)
  add#(mark(X1),X2)	→	add#(X1,X2)	(86)
  add#(ok(X1),ok(X2))	→	add#(X1,X2)	(115)

  1.1.8 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [ok(x1)]	=	1 · x1
  [add#(x1, x2)]	=	1 · x1 + 1 · x2

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.8.1 Size-Change Termination

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

  add#(X1,mark(X2))	→	add#(X1,X2)	(87)
  1	≥	1
  2	>	2
  add#(mark(X1),X2)	→	add#(X1,X2)	(86)
  1	>	1
  2	≥	2
  add#(ok(X1),ok(X2))	→	add#(X1,X2)	(115)
  1	>	1
  2	>	2

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

• The 9^th component contains the pair

  dbl#(ok(X))	→	dbl#(X)	(116)
  dbl#(mark(X))	→	dbl#(X)	(88)

  1.1.9 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [dbl#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.9.1 Size-Change Termination

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

  dbl#(ok(X))	→	dbl#(X)	(116)
  1	>	1
  dbl#(mark(X))	→	dbl#(X)	(88)
  1	>	1

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

• The 10^th component contains the pair

  first#(X1,mark(X2))	→	first#(X1,X2)	(90)
  first#(mark(X1),X2)	→	first#(X1,X2)	(89)
  first#(ok(X1),ok(X2))	→	first#(X1,X2)	(117)

  1.1.10 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [ok(x1)]	=	1 · x1
  [first#(x1, x2)]	=	1 · x1 + 1 · x2

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.10.1 Size-Change Termination

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

  first#(X1,mark(X2))	→	first#(X1,X2)	(90)
  1	≥	1
  2	>	2
  first#(mark(X1),X2)	→	first#(X1,X2)	(89)
  1	>	1
  2	≥	2
  first#(ok(X1),ok(X2))	→	first#(X1,X2)	(117)
  1	>	1
  2	>	2

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

• The 11^th component contains the pair

  s#(ok(X))

  →

  s#(X)

  (114)

  1.1.11 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [ok(x1)]	=	1 · x1
  [s#(x1)]	=	1 · x1

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

  1.1.11.1 Size-Change Termination

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

  s#(ok(X))	→	s#(X)	(114)
  1	>	1

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