Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex15_Luc98_C)

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))	(92)
  top#(mark(X))	→	top#(proper(X))	(90)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(top#)	=	0		stat(top#)	=	lex
  prec(ok)	=	0		stat(ok)	=	lex
  prec(proper)	=	0		stat(proper)	=	lex
  prec(from)	=	3		stat(from)	=	lex
  prec(cons)	=	0		stat(cons)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(first)	=	3		stat(first)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(add)	=	3		stat(add)	=	lex
  prec(0)	=	0		stat(0)	=	lex
  prec(if)	=	2		stat(if)	=	lex
  prec(false)	=	0		stat(false)	=	lex
  prec(mark)	=	1		stat(mark)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(and)	=	3		stat(and)	=	lex
  prec(true)	=	0		stat(true)	=	lex

  π(top#)	=	[1]
  π(ok)	=	1
  π(proper)	=	1
  π(from)	=	[]
  π(cons)	=	[]
  π(nil)	=	[]
  π(first)	=	[1,2]
  π(s)	=	[]
  π(add)	=	[1,2]
  π(0)	=	[]
  π(if)	=	[1,2,3]
  π(false)	=	[]
  π(mark)	=	[1]
  π(active)	=	1
  π(and)	=	[1,2]
  π(true)	=	[]

  together with the usable rules

  active(and(true,X))	→	mark(X)	(1)
  active(and(false,Y))	→	mark(false)	(2)
  active(if(true,X,Y))	→	mark(X)	(3)
  active(if(false,X,Y))	→	mark(Y)	(4)
  active(add(0,X))	→	mark(X)	(5)
  active(add(s(X),Y))	→	mark(s(add(X,Y)))	(6)
  active(first(0,X))	→	mark(nil)	(7)
  active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(8)
  active(from(X))	→	mark(cons(X,from(s(X))))	(9)
  active(and(X1,X2))	→	and(active(X1),X2)	(10)
  active(if(X1,X2,X3))	→	if(active(X1),X2,X3)	(11)
  active(add(X1,X2))	→	add(active(X1),X2)	(12)
  active(first(X1,X2))	→	first(active(X1),X2)	(13)
  active(first(X1,X2))	→	first(X1,active(X2))	(14)
  add(mark(X1),X2)	→	mark(add(X1,X2))	(17)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(33)
  s(ok(X))	→	ok(s(X))	(34)
  first(mark(X1),X2)	→	mark(first(X1,X2))	(18)
  first(X1,mark(X2))	→	mark(first(X1,X2))	(19)
  first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(35)
  cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
  from(ok(X))	→	ok(from(X))	(37)
  and(mark(X1),X2)	→	mark(and(X1,X2))	(15)
  and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(31)
  if(mark(X1),X2,X3)	→	mark(if(X1,X2,X3))	(16)
  if(ok(X1),ok(X2),ok(X3))	→	ok(if(X1,X2,X3))	(32)
  proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(20)
  proper(true)	→	ok(true)	(21)
  proper(false)	→	ok(false)	(22)
  proper(if(X1,X2,X3))	→	if(proper(X1),proper(X2),proper(X3))	(23)
  proper(add(X1,X2))	→	add(proper(X1),proper(X2))	(24)
  proper(0)	→	ok(0)	(25)
  proper(s(X))	→	s(proper(X))	(26)
  proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(27)
  proper(nil)	→	ok(nil)	(28)
  proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(29)
  proper(from(X))	→	from(proper(X))	(30)

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

  top#(mark(X))

  →

  top#(proper(X))

  (90)

  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(from)	=	1		stat(from)	=	lex
  prec(cons)	=	0		stat(cons)	=	lex
  prec(nil)	=	0		stat(nil)	=	lex
  prec(first)	=	9		stat(first)	=	lex
  prec(s)	=	1		stat(s)	=	lex
  prec(add)	=	2		stat(add)	=	lex
  prec(0)	=	1		stat(0)	=	lex
  prec(if)	=	1		stat(if)	=	lex
  prec(false)	=	0		stat(false)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(and)	=	1		stat(and)	=	lex
  prec(true)	=	8		stat(true)	=	lex

  π(top#)	=	1
  π(ok)	=	[1]
  π(from)	=	[]
  π(cons)	=	[]
  π(nil)	=	[]
  π(first)	=	[2]
  π(s)	=	[]
  π(add)	=	[1]
  π(0)	=	[]
  π(if)	=	[2]
  π(false)	=	[]
  π(mark)	=	[]
  π(active)	=	1
  π(and)	=	[1]
  π(true)	=	[]

  together with the usable rules

  active(and(true,X))	→	mark(X)	(1)
  active(and(false,Y))	→	mark(false)	(2)
  active(if(true,X,Y))	→	mark(X)	(3)
  active(if(false,X,Y))	→	mark(Y)	(4)
  active(add(0,X))	→	mark(X)	(5)
  active(add(s(X),Y))	→	mark(s(add(X,Y)))	(6)
  active(first(0,X))	→	mark(nil)	(7)
  active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(8)
  active(from(X))	→	mark(cons(X,from(s(X))))	(9)
  active(and(X1,X2))	→	and(active(X1),X2)	(10)
  active(if(X1,X2,X3))	→	if(active(X1),X2,X3)	(11)
  active(add(X1,X2))	→	add(active(X1),X2)	(12)
  active(first(X1,X2))	→	first(active(X1),X2)	(13)
  active(first(X1,X2))	→	first(X1,active(X2))	(14)
  add(mark(X1),X2)	→	mark(add(X1,X2))	(17)
  add(ok(X1),ok(X2))	→	ok(add(X1,X2))	(33)
  first(mark(X1),X2)	→	mark(first(X1,X2))	(18)
  first(X1,mark(X2))	→	mark(first(X1,X2))	(19)
  first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(35)
  and(mark(X1),X2)	→	mark(and(X1,X2))	(15)
  and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(31)
  if(mark(X1),X2,X3)	→	mark(if(X1,X2,X3))	(16)
  if(ok(X1),ok(X2),ok(X3))	→	ok(if(X1,X2,X3))	(32)

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

  top#(ok(X))

  →

  top#(active(X))

  (92)

  could be deleted.

  1.1.1.1.1 P is empty

  There are no pairs anymore.

• The 2^nd component contains the pair

  active#(and(X1,X2))	→	active#(X1)	(47)
  active#(if(X1,X2,X3))	→	active#(X1)	(49)
  active#(add(X1,X2))	→	active#(X1)	(51)
  active#(first(X1,X2))	→	active#(X1)	(53)
  active#(first(X1,X2))	→	active#(X2)	(55)

  1.1.2 Size-Change Termination

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

  active#(and(X1,X2))	→	active#(X1)	(47)
  1	>	1
  active#(if(X1,X2,X3))	→	active#(X1)	(49)
  1	>	1
  active#(add(X1,X2))	→	active#(X1)	(51)
  1	>	1
  active#(first(X1,X2))	→	active#(X1)	(53)
  1	>	1
  active#(first(X1,X2))	→	active#(X2)	(55)
  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#(and(X1,X2))	→	proper#(X2)	(62)
  proper#(and(X1,X2))	→	proper#(X1)	(63)
  proper#(if(X1,X2,X3))	→	proper#(X3)	(65)
  proper#(if(X1,X2,X3))	→	proper#(X2)	(66)
  proper#(if(X1,X2,X3))	→	proper#(X1)	(67)
  proper#(add(X1,X2))	→	proper#(X2)	(69)
  proper#(add(X1,X2))	→	proper#(X1)	(70)
  proper#(s(X))	→	proper#(X)	(72)
  proper#(first(X1,X2))	→	proper#(X2)	(74)
  proper#(first(X1,X2))	→	proper#(X1)	(75)
  proper#(cons(X1,X2))	→	proper#(X2)	(77)
  proper#(cons(X1,X2))	→	proper#(X1)	(78)
  proper#(from(X))	→	proper#(X)	(80)

  1.1.3 Subterm Criterion Processor

  We use the projection

  π(proper#)

  =

  1

  and remove the pairs:

  proper#(and(X1,X2))	→	proper#(X2)	(62)
  proper#(and(X1,X2))	→	proper#(X1)	(63)
  proper#(if(X1,X2,X3))	→	proper#(X3)	(65)
  proper#(if(X1,X2,X3))	→	proper#(X2)	(66)
  proper#(if(X1,X2,X3))	→	proper#(X1)	(67)
  proper#(add(X1,X2))	→	proper#(X2)	(69)
  proper#(add(X1,X2))	→	proper#(X1)	(70)
  proper#(s(X))	→	proper#(X)	(72)
  proper#(first(X1,X2))	→	proper#(X2)	(74)
  proper#(first(X1,X2))	→	proper#(X1)	(75)
  proper#(cons(X1,X2))	→	proper#(X2)	(77)
  proper#(cons(X1,X2))	→	proper#(X1)	(78)
  proper#(from(X))	→	proper#(X)	(80)

  1.1.3.1 P is empty

  There are no pairs anymore.

• The 4^th component contains the pair

  from#(ok(X))

  →

  from#(X)

  (88)

  1.1.4 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)	(88)
  1	>	1

  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)

  (87)

  1.1.5 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)	(87)
  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

  first#(mark(X1),X2)	→	first#(X1,X2)	(60)
  first#(X1,mark(X2))	→	first#(X1,X2)	(61)
  first#(ok(X1),ok(X2))	→	first#(X1,X2)	(86)

  1.1.6 Size-Change Termination

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

  first#(mark(X1),X2)	→	first#(X1,X2)	(60)
  2	≥	2
  1	>	1
  first#(X1,mark(X2))	→	first#(X1,X2)	(61)
  2	>	2
  1	≥	1
  first#(ok(X1),ok(X2))	→	first#(X1,X2)	(86)
  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)

  (85)

  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)	(85)
  1	>	1

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

• The 8^th component contains the pair

  add#(mark(X1),X2)	→	add#(X1,X2)	(59)
  add#(ok(X1),ok(X2))	→	add#(X1,X2)	(84)

  1.1.8 Size-Change Termination

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

  add#(mark(X1),X2)	→	add#(X1,X2)	(59)
  2	≥	2
  1	>	1
  add#(ok(X1),ok(X2))	→	add#(X1,X2)	(84)
  2	>	2
  1	>	1

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

• The 9^th component contains the pair

  if#(mark(X1),X2,X3)	→	if#(X1,X2,X3)	(58)
  if#(ok(X1),ok(X2),ok(X3))	→	if#(X1,X2,X3)	(83)

  1.1.9 Size-Change Termination

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

  if#(mark(X1),X2,X3)	→	if#(X1,X2,X3)	(58)
  3	≥	3
  2	≥	2
  1	>	1
  if#(ok(X1),ok(X2),ok(X3))	→	if#(X1,X2,X3)	(83)
  3	>	3
  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

  and#(mark(X1),X2)	→	and#(X1,X2)	(57)
  and#(ok(X1),ok(X2))	→	and#(X1,X2)	(82)

  1.1.10 Size-Change Termination

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

  and#(mark(X1),X2)	→	and#(X1,X2)	(57)
  2	≥	2
  1	>	1
  and#(ok(X1),ok(X2))	→	and#(X1,X2)	(82)
  2	>	2
  1	>	1

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