Certification Problem

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

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(97)
  top#(mark(X))	→	top#(proper(X))	(95)

  1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [proper(x1)]	=	1 · x1
  [app(x1, x2)]	=	1 · x1 + 1 · x2
  [nil]	=	0
  [ok(x1)]	=	2 · x1
  [cons(x1, x2)]	=	2 · x1 + 1 · x2
  [from(x1)]	=	2 · x1
  [s(x1)]	=	1 · x1
  [zWadr(x1, x2)]	=	1 · x1 + 1 · x2
  [prefix(x1)]	=	2 · x1
  [mark(x1)]	=	1 · x1
  [active(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  proper(app(X1,X2))	→	app(proper(X1),proper(X2))	(24)
  proper(nil)	→	ok(nil)	(25)
  proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(26)
  proper(from(X))	→	from(proper(X))	(27)
  proper(s(X))	→	s(proper(X))	(28)
  proper(zWadr(X1,X2))	→	zWadr(proper(X1),proper(X2))	(29)
  proper(prefix(X))	→	prefix(proper(X))	(30)
  prefix(mark(X))	→	mark(prefix(X))	(23)
  prefix(ok(X))	→	ok(prefix(X))	(36)
  zWadr(mark(X1),X2)	→	mark(zWadr(X1,X2))	(21)
  zWadr(X1,mark(X2))	→	mark(zWadr(X1,X2))	(22)
  zWadr(ok(X1),ok(X2))	→	ok(zWadr(X1,X2))	(35)
  s(mark(X))	→	mark(s(X))	(20)
  s(ok(X))	→	ok(s(X))	(34)
  from(mark(X))	→	mark(from(X))	(19)
  from(ok(X))	→	ok(from(X))	(33)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(18)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
  app(mark(X1),X2)	→	mark(app(X1,X2))	(16)
  app(X1,mark(X2))	→	mark(app(X1,X2))	(17)
  app(ok(X1),ok(X2))	→	ok(app(X1,X2))	(31)
  active(app(nil,YS))	→	mark(YS)	(1)
  active(app(cons(X,XS),YS))	→	mark(cons(X,app(XS,YS)))	(2)
  active(from(X))	→	mark(cons(X,from(s(X))))	(3)
  active(zWadr(nil,YS))	→	mark(nil)	(4)
  active(zWadr(XS,nil))	→	mark(nil)	(5)
  active(zWadr(cons(X,XS),cons(Y,YS)))	→	mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))	(6)
  active(prefix(L))	→	mark(cons(nil,zWadr(L,prefix(L))))	(7)
  active(app(X1,X2))	→	app(active(X1),X2)	(8)
  active(app(X1,X2))	→	app(X1,active(X2))	(9)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
  active(from(X))	→	from(active(X))	(11)
  active(s(X))	→	s(active(X))	(12)
  active(zWadr(X1,X2))	→	zWadr(active(X1),X2)	(13)
  active(zWadr(X1,X2))	→	zWadr(X1,active(X2))	(14)
  active(prefix(X))	→	prefix(active(X))	(15)

  (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

  prec(mark)	=	0		stat(mark)	=	lex
  prec(app)	=	1		stat(app)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(from)	=	0		stat(from)	=	lex
  prec(s)	=	2		stat(s)	=	lex
  prec(zWadr)	=	3		stat(zWadr)	=	lex
  prec(prefix)	=	4		stat(prefix)	=	lex

  π(top#)	=	1
  π(ok)	=	1
  π(active)	=	1
  π(mark)	=	[1]
  π(proper)	=	1
  π(app)	=	[2,1]
  π(nil)	=	[]
  π(cons)	=	1
  π(from)	=	[1]
  π(s)	=	[1]
  π(zWadr)	=	[2,1]
  π(prefix)	=	[1]

  the pair

  top#(mark(X))

  →

  top#(proper(X))

  (95)

  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
  [app(x1, x2)]	=	1 · x1 + 2 · x2
  [nil]	=	0
  [mark(x1)]	=	1 · x1
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [from(x1)]	=	2 · x1
  [s(x1)]	=	1 · x1
  [zWadr(x1, x2)]	=	1 · x1 + 1 · x2
  [prefix(x1)]	=	1 · x1
  [ok(x1)]	=	2 · x1
  [top#(x1)]	=	1 · x1

  together with the usable rules

  active(app(nil,YS))	→	mark(YS)	(1)
  active(app(cons(X,XS),YS))	→	mark(cons(X,app(XS,YS)))	(2)
  active(from(X))	→	mark(cons(X,from(s(X))))	(3)
  active(zWadr(nil,YS))	→	mark(nil)	(4)
  active(zWadr(XS,nil))	→	mark(nil)	(5)
  active(zWadr(cons(X,XS),cons(Y,YS)))	→	mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))	(6)
  active(prefix(L))	→	mark(cons(nil,zWadr(L,prefix(L))))	(7)
  active(app(X1,X2))	→	app(active(X1),X2)	(8)
  active(app(X1,X2))	→	app(X1,active(X2))	(9)
  active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
  active(from(X))	→	from(active(X))	(11)
  active(s(X))	→	s(active(X))	(12)
  active(zWadr(X1,X2))	→	zWadr(active(X1),X2)	(13)
  active(zWadr(X1,X2))	→	zWadr(X1,active(X2))	(14)
  active(prefix(X))	→	prefix(active(X))	(15)
  prefix(mark(X))	→	mark(prefix(X))	(23)
  prefix(ok(X))	→	ok(prefix(X))	(36)
  zWadr(mark(X1),X2)	→	mark(zWadr(X1,X2))	(21)
  zWadr(X1,mark(X2))	→	mark(zWadr(X1,X2))	(22)
  zWadr(ok(X1),ok(X2))	→	ok(zWadr(X1,X2))	(35)
  s(mark(X))	→	mark(s(X))	(20)
  s(ok(X))	→	ok(s(X))	(34)
  from(mark(X))	→	mark(from(X))	(19)
  from(ok(X))	→	ok(from(X))	(33)
  cons(mark(X1),X2)	→	mark(cons(X1,X2))	(18)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
  app(mark(X1),X2)	→	mark(app(X1,X2))	(16)
  app(X1,mark(X2))	→	mark(app(X1,X2))	(17)
  app(ok(X1),ok(X2))	→	ok(app(X1,X2))	(31)

  (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
  [app(x1, x2)]	=	1 · x1 + 1 · x2
  [nil]	=	0
  [mark(x1)]	=	1 · x1
  [cons(x1, x2)]	=	2 · x1 + 1 · x2
  [from(x1)]	=	2 · x1
  [s(x1)]	=	1 · x1
  [zWadr(x1, x2)]	=	1 · x1 + 1 · x2
  [prefix(x1)]	=	1 · x1
  [ok(x1)]	=	1 + 2 · x1
  [top#(x1)]	=	2 · x1

  the pair

  top#(ok(X))

  →

  top#(active(X))

  (97)

  and the rules

  zWadr(ok(X1),ok(X2))	→	ok(zWadr(X1,X2))	(35)
  from(ok(X))	→	ok(from(X))	(33)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
  app(ok(X1),ok(X2))	→	ok(app(X1,X2))	(31)

  could be deleted.

  1.1.1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  active#(app(X1,X2))	→	active#(X2)	(53)
  active#(app(X1,X2))	→	active#(X1)	(51)
  active#(cons(X1,X2))	→	active#(X1)	(55)
  active#(from(X))	→	active#(X)	(57)
  active#(s(X))	→	active#(X)	(59)
  active#(zWadr(X1,X2))	→	active#(X1)	(61)
  active#(zWadr(X1,X2))	→	active#(X2)	(63)
  active#(prefix(X))	→	active#(X)	(65)

  1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [app(x1, x2)]	=	1 · x1 + 1 · x2
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [from(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [zWadr(x1, x2)]	=	1 · x1 + 1 · x2
  [prefix(x1)]	=	1 · x1
  [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#(app(X1,X2))	→	active#(X2)	(53)
  1	>	1
  active#(app(X1,X2))	→	active#(X1)	(51)
  1	>	1
  active#(cons(X1,X2))	→	active#(X1)	(55)
  1	>	1
  active#(from(X))	→	active#(X)	(57)
  1	>	1
  active#(s(X))	→	active#(X)	(59)
  1	>	1
  active#(zWadr(X1,X2))	→	active#(X1)	(61)
  1	>	1
  active#(zWadr(X1,X2))	→	active#(X2)	(63)
  1	>	1
  active#(prefix(X))	→	active#(X)	(65)
  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#(app(X1,X2))	→	proper#(X2)	(76)
  proper#(app(X1,X2))	→	proper#(X1)	(75)
  proper#(cons(X1,X2))	→	proper#(X1)	(78)
  proper#(cons(X1,X2))	→	proper#(X2)	(79)
  proper#(from(X))	→	proper#(X)	(81)
  proper#(s(X))	→	proper#(X)	(83)
  proper#(zWadr(X1,X2))	→	proper#(X1)	(85)
  proper#(zWadr(X1,X2))	→	proper#(X2)	(86)
  proper#(prefix(X))	→	proper#(X)	(88)

  1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [app(x1, x2)]	=	1 · x1 + 1 · x2
  [cons(x1, x2)]	=	1 · x1 + 1 · x2
  [from(x1)]	=	1 · x1
  [s(x1)]	=	1 · x1
  [zWadr(x1, x2)]	=	1 · x1 + 1 · x2
  [prefix(x1)]	=	1 · x1
  [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#(app(X1,X2))	→	proper#(X2)	(76)
  1	>	1
  proper#(app(X1,X2))	→	proper#(X1)	(75)
  1	>	1
  proper#(cons(X1,X2))	→	proper#(X1)	(78)
  1	>	1
  proper#(cons(X1,X2))	→	proper#(X2)	(79)
  1	>	1
  proper#(from(X))	→	proper#(X)	(81)
  1	>	1
  proper#(s(X))	→	proper#(X)	(83)
  1	>	1
  proper#(zWadr(X1,X2))	→	proper#(X1)	(85)
  1	>	1
  proper#(zWadr(X1,X2))	→	proper#(X2)	(86)
  1	>	1
  proper#(prefix(X))	→	proper#(X)	(88)
  1	>	1

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

• The 4^th component contains the pair

  app#(X1,mark(X2))	→	app#(X1,X2)	(67)
  app#(mark(X1),X2)	→	app#(X1,X2)	(66)
  app#(ok(X1),ok(X2))	→	app#(X1,X2)	(89)

  1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

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

  app#(X1,mark(X2))	→	app#(X1,X2)	(67)
  1	≥	1
  2	>	2
  app#(mark(X1),X2)	→	app#(X1,X2)	(66)
  1	>	1
  2	≥	2
  app#(ok(X1),ok(X2))	→	app#(X1,X2)	(89)
  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

  cons#(ok(X1),ok(X2))	→	cons#(X1,X2)	(90)
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(68)

  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)	(90)
  1	>	1
  2	>	2
  cons#(mark(X1),X2)	→	cons#(X1,X2)	(68)
  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

  from#(ok(X))	→	from#(X)	(91)
  from#(mark(X))	→	from#(X)	(69)

  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
  [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.6.1 Size-Change Termination

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

  from#(ok(X))	→	from#(X)	(91)
  1	>	1
  from#(mark(X))	→	from#(X)	(69)
  1	>	1

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

• The 7^th component contains the pair

  s#(ok(X))	→	s#(X)	(92)
  s#(mark(X))	→	s#(X)	(70)

  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
  [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.7.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)	(92)
  1	>	1
  s#(mark(X))	→	s#(X)	(70)
  1	>	1

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

• The 8^th component contains the pair

  zWadr#(X1,mark(X2))	→	zWadr#(X1,X2)	(72)
  zWadr#(mark(X1),X2)	→	zWadr#(X1,X2)	(71)
  zWadr#(ok(X1),ok(X2))	→	zWadr#(X1,X2)	(93)

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

  zWadr#(X1,mark(X2))	→	zWadr#(X1,X2)	(72)
  1	≥	1
  2	>	2
  zWadr#(mark(X1),X2)	→	zWadr#(X1,X2)	(71)
  1	>	1
  2	≥	2
  zWadr#(ok(X1),ok(X2))	→	zWadr#(X1,X2)	(93)
  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

  prefix#(ok(X))	→	prefix#(X)	(94)
  prefix#(mark(X))	→	prefix#(X)	(73)

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

  prefix#(ok(X))	→	prefix#(X)	(94)
  1	>	1
  prefix#(mark(X))	→	prefix#(X)	(73)
  1	>	1

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