Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_GL02a_iGM)

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

• The 1^st component contains the pair

  active#(eq(s(X),s(Y)))	→	mark#(eq(X,Y))	(38)
  mark#(eq(X1,X2))	→	active#(eq(X1,X2))	(53)
  active#(inf(X))	→	mark#(cons(X,inf(s(X))))	(41)
  mark#(s(X))	→	active#(s(X))	(56)
  active#(take(s(X),cons(Y,L)))	→	mark#(cons(Y,take(X,L)))	(46)
  mark#(inf(X))	→	active#(inf(mark(X)))	(58)
  active#(length(cons(X,L)))	→	mark#(s(length(L)))	(50)
  mark#(inf(X))	→	mark#(X)	(60)
  mark#(cons(X1,X2))	→	active#(cons(X1,X2))	(61)
  mark#(take(X1,X2))	→	active#(take(mark(X1),mark(X2)))	(62)
  mark#(take(X1,X2))	→	mark#(X1)	(64)
  mark#(take(X1,X2))	→	mark#(X2)	(65)
  mark#(length(X))	→	active#(length(mark(X)))	(67)
  mark#(length(X))	→	mark#(X)	(69)

  1.1.1 Reduction Pair Processor

  Using the Knuth Bendix order with w0 = 3 and the following precedence and weight functions

  prec(eq)	=	2		weight(eq)	=	7
  prec(cons)	=	6		weight(cons)	=	3
  prec(s)	=	0		weight(s)	=	5
  prec(take)	=	4		weight(take)	=	3
  prec(length)	=	3		weight(length)	=	4
  prec(0)	=	5		weight(0)	=	8
  prec(true)	=	1		weight(true)	=	5
  prec(false)	=	7		weight(false)	=	5
  prec(nil)	=	8		weight(nil)	=	8

  in combination with the following argument filter

  π(active#)	=	1
  π(eq)	=	[]
  π(mark#)	=	1
  π(inf)	=	1
  π(cons)	=	[]
  π(s)	=	[]
  π(take)	=	[1,2]
  π(mark)	=	1
  π(length)	=	[1]
  π(active)	=	1
  π(0)	=	[]
  π(true)	=	[]
  π(false)	=	[]
  π(nil)	=	[]

  the pairs

  active#(take(s(X),cons(Y,L)))	→	mark#(cons(Y,take(X,L)))	(46)
  active#(length(cons(X,L)))	→	mark#(s(length(L)))	(50)
  mark#(take(X1,X2))	→	mark#(X1)	(64)
  mark#(take(X1,X2))	→	mark#(X2)	(65)
  mark#(length(X))	→	mark#(X)	(69)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(active#)	=	2		stat(active#)	=	mul
  prec(eq)	=	2		stat(eq)	=	mul
  prec(s)	=	2		stat(s)	=	mul
  prec(inf)	=	3		stat(inf)	=	mul
  prec(cons)	=	2		stat(cons)	=	mul
  prec(mark)	=	0		stat(mark)	=	mul
  prec(take)	=	4		stat(take)	=	mul
  prec(length)	=	2		stat(length)	=	mul
  prec(active)	=	1		stat(active)	=	mul
  prec(0)	=	4		stat(0)	=	mul
  prec(true)	=	1		stat(true)	=	mul
  prec(false)	=	5		stat(false)	=	mul
  prec(nil)	=	4		stat(nil)	=	mul

  π(active#)	=	[]
  π(eq)	=	[]
  π(s)	=	[1]
  π(mark#)	=	1
  π(inf)	=	[1]
  π(cons)	=	[]
  π(mark)	=	[1]
  π(take)	=	[1,2]
  π(length)	=	[]
  π(active)	=	[]
  π(0)	=	[]
  π(true)	=	[]
  π(false)	=	[]
  π(nil)	=	[]

  together with the usable rules

  eq(X1,mark(X2))	→	eq(X1,X2)	(20)
  eq(mark(X1),X2)	→	eq(X1,X2)	(19)
  eq(active(X1),X2)	→	eq(X1,X2)	(21)
  eq(X1,active(X2))	→	eq(X1,X2)	(22)
  cons(X1,mark(X2))	→	cons(X1,X2)	(28)
  cons(mark(X1),X2)	→	cons(X1,X2)	(27)
  cons(active(X1),X2)	→	cons(X1,X2)	(29)
  cons(X1,active(X2))	→	cons(X1,X2)	(30)

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

  mark#(s(X))	→	active#(s(X))	(56)
  mark#(inf(X))	→	active#(inf(mark(X)))	(58)
  mark#(inf(X))	→	mark#(X)	(60)
  mark#(take(X1,X2))	→	active#(take(mark(X1),mark(X2)))	(62)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

  prec(eq)	=	0		weight(eq)	=	1
  prec(inf)	=	2		weight(inf)	=	3
  prec(cons)	=	3		weight(cons)	=	2
  prec(length)	=	1		weight(length)	=	2

  in combination with the following argument filter

  π(active#)	=	1
  π(eq)	=	[]
  π(mark#)	=	1
  π(inf)	=	[]
  π(cons)	=	[]
  π(length)	=	[]

  together with the usable rules

  eq(X1,mark(X2))	→	eq(X1,X2)	(20)
  eq(mark(X1),X2)	→	eq(X1,X2)	(19)
  eq(active(X1),X2)	→	eq(X1,X2)	(21)
  eq(X1,active(X2))	→	eq(X1,X2)	(22)
  cons(X1,mark(X2))	→	cons(X1,X2)	(28)
  cons(mark(X1),X2)	→	cons(X1,X2)	(27)
  cons(active(X1),X2)	→	cons(X1,X2)	(29)
  cons(X1,active(X2))	→	cons(X1,X2)	(30)
  length(active(X))	→	length(X)	(36)
  length(mark(X))	→	length(X)	(35)

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

  active#(inf(X))

  →

  mark#(cons(X,inf(s(X))))

  (41)

  could be deleted.

  1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

  prec(s)	=	0		weight(s)	=	1
  prec(cons)	=	2		weight(cons)	=	2
  prec(length)	=	1		weight(length)	=	1

  in combination with the following argument filter

  π(active#)	=	1
  π(eq)	=	2
  π(s)	=	[1]
  π(mark#)	=	1
  π(cons)	=	[]
  π(length)	=	[]
  π(mark)	=	1
  π(active)	=	1

  together with the usable rules

  eq(X1,mark(X2))	→	eq(X1,X2)	(20)
  eq(mark(X1),X2)	→	eq(X1,X2)	(19)
  eq(active(X1),X2)	→	eq(X1,X2)	(21)
  eq(X1,active(X2))	→	eq(X1,X2)	(22)
  cons(X1,mark(X2))	→	cons(X1,X2)	(28)
  cons(mark(X1),X2)	→	cons(X1,X2)	(27)
  cons(active(X1),X2)	→	cons(X1,X2)	(29)
  cons(X1,active(X2))	→	cons(X1,X2)	(30)
  length(active(X))	→	length(X)	(36)
  length(mark(X))	→	length(X)	(35)

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

  active#(eq(s(X),s(Y)))

  →

  mark#(eq(X,Y))

  (38)

  could be deleted.

  1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  eq#(X1,mark(X2))	→	eq#(X1,X2)	(71)
  eq#(mark(X1),X2)	→	eq#(X1,X2)	(70)
  eq#(active(X1),X2)	→	eq#(X1,X2)	(72)
  eq#(X1,active(X2))	→	eq#(X1,X2)	(73)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [active(x1)]	=	1 · x1
  [eq#(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.2.1 Size-Change Termination

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

  eq#(X1,mark(X2))	→	eq#(X1,X2)	(71)
  1	≥	1
  2	>	2
  eq#(mark(X1),X2)	→	eq#(X1,X2)	(70)
  1	>	1
  2	≥	2
  eq#(active(X1),X2)	→	eq#(X1,X2)	(72)
  1	>	1
  2	≥	2
  eq#(X1,active(X2))	→	eq#(X1,X2)	(73)
  1	≥	1
  2	>	2

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

• The 3^rd component contains the pair

  s#(active(X))	→	s#(X)	(75)
  s#(mark(X))	→	s#(X)	(74)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 · x1
  [mark(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.3.1 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)	(75)
  1	>	1
  s#(mark(X))	→	s#(X)	(74)
  1	>	1

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

• The 4^th component contains the pair

  inf#(active(X))	→	inf#(X)	(77)
  inf#(mark(X))	→	inf#(X)	(76)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [inf#(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.

  inf#(active(X))	→	inf#(X)	(77)
  1	>	1
  inf#(mark(X))	→	inf#(X)	(76)
  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#(X1,mark(X2))	→	cons#(X1,X2)	(79)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(78)
  cons#(active(X1),X2)	→	cons#(X1,X2)	(80)
  cons#(X1,active(X2))	→	cons#(X1,X2)	(81)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [active(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#(X1,mark(X2))	→	cons#(X1,X2)	(79)
  1	≥	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(78)
  1	>	1
  2	≥	2
  cons#(active(X1),X2)	→	cons#(X1,X2)	(80)
  1	>	1
  2	≥	2
  cons#(X1,active(X2))	→	cons#(X1,X2)	(81)
  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

  take#(X1,mark(X2))	→	take#(X1,X2)	(83)
  take#(mark(X1),X2)	→	take#(X1,X2)	(82)
  take#(active(X1),X2)	→	take#(X1,X2)	(84)
  take#(X1,active(X2))	→	take#(X1,X2)	(85)

  1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [active(x1)]	=	1 · x1
  [take#(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.6.1 Size-Change Termination

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

  take#(X1,mark(X2))	→	take#(X1,X2)	(83)
  1	≥	1
  2	>	2
  take#(mark(X1),X2)	→	take#(X1,X2)	(82)
  1	>	1
  2	≥	2
  take#(active(X1),X2)	→	take#(X1,X2)	(84)
  1	>	1
  2	≥	2
  take#(X1,active(X2))	→	take#(X1,X2)	(85)
  1	≥	1
  2	>	2

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

• The 7^th component contains the pair

  length#(active(X))	→	length#(X)	(87)
  length#(mark(X))	→	length#(X)	(86)

  1.1.7 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [active(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [length#(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.

  length#(active(X))	→	length#(X)	(87)
  1	>	1
  length#(mark(X))	→	length#(X)	(86)
  1	>	1

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