Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec11_1_Luc02a_iGM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

• The 1^st component contains the pair

  mark#(half(X))	→	mark#(X)	(108)
  mark#(half(X))	→	active#(half(mark(X)))	(110)
  active#(half(dbl(X)))	→	mark#(X)	(79)
  mark#(first(X1,X2))	→	active#(first(mark(X1),mark(X2)))	(106)
  active#(first(s(X),cons(Y,Z)))	→	mark#(cons(Y,first(X,Z)))	(73)
  mark#(cons(X1,X2))	→	mark#(X1)	(83)
  mark#(first(X1,X2))	→	mark#(X1)	(104)
  mark#(first(X1,X2))	→	mark#(X2)	(103)
  mark#(dbl(X))	→	active#(dbl(mark(X)))	(102)
  active#(dbl(s(X)))	→	mark#(s(s(dbl(X))))	(65)
  mark#(s(X))	→	mark#(X)	(92)
  mark#(dbl(X))	→	mark#(X)	(100)
  mark#(add(X1,X2))	→	active#(add(mark(X1),mark(X2)))	(99)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(69)
  active#(add(0,X))	→	mark#(X)	(66)
  mark#(add(X1,X2))	→	mark#(X1)	(97)
  mark#(add(X1,X2))	→	mark#(X2)	(96)
  mark#(sqr(X))	→	active#(sqr(mark(X)))	(91)
  active#(sqr(s(X)))	→	mark#(s(add(sqr(X),dbl(X))))	(60)
  mark#(sqr(X))	→	mark#(X)	(89)
  mark#(recip(X))	→	mark#(X)	(86)
  mark#(terms(X))	→	active#(terms(mark(X)))	(82)
  active#(terms(N))	→	mark#(cons(recip(sqr(N)),terms(s(N))))	(54)
  mark#(terms(X))	→	mark#(X)	(80)
  active#(half(s(s(X))))	→	mark#(s(half(X)))	(78)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(mark#)	=	0		stat(mark#)	=	lex
  prec(active#)	=	0		stat(active#)	=	lex
  prec(half)	=	1		stat(half)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(first)	=	2		stat(first)	=	lex
  prec(add)	=	1		stat(add)	=	lex
  prec(dbl)	=	1		stat(dbl)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(cons)	=	0		stat(cons)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(recip)	=	0		stat(recip)	=	lex
  prec(sqr)	=	8		stat(sqr)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(terms)	=	12		stat(terms)	=	lex

  π(mark#)	=	1
  π(active#)	=	1
  π(half)	=	[1]
  π(nil)	=	[]
  π(first)	=	[1,2]
  π(add)	=	[1,2]
  π(dbl)	=	[1]
  π(0)	=	[]
  π(mark)	=	1
  π(cons)	=	1
  π(s)	=	[1]
  π(recip)	=	1
  π(sqr)	=	[1]
  π(active)	=	1
  π(terms)	=	[1]

  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(half(0))	→	mark(0)	(10)
  active(half(s(0)))	→	mark(0)	(11)
  active(half(s(s(X))))	→	mark(s(half(X)))	(12)
  active(half(dbl(X)))	→	mark(X)	(13)
  mark(terms(X))	→	active(terms(mark(X)))	(14)
  mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(15)
  mark(recip(X))	→	active(recip(mark(X)))	(16)
  mark(sqr(X))	→	active(sqr(mark(X)))	(17)
  mark(s(X))	→	active(s(mark(X)))	(18)
  mark(0)	→	active(0)	(19)
  mark(add(X1,X2))	→	active(add(mark(X1),mark(X2)))	(20)
  mark(dbl(X))	→	active(dbl(mark(X)))	(21)
  mark(first(X1,X2))	→	active(first(mark(X1),mark(X2)))	(22)
  mark(nil)	→	active(nil)	(23)
  mark(half(X))	→	active(half(mark(X)))	(24)
  terms(mark(X))	→	terms(X)	(25)
  terms(active(X))	→	terms(X)	(26)
  cons(mark(X1),X2)	→	cons(X1,X2)	(27)
  cons(X1,mark(X2))	→	cons(X1,X2)	(28)
  cons(active(X1),X2)	→	cons(X1,X2)	(29)
  cons(X1,active(X2))	→	cons(X1,X2)	(30)
  recip(mark(X))	→	recip(X)	(31)
  recip(active(X))	→	recip(X)	(32)
  sqr(mark(X))	→	sqr(X)	(33)
  sqr(active(X))	→	sqr(X)	(34)
  s(mark(X))	→	s(X)	(35)
  s(active(X))	→	s(X)	(36)
  add(mark(X1),X2)	→	add(X1,X2)	(37)
  add(X1,mark(X2))	→	add(X1,X2)	(38)
  add(active(X1),X2)	→	add(X1,X2)	(39)
  add(X1,active(X2))	→	add(X1,X2)	(40)
  dbl(mark(X))	→	dbl(X)	(41)
  dbl(active(X))	→	dbl(X)	(42)
  first(mark(X1),X2)	→	first(X1,X2)	(43)
  first(X1,mark(X2))	→	first(X1,X2)	(44)
  first(active(X1),X2)	→	first(X1,X2)	(45)
  first(X1,active(X2))	→	first(X1,X2)	(46)
  half(mark(X))	→	half(X)	(47)
  half(active(X))	→	half(X)	(48)

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

  mark#(half(X))	→	mark#(X)	(108)
  active#(half(dbl(X)))	→	mark#(X)	(79)
  active#(first(s(X),cons(Y,Z)))	→	mark#(cons(Y,first(X,Z)))	(73)
  mark#(first(X1,X2))	→	mark#(X1)	(104)
  mark#(first(X1,X2))	→	mark#(X2)	(103)
  active#(dbl(s(X)))	→	mark#(s(s(dbl(X))))	(65)
  mark#(s(X))	→	mark#(X)	(92)
  mark#(dbl(X))	→	mark#(X)	(100)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(69)
  active#(add(0,X))	→	mark#(X)	(66)
  mark#(add(X1,X2))	→	mark#(X1)	(97)
  mark#(add(X1,X2))	→	mark#(X2)	(96)
  active#(sqr(s(X)))	→	mark#(s(add(sqr(X),dbl(X))))	(60)
  mark#(sqr(X))	→	mark#(X)	(89)
  active#(terms(N))	→	mark#(cons(recip(sqr(N)),terms(s(N))))	(54)
  mark#(terms(X))	→	mark#(X)	(80)
  active#(half(s(s(X))))	→	mark#(s(half(X)))	(78)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    mark#(cons(X1,X2))	→	mark#(X1)	(83)
    mark#(recip(X))	→	mark#(X)	(86)

    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#(cons(X1,X2))	→	mark#(X1)	(83)
    1	>	1
    mark#(recip(X))	→	mark#(X)	(86)
    1	>	1

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

• The 2^nd component contains the pair

  terms#(active(X))	→	terms#(X)	(112)
  terms#(mark(X))	→	terms#(X)	(111)

  1.1.2 Size-Change Termination

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

  terms#(active(X))	→	terms#(X)	(112)
  1	>	1
  terms#(mark(X))	→	terms#(X)	(111)
  1	>	1

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

• The 3^rd component contains the pair

  recip#(active(X))	→	recip#(X)	(118)
  recip#(mark(X))	→	recip#(X)	(117)

  1.1.3 Size-Change Termination

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

  recip#(active(X))	→	recip#(X)	(118)
  1	>	1
  recip#(mark(X))	→	recip#(X)	(117)
  1	>	1

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

• The 4^th component contains the pair

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

  1.1.4 Size-Change Termination

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

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

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

• The 5^th component contains the pair

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

  1.1.5 Size-Change Termination

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

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

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

• The 6^th component contains the pair

  cons#(X1,active(X2))	→	cons#(X1,X2)	(116)
  cons#(active(X1),X2)	→	cons#(X1,X2)	(115)
  cons#(X1,mark(X2))	→	cons#(X1,X2)	(114)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(113)

  1.1.6 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)	(116)
  2	>	2
  1	≥	1
  cons#(active(X1),X2)	→	cons#(X1,X2)	(115)
  2	≥	2
  1	>	1
  cons#(X1,mark(X2))	→	cons#(X1,X2)	(114)
  2	>	2
  1	≥	1
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(113)
  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

  dbl#(mark(X))	→	dbl#(X)	(127)
  dbl#(active(X))	→	dbl#(X)	(128)

  1.1.7 Size-Change Termination

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

  dbl#(mark(X))	→	dbl#(X)	(127)
  1	>	1
  dbl#(active(X))	→	dbl#(X)	(128)
  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#(mark(X1),X2)	→	add#(X1,X2)	(123)
  add#(X1,active(X2))	→	add#(X1,X2)	(126)
  add#(active(X1),X2)	→	add#(X1,X2)	(125)
  add#(X1,mark(X2))	→	add#(X1,X2)	(124)

  1.1.8 Size-Change Termination

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

  add#(mark(X1),X2)	→	add#(X1,X2)	(123)
  2	≥	2
  1	>	1
  add#(X1,active(X2))	→	add#(X1,X2)	(126)
  2	>	2
  1	≥	1
  add#(active(X1),X2)	→	add#(X1,X2)	(125)
  2	≥	2
  1	>	1
  add#(X1,mark(X2))	→	add#(X1,X2)	(124)
  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

  first#(mark(X1),X2)	→	first#(X1,X2)	(129)
  first#(X1,active(X2))	→	first#(X1,X2)	(132)
  first#(active(X1),X2)	→	first#(X1,X2)	(131)
  first#(X1,mark(X2))	→	first#(X1,X2)	(130)

  1.1.9 Size-Change Termination

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

  first#(mark(X1),X2)	→	first#(X1,X2)	(129)
  2	≥	2
  1	>	1
  first#(X1,active(X2))	→	first#(X1,X2)	(132)
  2	>	2
  1	≥	1
  first#(active(X1),X2)	→	first#(X1,X2)	(131)
  2	≥	2
  1	>	1
  first#(X1,mark(X2))	→	first#(X1,X2)	(130)
  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

  half#(mark(X))	→	half#(X)	(133)
  half#(active(X))	→	half#(X)	(134)

  1.1.10 Size-Change Termination

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

  half#(mark(X))	→	half#(X)	(133)
  1	>	1
  half#(active(X))	→	half#(X)	(134)
  1	>	1

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