Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_3_25_Bor03_GM)

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 1 component.

• The 1^st component contains the pair

  a__zWadr#(cons(X,XS),cons(Y,YS))	→	mark#(Y)	(23)
  mark#(app(X1,X2))	→	mark#(X2)	(25)
  mark#(app(X1,X2))	→	mark#(X1)	(26)
  mark#(app(X1,X2))	→	a__app#(mark(X1),mark(X2))	(27)
  a__app#(nil,YS)	→	mark#(YS)	(19)
  mark#(from(X))	→	mark#(X)	(28)
  mark#(from(X))	→	a__from#(mark(X))	(29)
  a__from#(X)	→	mark#(X)	(21)
  mark#(zWadr(X1,X2))	→	mark#(X2)	(30)
  mark#(zWadr(X1,X2))	→	mark#(X1)	(31)
  mark#(zWadr(X1,X2))	→	a__zWadr#(mark(X1),mark(X2))	(32)
  a__zWadr#(cons(X,XS),cons(Y,YS))	→	mark#(X)	(22)
  mark#(prefix(X))	→	mark#(X)	(33)
  mark#(cons(X1,X2))	→	mark#(X1)	(35)
  mark#(s(X))	→	mark#(X)	(36)
  a__zWadr#(cons(X,XS),cons(Y,YS))	→	a__app#(mark(Y),cons(mark(X),nil))	(24)
  a__app#(cons(X,XS),YS)	→	mark#(X)	(20)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__zWadr#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [cons(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__from(x1)]	=	0 · x1 + 0
  [a__prefix(x1)]	=	1 · x1 + 1
  [nil]	=	0
  [from(x1)]	=	0 · x1 + -∞
  [a__from#(x1)]	=	0 · x1 + 0
  [a__app#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [prefix(x1)]	=	1 · x1 + 1
  [zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [mark#(x1)]	=	0 · x1 + 0
  [s(x1)]	=	0 · x1 + -∞
  [mark(x1)]	=	0 · x1 + 0

  together with the usable rules

  a__app(nil,YS)	→	mark(YS)	(1)
  a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
  a__from(X)	→	cons(mark(X),from(s(X)))	(3)
  a__zWadr(nil,YS)	→	nil	(4)
  a__zWadr(XS,nil)	→	nil	(5)
  a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
  a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
  mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
  mark(from(X))	→	a__from(mark(X))	(9)
  mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
  mark(prefix(X))	→	a__prefix(mark(X))	(11)
  mark(nil)	→	nil	(12)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
  mark(s(X))	→	s(mark(X))	(14)
  a__app(X1,X2)	→	app(X1,X2)	(15)
  a__from(X)	→	from(X)	(16)
  a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
  a__prefix(X)	→	prefix(X)	(18)

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

  mark#(prefix(X))

  →

  mark#(X)

  (33)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__zWadr#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [cons(x1, x2)]	=	0 · x1 + -∞ · x2 + 0
  [a__from(x1)]	=	0 · x1 + 0
  [a__prefix(x1)]	=	-∞ · x1 + 3
  [nil]	=	0
  [from(x1)]	=	0 · x1 + 0
  [a__from#(x1)]	=	0 · x1 + 0
  [a__app#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [prefix(x1)]	=	-∞ · x1 + 3
  [zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [mark#(x1)]	=	0 · x1 + 0
  [s(x1)]	=	3 · x1 + 4
  [mark(x1)]	=	0 · x1 + 0

  together with the usable rules

  a__app(nil,YS)	→	mark(YS)	(1)
  a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
  a__from(X)	→	cons(mark(X),from(s(X)))	(3)
  a__zWadr(nil,YS)	→	nil	(4)
  a__zWadr(XS,nil)	→	nil	(5)
  a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
  a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
  mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
  mark(from(X))	→	a__from(mark(X))	(9)
  mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
  mark(prefix(X))	→	a__prefix(mark(X))	(11)
  mark(nil)	→	nil	(12)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
  mark(s(X))	→	s(mark(X))	(14)
  a__app(X1,X2)	→	app(X1,X2)	(15)
  a__from(X)	→	from(X)	(16)
  a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
  a__prefix(X)	→	prefix(X)	(18)

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

  mark#(s(X))

  →

  mark#(X)

  (36)

  could be deleted.

  1.1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the arctic semiring over the integers

  [app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [a__zWadr#(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [a__zWadr(x1, x2)]	=	7 · x1 + 7 · x2 + 0
  [a__app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
  [cons(x1, x2)]	=	0 · x1 + -∞ · x2 + 0
  [a__from(x1)]	=	0 · x1 + 2
  [a__prefix(x1)]	=	-∞ · x1 + 0
  [nil]	=	0
  [from(x1)]	=	0 · x1 + 2
  [a__from#(x1)]	=	0 · x1 + 0
  [a__app#(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
  [prefix(x1)]	=	-∞ · x1 + 0
  [zWadr(x1, x2)]	=	7 · x1 + 7 · x2 + 0
  [mark#(x1)]	=	0 · x1 + 0
  [s(x1)]	=	0 · x1 + 3
  [mark(x1)]	=	0 · x1 + -∞

  together with the usable rules

  a__app(nil,YS)	→	mark(YS)	(1)
  a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
  a__from(X)	→	cons(mark(X),from(s(X)))	(3)
  a__zWadr(nil,YS)	→	nil	(4)
  a__zWadr(XS,nil)	→	nil	(5)
  a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
  a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
  mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
  mark(from(X))	→	a__from(mark(X))	(9)
  mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
  mark(prefix(X))	→	a__prefix(mark(X))	(11)
  mark(nil)	→	nil	(12)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
  mark(s(X))	→	s(mark(X))	(14)
  a__app(X1,X2)	→	app(X1,X2)	(15)
  a__from(X)	→	from(X)	(16)
  a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
  a__prefix(X)	→	prefix(X)	(18)

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

  mark#(zWadr(X1,X2))

  →

  a__zWadr#(mark(X1),mark(X2))

  (32)

  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#(app(X1,X2))	→	mark#(X2)	(25)
    mark#(app(X1,X2))	→	mark#(X1)	(26)
    mark#(app(X1,X2))	→	a__app#(mark(X1),mark(X2))	(27)
    a__app#(nil,YS)	→	mark#(YS)	(19)
    mark#(from(X))	→	mark#(X)	(28)
    mark#(from(X))	→	a__from#(mark(X))	(29)
    a__from#(X)	→	mark#(X)	(21)
    mark#(zWadr(X1,X2))	→	mark#(X2)	(30)
    mark#(zWadr(X1,X2))	→	mark#(X1)	(31)
    mark#(cons(X1,X2))	→	mark#(X1)	(35)
    a__app#(cons(X,XS),YS)	→	mark#(X)	(20)

    1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the arctic semiring over the integers

    [app(x1, x2)]	=	6 · x1 + 0 · x2 + -∞
    [a__zWadr(x1, x2)]	=	0 · x1 + 6 · x2 + -∞
    [a__app(x1, x2)]	=	6 · x1 + 0 · x2 + -∞
    [cons(x1, x2)]	=	0 · x1 + -∞ · x2 + 0
    [a__from(x1)]	=	0 · x1 + 0
    [a__prefix(x1)]	=	0 · x1 + 0
    [nil]	=	0
    [from(x1)]	=	0 · x1 + 0
    [a__from#(x1)]	=	0 · x1 + -∞
    [a__app#(x1, x2)]	=	6 · x1 + 0 · x2 + -∞
    [prefix(x1)]	=	0 · x1 + 0
    [zWadr(x1, x2)]	=	0 · x1 + 6 · x2 + -∞
    [mark#(x1)]	=	0 · x1 + -∞
    [s(x1)]	=	-∞ · x1 + 1
    [mark(x1)]	=	0 · x1 + -∞

    together with the usable rules

    a__app(nil,YS)	→	mark(YS)	(1)
    a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
    a__from(X)	→	cons(mark(X),from(s(X)))	(3)
    a__zWadr(nil,YS)	→	nil	(4)
    a__zWadr(XS,nil)	→	nil	(5)
    a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
    a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
    mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
    mark(from(X))	→	a__from(mark(X))	(9)
    mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
    mark(prefix(X))	→	a__prefix(mark(X))	(11)
    mark(nil)	→	nil	(12)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
    mark(s(X))	→	s(mark(X))	(14)
    a__app(X1,X2)	→	app(X1,X2)	(15)
    a__from(X)	→	from(X)	(16)
    a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
    a__prefix(X)	→	prefix(X)	(18)

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

    mark#(app(X1,X2))	→	mark#(X1)	(26)
    mark#(zWadr(X1,X2))	→	mark#(X2)	(30)
    a__app#(cons(X,XS),YS)	→	mark#(X)	(20)

    could be deleted.

    1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the arctic semiring over the integers

    [app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [a__zWadr(x1, x2)]	=	1 · x1 + 0 · x2 + 0
    [a__app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [cons(x1, x2)]	=	0 · x1 + -∞ · x2 + -∞
    [a__from(x1)]	=	0 · x1 + -∞
    [a__prefix(x1)]	=	-∞ · x1 + 0
    [nil]	=	0
    [from(x1)]	=	0 · x1 + -∞
    [a__from#(x1)]	=	0 · x1 + -∞
    [a__app#(x1, x2)]	=	0 · x1 + 0 · x2 + 0
    [prefix(x1)]	=	-∞ · x1 + 0
    [zWadr(x1, x2)]	=	1 · x1 + 0 · x2 + 0
    [mark#(x1)]	=	0 · x1 + -∞
    [s(x1)]	=	1 · x1 + -∞
    [mark(x1)]	=	0 · x1 + -∞

    together with the usable rules

    a__app(nil,YS)	→	mark(YS)	(1)
    a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
    a__from(X)	→	cons(mark(X),from(s(X)))	(3)
    a__zWadr(nil,YS)	→	nil	(4)
    a__zWadr(XS,nil)	→	nil	(5)
    a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
    a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
    mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
    mark(from(X))	→	a__from(mark(X))	(9)
    mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
    mark(prefix(X))	→	a__prefix(mark(X))	(11)
    mark(nil)	→	nil	(12)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
    mark(s(X))	→	s(mark(X))	(14)
    a__app(X1,X2)	→	app(X1,X2)	(15)
    a__from(X)	→	from(X)	(16)
    a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
    a__prefix(X)	→	prefix(X)	(18)

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

    mark#(zWadr(X1,X2))

    →

    mark#(X1)

    (31)

    could be deleted.

    1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the linear polynomial interpretation over the arctic semiring over the integers

    [app(x1, x2)]	=	1 · x1 + 5 · x2 + -∞
    [a__zWadr(x1, x2)]	=	6 · x1 + 2 · x2 + 0
    [a__app(x1, x2)]	=	1 · x1 + 5 · x2 + -∞
    [cons(x1, x2)]	=	1 · x1 + -∞ · x2 + 0
    [a__from(x1)]	=	1 · x1 + 0
    [a__prefix(x1)]	=	0 · x1 + 1
    [nil]	=	0
    [from(x1)]	=	1 · x1 + 0
    [a__from#(x1)]	=	0 · x1 + 0
    [a__app#(x1, x2)]	=	0 · x1 + 4 · x2 + -∞
    [prefix(x1)]	=	0 · x1 + 1
    [zWadr(x1, x2)]	=	6 · x1 + 2 · x2 + 0
    [mark#(x1)]	=	0 · x1 + 0
    [s(x1)]	=	0 · x1 + -∞
    [mark(x1)]	=	0 · x1 + -∞

    together with the usable rules

    a__app(nil,YS)	→	mark(YS)	(1)
    a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
    a__from(X)	→	cons(mark(X),from(s(X)))	(3)
    a__zWadr(nil,YS)	→	nil	(4)
    a__zWadr(XS,nil)	→	nil	(5)
    a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
    a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
    mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
    mark(from(X))	→	a__from(mark(X))	(9)
    mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
    mark(prefix(X))	→	a__prefix(mark(X))	(11)
    mark(nil)	→	nil	(12)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
    mark(s(X))	→	s(mark(X))	(14)
    a__app(X1,X2)	→	app(X1,X2)	(15)
    a__from(X)	→	from(X)	(16)
    a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
    a__prefix(X)	→	prefix(X)	(18)

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

    mark#(app(X1,X2))

    →

    a__app#(mark(X1),mark(X2))

    (27)

    could be deleted.

    1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      a__from#(X)	→	mark#(X)	(21)
      mark#(app(X1,X2))	→	mark#(X2)	(25)
      mark#(from(X))	→	mark#(X)	(28)
      mark#(from(X))	→	a__from#(mark(X))	(29)
      mark#(cons(X1,X2))	→	mark#(X1)	(35)

      1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the linear polynomial interpretation over the arctic semiring over the integers

      [app(x1, x2)]	=	0 · x1 + 0 · x2 + -∞
      [a__zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [a__app(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [cons(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [a__from(x1)]	=	4 · x1 + 6
      [a__prefix(x1)]	=	0 · x1 + 0
      [nil]	=	0
      [from(x1)]	=	4 · x1 + 6
      [a__from#(x1)]	=	4 · x1 + 6
      [prefix(x1)]	=	0 · x1 + -∞
      [zWadr(x1, x2)]	=	0 · x1 + 0 · x2 + 0
      [mark#(x1)]	=	0 · x1 + 0
      [s(x1)]	=	0 · x1 + 0
      [mark(x1)]	=	0 · x1 + 0

      together with the usable rules

      a__app(nil,YS)	→	mark(YS)	(1)
      a__app(cons(X,XS),YS)	→	cons(mark(X),app(XS,YS))	(2)
      a__from(X)	→	cons(mark(X),from(s(X)))	(3)
      a__zWadr(nil,YS)	→	nil	(4)
      a__zWadr(XS,nil)	→	nil	(5)
      a__zWadr(cons(X,XS),cons(Y,YS))	→	cons(a__app(mark(Y),cons(mark(X),nil)),zWadr(XS,YS))	(6)
      a__prefix(L)	→	cons(nil,zWadr(L,prefix(L)))	(7)
      mark(app(X1,X2))	→	a__app(mark(X1),mark(X2))	(8)
      mark(from(X))	→	a__from(mark(X))	(9)
      mark(zWadr(X1,X2))	→	a__zWadr(mark(X1),mark(X2))	(10)
      mark(prefix(X))	→	a__prefix(mark(X))	(11)
      mark(nil)	→	nil	(12)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(13)
      mark(s(X))	→	s(mark(X))	(14)
      a__app(X1,X2)	→	app(X1,X2)	(15)
      a__from(X)	→	from(X)	(16)
      a__zWadr(X1,X2)	→	zWadr(X1,X2)	(17)
      a__prefix(X)	→	prefix(X)	(18)

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

      a__from#(X)	→	mark#(X)	(21)
      mark#(from(X))	→	mark#(X)	(28)

      could be deleted.

      1.1.1.1.1.1.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#(app(X1,X2))	→	mark#(X2)	(25)
        mark#(cons(X1,X2))	→	mark#(X1)	(35)

        1.1.1.1.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#(app(X1,X2))	→	mark#(X2)	(25)
        1	>	1
        mark#(cons(X1,X2))	→	mark#(X1)	(35)
        1	>	1

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