Certification Problem

Input (TPDB TRS_Standard/AG01/#3.13)

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

• The 1^st component contains the pair

  if_reach_2#(false,x,y,edge(u,v,i),h)	→	reach#(v,y,union(i,h),empty)	(22)
  reach#(x,y,edge(u,v,i),h)	→	if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)	(18)
  if_reach_1#(true,x,y,edge(u,v,i),h)	→	if_reach_2#(eq(y,v),x,y,edge(u,v,i),h)	(20)
  if_reach_2#(false,x,y,edge(u,v,i),h)	→	reach#(x,y,i,h)	(23)
  if_reach_1#(false,x,y,edge(u,v,i),h)	→	reach#(x,y,i,edge(u,v,h))	(25)

  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

  [false]	=	0 0 0 1 0 0 1 0 0
  [reach#(x1,...,x4)]	=	0 0 0 0 0 0 0 0 0 · x1 + 0 0 0 0 0 0 0 0 0 · x2 + 1 1 0 0 0 0 0 0 0 · x3 + 1 1 0 0 0 0 0 0 0 · x4 + 0 0 0 0 0 0 0 0 0
  [edge(x1, x2, x3)]	=	0 0 1 0 0 1 0 0 0 · x1 + 1 0 1 0 0 1 0 0 0 · x2 + 1 0 0 0 1 0 1 1 0 · x3 + 0 0 0 0 0 0 0 0 0
  [eq(x1, x2)]	=	1 0 0 0 0 0 0 0 0 · x1 + 0 0 0 0 0 1 0 0 1 · x2 + 0 0 0 0 0 0 0 0 0
  [s(x1)]	=	1 0 0 0 0 0 1 0 1 · x1 + 0 0 0 0 0 0 1 0 0
  [if_reach_1#(x1,...,x5)]	=	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 · x3 + 1 1 0 0 0 0 0 0 0 · x4 + 1 1 0 0 0 0 0 0 0 · x5 + 0 0 0 0 0 0 0 0 0
  [if_reach_2#(x1,...,x5)]	=	0 1 1 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 · x3 + 0 0 1 0 0 0 0 0 0 · x4 + 1 1 0 0 0 0 0 0 0 · x5 + 0 0 0 0 0 0 0 0 0
  [0]	=	1 0 0 0 0 0 1 0 0
  [union(x1, x2)]	=	1 0 0 0 1 0 0 1 1 · x1 + 1 0 0 0 1 0 1 1 1 · x2 + 0 0 0 0 0 0 0 0 0
  [empty]	=	0 0 0 0 0 0 1 0 0
  [true]	=	0 0 0 0 0 0 0 0 0

  together with the usable rules

  union(empty,h)	→	h	(7)
  union(edge(x,y,i),h)	→	edge(x,y,union(i,h))	(8)
  eq(0,0)	→	true	(1)
  eq(0,s(x))	→	false	(2)
  eq(s(x),0)	→	false	(3)
  eq(s(x),s(y))	→	eq(x,y)	(4)

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

  if_reach_2#(false,x,y,edge(u,v,i),h)	→	reach#(v,y,union(i,h),empty)	(22)
  if_reach_2#(false,x,y,edge(u,v,i),h)	→	reach#(x,y,i,h)	(23)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    if_reach_1#(false,x,y,edge(u,v,i),h)	→	reach#(x,y,i,edge(u,v,h))	(25)
    reach#(x,y,edge(u,v,i),h)	→	if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)	(18)

    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.

    if_reach_1#(false,x,y,edge(u,v,i),h)	→	reach#(x,y,i,edge(u,v,h))	(25)
    4	>	3
    3	≥	2
    2	≥	1
    reach#(x,y,edge(u,v,i),h)	→	if_reach_1#(eq(x,u),x,y,edge(u,v,i),h)	(18)
    4	≥	5
    3	≥	4
    2	≥	3
    1	≥	2

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

• The 2^nd component contains the pair

  union#(edge(x,y,i),h)

  →

  union#(i,h)

  (16)

  1.1.2 Size-Change Termination

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

  union#(edge(x,y,i),h)	→	union#(i,h)	(16)
  2	≥	2
  1	>	1

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

• The 3^rd component contains the pair

  eq#(s(x),s(y))

  →

  eq#(x,y)

  (15)

  1.1.3 Size-Change Termination

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

  eq#(s(x),s(y))	→	eq#(x,y)	(15)
  2	>	2
  1	>	1

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