Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex49_GM04_iGM)

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

• The 1^st component contains the pair

  mark#(if(X1,X2,X3))	→	mark#(X1)	(65)
  mark#(if(X1,X2,X3))	→	active#(if(mark(X1),X2,X3))	(67)
  active#(if(false,X,Y))	→	mark#(Y)	(53)
  mark#(div(X1,X2))	→	active#(div(mark(X1),X2))	(64)
  active#(div(s(X),s(Y)))	→	mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(51)
  mark#(div(X1,X2))	→	mark#(X1)	(62)
  mark#(s(X))	→	mark#(X)	(56)
  active#(if(true,X,Y))	→	mark#(X)	(52)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the

  prec(mark#)	=	0		stat(mark#)	=	lex
  prec(active#)	=	0		stat(active#)	=	lex
  prec(if)	=	0		stat(if)	=	lex
  prec(div)	=	3		stat(div)	=	lex
  prec(false)	=	0		stat(false)	=	lex
  prec(true)	=	0		stat(true)	=	lex
  prec(geq)	=	2		stat(geq)	=	lex
  prec(s)	=	0		stat(s)	=	lex
  prec(mark)	=	0		stat(mark)	=	lex
  prec(active)	=	0		stat(active)	=	lex
  prec(minus)	=	0		stat(minus)	=	lex
  prec(0)	=	0		stat(0)	=	lex

  π(mark#)	=	1
  π(active#)	=	1
  π(if)	=	[1,2,3]
  π(div)	=	[1]
  π(false)	=	[]
  π(true)	=	[]
  π(geq)	=	[]
  π(s)	=	[1]
  π(mark)	=	1
  π(active)	=	1
  π(minus)	=	1
  π(0)	=	[]

  together with the usable rules

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

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

  mark#(if(X1,X2,X3))	→	mark#(X1)	(65)
  active#(if(false,X,Y))	→	mark#(Y)	(53)
  active#(div(s(X),s(Y)))	→	mark#(if(geq(X,Y),s(div(minus(X,Y),s(Y))),0))	(51)
  mark#(div(X1,X2))	→	mark#(X1)	(62)
  mark#(s(X))	→	mark#(X)	(56)
  active#(if(true,X,Y))	→	mark#(X)	(52)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  mark#(minus(X1,X2))	→	active#(minus(X1,X2))	(54)
  active#(minus(s(X),s(Y)))	→	mark#(minus(X,Y))	(40)

  1.1.2 Subterm Criterion Processor

  We use the projection to multisets

  π(mark#)	=	{ 1 }
  π(active#)	=	{ 1 }
  π(minus)	=	{ 2 }

  to remove the pairs:

  active#(minus(s(X),s(Y)))

  →

  mark#(minus(X,Y))

  (40)

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 3^rd component contains the pair

  mark#(geq(X1,X2))	→	active#(geq(X1,X2))	(59)
  active#(geq(s(X),s(Y)))	→	mark#(geq(X,Y))	(44)

  1.1.3 Subterm Criterion Processor

  We use the projection to multisets

  π(mark#)	=	{ 1 }
  π(active#)	=	{ 1 }
  π(geq)	=	{ 2 }

  to remove the pairs:

  active#(geq(s(X),s(Y)))

  →

  mark#(geq(X,Y))

  (44)

  1.1.3.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 4^th component contains the pair

  minus#(mark(X1),X2)	→	minus#(X1,X2)	(68)
  minus#(X1,active(X2))	→	minus#(X1,X2)	(71)
  minus#(active(X1),X2)	→	minus#(X1,X2)	(70)
  minus#(X1,mark(X2))	→	minus#(X1,X2)	(69)

  1.1.4 Size-Change Termination

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

  minus#(mark(X1),X2)	→	minus#(X1,X2)	(68)
  2	≥	2
  1	>	1
  minus#(X1,active(X2))	→	minus#(X1,X2)	(71)
  2	>	2
  1	≥	1
  minus#(active(X1),X2)	→	minus#(X1,X2)	(70)
  2	≥	2
  1	>	1
  minus#(X1,mark(X2))	→	minus#(X1,X2)	(69)
  2	>	2
  1	≥	1

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

• The 5^th component contains the pair

  geq#(mark(X1),X2)	→	geq#(X1,X2)	(74)
  geq#(X1,active(X2))	→	geq#(X1,X2)	(77)
  geq#(active(X1),X2)	→	geq#(X1,X2)	(76)
  geq#(X1,mark(X2))	→	geq#(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.

  geq#(mark(X1),X2)	→	geq#(X1,X2)	(74)
  2	≥	2
  1	>	1
  geq#(X1,active(X2))	→	geq#(X1,X2)	(77)
  2	>	2
  1	≥	1
  geq#(active(X1),X2)	→	geq#(X1,X2)	(76)
  2	≥	2
  1	>	1
  geq#(X1,mark(X2))	→	geq#(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

  div#(mark(X1),X2)	→	div#(X1,X2)	(78)
  div#(X1,active(X2))	→	div#(X1,X2)	(81)
  div#(active(X1),X2)	→	div#(X1,X2)	(80)
  div#(X1,mark(X2))	→	div#(X1,X2)	(79)

  1.1.6 Subterm Criterion Processor

  We use the projection

  π(div#)

  =

  1

  and remove the pairs:

  div#(mark(X1),X2)	→	div#(X1,X2)	(78)
  div#(active(X1),X2)	→	div#(X1,X2)	(80)

  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.

  div#(X1,active(X2))	→	div#(X1,X2)	(81)
  2	>	2
  1	≥	1
  div#(X1,mark(X2))	→	div#(X1,X2)	(79)
  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#(mark(X))	→	s#(X)	(72)
  s#(active(X))	→	s#(X)	(73)

  1.1.7 Subterm Criterion Processor

  We use the projection

  π(s#)

  =

  1

  and remove the pairs:

  s#(mark(X))	→	s#(X)	(72)
  s#(active(X))	→	s#(X)	(73)

  1.1.7.1 P is empty

  There are no pairs anymore.

• The 8^th component contains the pair

  if#(mark(X1),X2,X3)	→	if#(X1,X2,X3)	(82)
  if#(X1,X2,active(X3))	→	if#(X1,X2,X3)	(87)
  if#(X1,active(X2),X3)	→	if#(X1,X2,X3)	(86)
  if#(active(X1),X2,X3)	→	if#(X1,X2,X3)	(85)
  if#(X1,X2,mark(X3))	→	if#(X1,X2,X3)	(84)
  if#(X1,mark(X2),X3)	→	if#(X1,X2,X3)	(83)

  1.1.8 Subterm Criterion Processor

  We use the projection

  π(if#)

  =

  2

  and remove the pairs:

  if#(X1,active(X2),X3)	→	if#(X1,X2,X3)	(86)
  if#(X1,mark(X2),X3)	→	if#(X1,X2,X3)	(83)

  1.1.8.1 Subterm Criterion Processor

  We use the projection

  π(if#)

  =

  3

  and remove the pairs:

  if#(X1,X2,active(X3))	→	if#(X1,X2,X3)	(87)
  if#(X1,X2,mark(X3))	→	if#(X1,X2,X3)	(84)

  1.1.8.1.1 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)	(82)
  3	≥	3
  2	≥	2
  1	>	1
  if#(active(X1),X2,X3)	→	if#(X1,X2,X3)	(85)
  3	≥	3
  2	≥	2
  1	>	1

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