Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci01)

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

• The 1^st component contains the pair

  top#(ok(X))	→	top#(active(X))	(84)
  top#(mark(X))	→	top#(proper(X))	(82)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

  [mark(x1)]	=	0 0 0 0 0 0 0 0 1 · x1 + 0 0 0 0 0 0 1 0 0
  [cons(x1, x2)]	=	0 0 0 0 0 0 0 0 0 · x1 + 0 0 0 0 0 0 0 0 0 · x2 + 0 0 0 0 0 0 0 0 0
  [eq(x1, x2)]	=	0 1 0 0 0 0 0 0 0 · x1 + 0 0 0 0 0 0 0 1 0 · x2 + 0 0 0 0 0 0 1 0 0
  [true]	=	0 0 0 1 0 0 0 0 0
  [s(x1)]	=	0 0 0 0 1 0 0 0 0 · x1 + 0 0 0 1 0 0 0 0 0
  [nil]	=	0 0 0 0 0 0 0 0 0
  [0]	=	0 0 0 0 0 0 0 0 0
  [inf(x1)]	=	0 1 0 0 1 0 0 0 1 · x1 + 0 0 0 0 0 0 1 0 0
  [top#(x1)]	=	0 0 1 0 0 0 0 0 0 · x1 + 0 0 0 0 0 0 0 0 0
  [any(x1)]	=	0 0 0 0 0 0 0 0 0 · x1 + 0 0 0 0 0 0 0 0 0
  [proper(x1)]	=	1 0 0 0 1 0 0 0 1 · x1 + 0 0 0 0 0 0 0 0 0
  [length(x1)]	=	0 1 0 0 0 0 0 0 1 · x1 + 0 0 0 0 0 0 1 0 0
  [take(x1, x2)]	=	0 0 0 0 0 0 0 0 1 · x1 + 0 0 0 0 0 0 0 0 1 · x2 + 0 0 0 0 0 0 1 0 0
  [ok(x1)]	=	0 0 0 0 1 0 0 0 1 · x1 + 0 0 0 0 0 0 0 0 0
  [false]	=	0 0 0 0 0 0 0 0 0
  [active(x1)]	=	0 0 0 0 0 0 0 0 1 · x1 + 0 0 0 0 0 0 0 0 0

  together with the usable rules

  active(eq(0,0))	→	mark(true)	(1)
  active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)
  active(eq(X,Y))	→	mark(false)	(3)
  active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
  active(take(0,X))	→	mark(nil)	(5)
  active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
  active(length(nil))	→	mark(0)	(7)
  active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
  active(inf(X))	→	inf(active(X))	(9)
  active(take(X1,X2))	→	take(active(X1),X2)	(10)
  active(take(X1,X2))	→	take(X1,active(X2))	(11)
  active(length(X))	→	length(active(X))	(12)
  eq(ok(X1),ok(X2))	→	ok(eq(X1,X2))	(27)
  s(ok(X))	→	ok(s(X))	(28)
  inf(mark(X))	→	mark(inf(X))	(13)
  inf(ok(X))	→	ok(inf(X))	(29)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(30)
  take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
  take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
  take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
  length(mark(X))	→	mark(length(X))	(16)
  length(ok(X))	→	ok(length(X))	(32)
  proper(eq(X1,X2))	→	eq(proper(X1),proper(X2))	(17)
  proper(0)	→	ok(0)	(18)
  proper(true)	→	ok(true)	(19)
  proper(s(X))	→	s(proper(X))	(20)
  proper(false)	→	ok(false)	(21)
  proper(inf(X))	→	inf(proper(X))	(22)
  proper(cons(any(X1),X2))	→	cons(any(any(proper(X1))),any(proper(X2)))	(23)
  proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(24)
  proper(nil)	→	ok(nil)	(25)
  proper(length(X))	→	length(proper(X))	(26)

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

  top#(mark(X))

  →

  top#(proper(X))

  (82)

  could be deleted.

  1.1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(top#)	=	0		stat(top#)	=	lex
  prec(ok)	=	0		stat(ok)	=	lex
  prec(length)	=	0		stat(length)	=	lex
  prec(nil)	=	2		stat(nil)	=	lex
  prec(take)	=	10		stat(take)	=	lex
  prec(cons)	=	1		stat(cons)	=	lex
  prec(inf)	=	1		stat(inf)	=	lex
  prec(false)	=	0		stat(false)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(true)	=	0		stat(true)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(eq)	=	1		stat(eq)	=	lex
  prec(0)	=	0		stat(0)	=	lex

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

  together with the usable rules

  active(eq(0,0))	→	mark(true)	(1)
  active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)
  active(eq(X,Y))	→	mark(false)	(3)
  active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
  active(take(0,X))	→	mark(nil)	(5)
  active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
  active(length(nil))	→	mark(0)	(7)
  active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
  active(inf(X))	→	inf(active(X))	(9)
  active(take(X1,X2))	→	take(active(X1),X2)	(10)
  active(take(X1,X2))	→	take(X1,active(X2))	(11)
  active(length(X))	→	length(active(X))	(12)
  inf(mark(X))	→	mark(inf(X))	(13)
  inf(ok(X))	→	ok(inf(X))	(29)
  take(mark(X1),X2)	→	mark(take(X1,X2))	(14)
  take(X1,mark(X2))	→	mark(take(X1,X2))	(15)
  take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(31)
  length(mark(X))	→	mark(length(X))	(16)
  length(ok(X))	→	ok(length(X))	(32)

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

  top#(ok(X))

  →

  top#(active(X))

  (84)

  could be deleted.

  1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  proper#(length(X))	→	proper#(X)	(73)
  proper#(take(X1,X2))	→	proper#(X1)	(71)
  proper#(take(X1,X2))	→	proper#(X2)	(70)
  proper#(cons(any(X1),X2))	→	proper#(X1)	(66)
  proper#(cons(any(X1),X2))	→	proper#(X2)	(64)
  proper#(inf(X))	→	proper#(X)	(62)
  proper#(s(X))	→	proper#(X)	(60)
  proper#(eq(X1,X2))	→	proper#(X1)	(58)
  proper#(eq(X1,X2))	→	proper#(X2)	(57)

  1.1.2 Subterm Criterion Processor

  We use the projection

  π(proper#)

  =

  1

  and remove the pairs:

  proper#(length(X))	→	proper#(X)	(73)
  proper#(take(X1,X2))	→	proper#(X1)	(71)
  proper#(take(X1,X2))	→	proper#(X2)	(70)
  proper#(cons(any(X1),X2))	→	proper#(X1)	(66)
  proper#(cons(any(X1),X2))	→	proper#(X2)	(64)
  proper#(inf(X))	→	proper#(X)	(62)
  proper#(s(X))	→	proper#(X)	(60)
  proper#(eq(X1,X2))	→	proper#(X1)	(58)
  proper#(eq(X1,X2))	→	proper#(X2)	(57)

  1.1.2.1 P is empty

  There are no pairs anymore.

• The 3^rd component contains the pair

  any#(proper(X))

  →

  any#(X)

  (86)

  1.1.3 Size-Change Termination

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

  any#(proper(X))	→	any#(X)	(86)
  1	>	1

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

• The 4^th component contains the pair

  active#(length(X))	→	active#(X)	(51)
  active#(take(X1,X2))	→	active#(X2)	(49)
  active#(take(X1,X2))	→	active#(X1)	(47)
  active#(inf(X))	→	active#(X)	(45)

  1.1.4 Size-Change Termination

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

  active#(length(X))	→	active#(X)	(51)
  1	>	1
  active#(take(X1,X2))	→	active#(X2)	(49)
  1	>	1
  active#(take(X1,X2))	→	active#(X1)	(47)
  1	>	1
  active#(inf(X))	→	active#(X)	(45)
  1	>	1

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

• The 5^th component contains the pair

  eq#(ok(X1),ok(X2))

  →

  eq#(X1,X2)

  (75)

  1.1.5 Size-Change Termination

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

  eq#(ok(X1),ok(X2))	→	eq#(X1,X2)	(75)
  2	>	2
  1	>	1

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

• The 6^th component contains the pair

  cons#(ok(X1),ok(X2))

  →

  cons#(X1,X2)

  (78)

  1.1.6 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)	(78)
  2	>	2
  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)

  (76)

  1.1.7 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)	(76)
  1	>	1

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

• The 8^th component contains the pair

  inf#(ok(X))	→	inf#(X)	(77)
  inf#(mark(X))	→	inf#(X)	(53)

  1.1.8 Size-Change Termination

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

  inf#(ok(X))	→	inf#(X)	(77)
  1	>	1
  inf#(mark(X))	→	inf#(X)	(53)
  1	>	1

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

• The 9^th component contains the pair

  take#(ok(X1),ok(X2))	→	take#(X1,X2)	(79)
  take#(X1,mark(X2))	→	take#(X1,X2)	(55)
  take#(mark(X1),X2)	→	take#(X1,X2)	(54)

  1.1.9 Size-Change Termination

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

  take#(ok(X1),ok(X2))	→	take#(X1,X2)	(79)
  2	>	2
  1	>	1
  take#(X1,mark(X2))	→	take#(X1,X2)	(55)
  2	>	2
  1	≥	1
  take#(mark(X1),X2)	→	take#(X1,X2)	(54)
  2	≥	2
  1	>	1

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

• The 10^th component contains the pair

  length#(ok(X))	→	length#(X)	(80)
  length#(mark(X))	→	length#(X)	(56)

  1.1.10 Size-Change Termination

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

  length#(ok(X))	→	length#(X)	(80)
  1	>	1
  length#(mark(X))	→	length#(X)	(56)
  1	>	1

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