Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_Luc03b_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#(fst(s(X),cons(Y,Z)))	→	mark#(cons(Y,fst(X,Z)))	(35)
  mark#(fst(X1,X2))	→	active#(fst(mark(X1),mark(X2)))	(50)
  active#(from(X))	→	mark#(cons(X,from(s(X))))	(38)
  mark#(fst(X1,X2))	→	mark#(X1)	(52)
  mark#(fst(X1,X2))	→	mark#(X2)	(53)
  mark#(s(X))	→	active#(s(X))	(56)
  active#(add(0,X))	→	mark#(X)	(42)
  mark#(cons(X1,X2))	→	active#(cons(mark(X1),X2))	(57)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(43)
  mark#(cons(X1,X2))	→	mark#(X1)	(59)
  mark#(from(X))	→	active#(from(mark(X)))	(60)
  active#(len(cons(X,Z)))	→	mark#(s(len(Z)))	(47)
  mark#(from(X))	→	mark#(X)	(62)
  mark#(add(X1,X2))	→	active#(add(mark(X1),mark(X2)))	(63)
  mark#(add(X1,X2))	→	mark#(X1)	(65)
  mark#(add(X1,X2))	→	mark#(X2)	(66)
  mark#(len(X))	→	active#(len(mark(X)))	(67)
  mark#(len(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(fst)	=	1		weight(fst)	=	3
  prec(s)	=	0		weight(s)	=	3
  prec(add)	=	2		weight(add)	=	1
  prec(0)	=	3		weight(0)	=	6
  prec(nil)	=	4		weight(nil)	=	8

  in combination with the following argument filter

  π(active#)	=	1
  π(fst)	=	[1,2]
  π(s)	=	[]
  π(cons)	=	1
  π(mark#)	=	1
  π(mark)	=	1
  π(from)	=	1
  π(add)	=	[1,2]
  π(0)	=	[]
  π(len)	=	1
  π(active)	=	1
  π(nil)	=	[]

  the pairs

  active#(fst(s(X),cons(Y,Z)))	→	mark#(cons(Y,fst(X,Z)))	(35)
  mark#(fst(X1,X2))	→	mark#(X1)	(52)
  mark#(fst(X1,X2))	→	mark#(X2)	(53)
  active#(add(0,X))	→	mark#(X)	(42)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(43)
  mark#(add(X1,X2))	→	mark#(X1)	(65)
  mark#(add(X1,X2))	→	mark#(X2)	(66)

  could be deleted.

  1.1.1.1 Reduction Pair Processor

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

  prec(s)	=	0		weight(s)	=	3
  prec(len)	=	3		weight(len)	=	4
  prec(add)	=	1		weight(add)	=	3
  prec(0)	=	2		weight(0)	=	3
  prec(nil)	=	4		weight(nil)	=	1

  in combination with the following argument filter

  π(mark#)	=	1
  π(fst)	=	2
  π(active#)	=	1
  π(mark)	=	1
  π(from)	=	1
  π(cons)	=	1
  π(s)	=	[]
  π(len)	=	[1]
  π(add)	=	[2]
  π(active)	=	1
  π(0)	=	[]
  π(nil)	=	[]

  the pairs

  active#(len(cons(X,Z)))	→	mark#(s(len(Z)))	(47)
  mark#(len(X))	→	mark#(X)	(69)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor

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

  prec(from)	=	3		weight(from)	=	1
  prec(s)	=	0		weight(s)	=	3
  prec(add)	=	1		weight(add)	=	3
  prec(len)	=	4		weight(len)	=	5
  prec(0)	=	2		weight(0)	=	3
  prec(nil)	=	5		weight(nil)	=	1

  in combination with the following argument filter

  π(mark#)	=	1
  π(fst)	=	2
  π(active#)	=	1
  π(mark)	=	1
  π(from)	=	[1]
  π(cons)	=	1
  π(s)	=	[]
  π(add)	=	[2]
  π(len)	=	[]
  π(active)	=	1
  π(0)	=	[]
  π(nil)	=	[]

  the pairs

  active#(from(X))	→	mark#(cons(X,from(s(X))))	(38)
  mark#(from(X))	→	mark#(X)	(62)

  could be deleted.

  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#(cons(X1,X2))

    →

    mark#(X1)

    (59)

    1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the naturals

    [cons(x1, x2)]	=	1 · x1 + 1 · x2
    [mark#(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.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#(cons(X1,X2))	→	mark#(X1)	(59)
    1	>	1

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

• The 2^nd component contains the pair

  fst#(X1,mark(X2))	→	fst#(X1,X2)	(71)
  fst#(mark(X1),X2)	→	fst#(X1,X2)	(70)
  fst#(active(X1),X2)	→	fst#(X1,X2)	(72)
  fst#(X1,active(X2))	→	fst#(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
  [fst#(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.

  fst#(X1,mark(X2))	→	fst#(X1,X2)	(71)
  1	≥	1
  2	>	2
  fst#(mark(X1),X2)	→	fst#(X1,X2)	(70)
  1	>	1
  2	≥	2
  fst#(active(X1),X2)	→	fst#(X1,X2)	(72)
  1	>	1
  2	≥	2
  fst#(X1,active(X2))	→	fst#(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

  cons#(X1,mark(X2))	→	cons#(X1,X2)	(77)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(76)
  cons#(active(X1),X2)	→	cons#(X1,X2)	(78)
  cons#(X1,active(X2))	→	cons#(X1,X2)	(79)

  1.1.4 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.4.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)	(77)
  1	≥	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(76)
  1	>	1
  2	≥	2
  cons#(active(X1),X2)	→	cons#(X1,X2)	(78)
  1	>	1
  2	≥	2
  cons#(X1,active(X2))	→	cons#(X1,X2)	(79)
  1	≥	1
  2	>	2

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

• The 5^th component contains the pair

  from#(active(X))	→	from#(X)	(81)
  from#(mark(X))	→	from#(X)	(80)

  1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

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

  from#(active(X))	→	from#(X)	(81)
  1	>	1
  from#(mark(X))	→	from#(X)	(80)
  1	>	1

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

• The 6^th component contains the pair

  add#(X1,mark(X2))	→	add#(X1,X2)	(83)
  add#(mark(X1),X2)	→	add#(X1,X2)	(82)
  add#(active(X1),X2)	→	add#(X1,X2)	(84)
  add#(X1,active(X2))	→	add#(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
  [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.6.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)	(83)
  1	≥	1
  2	>	2
  add#(mark(X1),X2)	→	add#(X1,X2)	(82)
  1	>	1
  2	≥	2
  add#(active(X1),X2)	→	add#(X1,X2)	(84)
  1	>	1
  2	≥	2
  add#(X1,active(X2))	→	add#(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

  len#(active(X))	→	len#(X)	(87)
  len#(mark(X))	→	len#(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
  [len#(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.

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

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