Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex15_Luc98_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 8 components.

• The 1^st component contains the pair

  mark#(and(X1,X2))	→	active#(and(mark(X1),X2))	(63)
  active#(and(true,X))	→	mark#(X)	(47)
  mark#(and(X1,X2))	→	mark#(X1)	(65)
  mark#(if(X1,X2,X3))	→	active#(if(mark(X1),X2,X3))	(68)
  active#(if(true,X,Y))	→	mark#(X)	(49)
  mark#(if(X1,X2,X3))	→	mark#(X1)	(70)
  mark#(add(X1,X2))	→	active#(add(mark(X1),X2))	(71)
  active#(if(false,X,Y))	→	mark#(Y)	(50)
  mark#(add(X1,X2))	→	mark#(X1)	(73)
  mark#(s(X))	→	active#(s(X))	(75)
  active#(add(0,X))	→	mark#(X)	(51)
  mark#(first(X1,X2))	→	active#(first(mark(X1),mark(X2)))	(76)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(52)
  mark#(first(X1,X2))	→	mark#(X1)	(78)
  mark#(first(X1,X2))	→	mark#(X2)	(79)
  mark#(cons(X1,X2))	→	active#(cons(X1,X2))	(81)
  active#(first(s(X),cons(Y,Z)))	→	mark#(cons(Y,first(X,Z)))	(56)
  mark#(from(X))	→	active#(from(X))	(82)
  active#(from(X))	→	mark#(cons(X,from(s(X))))	(59)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark#(x1)]	=	1
  [and(x1, x2)]	=	1
  [active#(x1)]	=	1 · x1
  [mark(x1)]	=	0
  [true]	=	0
  [if(x1, x2, x3)]	=	1
  [add(x1, x2)]	=	1
  [false]	=	0
  [s(x1)]	=	0
  [0]	=	0
  [first(x1, x2)]	=	1
  [cons(x1, x2)]	=	0
  [from(x1)]	=	1
  [active(x1)]	=	0
  [nil]	=	0

  together with the usable rules

  and(X1,mark(X2))	→	and(X1,X2)	(22)
  and(mark(X1),X2)	→	and(X1,X2)	(21)
  and(active(X1),X2)	→	and(X1,X2)	(23)
  and(X1,active(X2))	→	and(X1,X2)	(24)
  if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(26)
  if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(25)
  if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(27)
  if(active(X1),X2,X3)	→	if(X1,X2,X3)	(28)
  if(X1,active(X2),X3)	→	if(X1,X2,X3)	(29)
  if(X1,X2,active(X3))	→	if(X1,X2,X3)	(30)
  add(X1,mark(X2))	→	add(X1,X2)	(32)
  add(mark(X1),X2)	→	add(X1,X2)	(31)
  add(active(X1),X2)	→	add(X1,X2)	(33)
  add(X1,active(X2))	→	add(X1,X2)	(34)
  s(active(X))	→	s(X)	(36)
  s(mark(X))	→	s(X)	(35)
  first(X1,mark(X2))	→	first(X1,X2)	(38)
  first(mark(X1),X2)	→	first(X1,X2)	(37)
  first(active(X1),X2)	→	first(X1,X2)	(39)
  first(X1,active(X2))	→	first(X1,X2)	(40)
  cons(X1,mark(X2))	→	cons(X1,X2)	(42)
  cons(mark(X1),X2)	→	cons(X1,X2)	(41)
  cons(active(X1),X2)	→	cons(X1,X2)	(43)
  cons(X1,active(X2))	→	cons(X1,X2)	(44)
  from(active(X))	→	from(X)	(46)
  from(mark(X))	→	from(X)	(45)

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

  mark#(s(X))	→	active#(s(X))	(75)
  mark#(cons(X1,X2))	→	active#(cons(X1,X2))	(81)

  could be deleted.

  1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [mark#(x1)]	=	1 · x1
  [and(x1, x2)]	=	1 · x1 + 1 · x2
  [active#(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [true]	=	1
  [if(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [add(x1, x2)]	=	1 + 1 · x1 + 1 · x2
  [false]	=	0
  [0]	=	1
  [first(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	0
  [cons(x1, x2)]	=	0
  [from(x1)]	=	0
  [active(x1)]	=	1 · x1
  [nil]	=	0

  the pairs

  active#(and(true,X))	→	mark#(X)	(47)
  active#(if(true,X,Y))	→	mark#(X)	(49)
  mark#(add(X1,X2))	→	mark#(X1)	(73)
  active#(add(0,X))	→	mark#(X)	(51)
  active#(add(s(X),Y))	→	mark#(s(add(X,Y)))	(52)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark#(x1)]	=	1
  [and(x1, x2)]	=	0
  [active#(x1)]	=	1 · x1
  [mark(x1)]	=	0
  [if(x1, x2, x3)]	=	1
  [add(x1, x2)]	=	0
  [false]	=	0
  [first(x1, x2)]	=	1
  [s(x1)]	=	0
  [cons(x1, x2)]	=	1 · x1
  [from(x1)]	=	1
  [active(x1)]	=	0
  [true]	=	0
  [0]	=	0
  [nil]	=	0

  together with the usable rules

  and(X1,mark(X2))	→	and(X1,X2)	(22)
  and(mark(X1),X2)	→	and(X1,X2)	(21)
  and(active(X1),X2)	→	and(X1,X2)	(23)
  and(X1,active(X2))	→	and(X1,X2)	(24)
  if(X1,mark(X2),X3)	→	if(X1,X2,X3)	(26)
  if(mark(X1),X2,X3)	→	if(X1,X2,X3)	(25)
  if(X1,X2,mark(X3))	→	if(X1,X2,X3)	(27)
  if(active(X1),X2,X3)	→	if(X1,X2,X3)	(28)
  if(X1,active(X2),X3)	→	if(X1,X2,X3)	(29)
  if(X1,X2,active(X3))	→	if(X1,X2,X3)	(30)
  add(X1,mark(X2))	→	add(X1,X2)	(32)
  add(mark(X1),X2)	→	add(X1,X2)	(31)
  add(active(X1),X2)	→	add(X1,X2)	(33)
  add(X1,active(X2))	→	add(X1,X2)	(34)
  first(X1,mark(X2))	→	first(X1,X2)	(38)
  first(mark(X1),X2)	→	first(X1,X2)	(37)
  first(active(X1),X2)	→	first(X1,X2)	(39)
  first(X1,active(X2))	→	first(X1,X2)	(40)
  from(active(X))	→	from(X)	(46)
  from(mark(X))	→	from(X)	(45)

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

  mark#(and(X1,X2))	→	active#(and(mark(X1),X2))	(63)
  mark#(add(X1,X2))	→	active#(add(mark(X1),X2))	(71)

  could be deleted.

  1.1.1.1.1.1 Reduction Pair Processor

  Using the linear polynomial interpretation over the naturals

  [mark#(x1)]	=	1 · x1
  [and(x1, x2)]	=	1 · x1 + 1 · x2
  [if(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3
  [active#(x1)]	=	1 · x1
  [mark(x1)]	=	1 · x1
  [false]	=	1
  [first(x1, x2)]	=	1 · x1 + 1 · x2
  [s(x1)]	=	0
  [cons(x1, x2)]	=	0
  [from(x1)]	=	0
  [active(x1)]	=	1 · x1
  [true]	=	0
  [add(x1, x2)]	=	1 · x2
  [0]	=	0
  [nil]	=	0

  the pair

  active#(if(false,X,Y))

  →

  mark#(Y)

  (50)

  could be deleted.

  1.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(if)	=	0		weight(if)	=	1
  prec(active#)	=	2		weight(active#)	=	1
  prec(first)	=	3		weight(first)	=	1
  prec(cons)	=	1		weight(cons)	=	1
  prec(from)	=	4		weight(from)	=	2

  in combination with the following argument filter

  π(mark#)	=	1
  π(and)	=	1
  π(if)	=	[1]
  π(active#)	=	[]
  π(first)	=	[1,2]
  π(cons)	=	[]
  π(from)	=	[]

  together with the usable rules

  cons(X1,mark(X2))	→	cons(X1,X2)	(42)
  cons(mark(X1),X2)	→	cons(X1,X2)	(41)
  cons(active(X1),X2)	→	cons(X1,X2)	(43)
  cons(X1,active(X2))	→	cons(X1,X2)	(44)

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

  mark#(if(X1,X2,X3))	→	active#(if(mark(X1),X2,X3))	(68)
  mark#(if(X1,X2,X3))	→	mark#(X1)	(70)
  mark#(first(X1,X2))	→	active#(first(mark(X1),mark(X2)))	(76)
  mark#(first(X1,X2))	→	mark#(X1)	(78)
  mark#(first(X1,X2))	→	mark#(X2)	(79)
  active#(first(s(X),cons(Y,Z)))	→	mark#(cons(Y,first(X,Z)))	(56)
  mark#(from(X))	→	active#(from(X))	(82)
  active#(from(X))	→	mark#(cons(X,from(s(X))))	(59)

  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

  [and(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.1 Size-Change Termination

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

  mark#(and(X1,X2))	→	mark#(X1)	(65)
  1	>	1

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

• The 2^nd component contains the pair

  and#(X1,mark(X2))	→	and#(X1,X2)	(84)
  and#(mark(X1),X2)	→	and#(X1,X2)	(83)
  and#(active(X1),X2)	→	and#(X1,X2)	(85)
  and#(X1,active(X2))	→	and#(X1,X2)	(86)

  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
  [and#(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.

  and#(X1,mark(X2))	→	and#(X1,X2)	(84)
  1	≥	1
  2	>	2
  and#(mark(X1),X2)	→	and#(X1,X2)	(83)
  1	>	1
  2	≥	2
  and#(active(X1),X2)	→	and#(X1,X2)	(85)
  1	>	1
  2	≥	2
  and#(X1,active(X2))	→	and#(X1,X2)	(86)
  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

  if#(X1,mark(X2),X3)	→	if#(X1,X2,X3)	(88)
  if#(mark(X1),X2,X3)	→	if#(X1,X2,X3)	(87)
  if#(X1,X2,mark(X3))	→	if#(X1,X2,X3)	(89)
  if#(active(X1),X2,X3)	→	if#(X1,X2,X3)	(90)
  if#(X1,active(X2),X3)	→	if#(X1,X2,X3)	(91)
  if#(X1,X2,active(X3))	→	if#(X1,X2,X3)	(92)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [mark(x1)]	=	1 · x1
  [active(x1)]	=	1 · x1
  [if#(x1, x2, x3)]	=	1 · x1 + 1 · x2 + 1 · x3

  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.

  if#(X1,mark(X2),X3)	→	if#(X1,X2,X3)	(88)
  1	≥	1
  2	>	2
  3	≥	3
  if#(mark(X1),X2,X3)	→	if#(X1,X2,X3)	(87)
  1	>	1
  2	≥	2
  3	≥	3
  if#(X1,X2,mark(X3))	→	if#(X1,X2,X3)	(89)
  1	≥	1
  2	≥	2
  3	>	3
  if#(active(X1),X2,X3)	→	if#(X1,X2,X3)	(90)
  1	>	1
  2	≥	2
  3	≥	3
  if#(X1,active(X2),X3)	→	if#(X1,X2,X3)	(91)
  1	≥	1
  2	>	2
  3	≥	3
  if#(X1,X2,active(X3))	→	if#(X1,X2,X3)	(92)
  1	≥	1
  2	≥	2
  3	>	3

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

• The 4^th component contains the pair

  add#(X1,mark(X2))	→	add#(X1,X2)	(94)
  add#(mark(X1),X2)	→	add#(X1,X2)	(93)
  add#(active(X1),X2)	→	add#(X1,X2)	(95)
  add#(X1,active(X2))	→	add#(X1,X2)	(96)

  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
  [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.4.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)	(94)
  1	≥	1
  2	>	2
  add#(mark(X1),X2)	→	add#(X1,X2)	(93)
  1	>	1
  2	≥	2
  add#(active(X1),X2)	→	add#(X1,X2)	(95)
  1	>	1
  2	≥	2
  add#(X1,active(X2))	→	add#(X1,X2)	(96)
  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

  s#(active(X))	→	s#(X)	(98)
  s#(mark(X))	→	s#(X)	(97)

  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
  [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.5.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)	(98)
  1	>	1
  s#(mark(X))	→	s#(X)	(97)
  1	>	1

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

• The 6^th component contains the pair

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

  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
  [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.6.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)	(100)
  1	≥	1
  2	>	2
  first#(mark(X1),X2)	→	first#(X1,X2)	(99)
  1	>	1
  2	≥	2
  first#(active(X1),X2)	→	first#(X1,X2)	(101)
  1	>	1
  2	≥	2
  first#(X1,active(X2))	→	first#(X1,X2)	(102)
  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

  cons#(X1,mark(X2))	→	cons#(X1,X2)	(104)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(103)
  cons#(active(X1),X2)	→	cons#(X1,X2)	(105)
  cons#(X1,active(X2))	→	cons#(X1,X2)	(106)

  1.1.7 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.7.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)	(104)
  1	≥	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(103)
  1	>	1
  2	≥	2
  cons#(active(X1),X2)	→	cons#(X1,X2)	(105)
  1	>	1
  2	≥	2
  cons#(X1,active(X2))	→	cons#(X1,X2)	(106)
  1	≥	1
  2	>	2

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

• The 8^th component contains the pair

  from#(active(X))	→	from#(X)	(108)
  from#(mark(X))	→	from#(X)	(107)

  1.1.8 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.8.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)	(108)
  1	>	1
  from#(mark(X))	→	from#(X)	(107)
  1	>	1

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