Certification Problem

Input (TPDB SRS_Standard/Zantema_06/abc)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

{c(☐), b(☐), a(☐)}

1.1 Semantic Labeling

As carrier we take the set {0,1,2}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 3):

1.1.1 Rule Removal

1.1.1.1 Dependency Pair Transformation

1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

• The 1^st component contains the pair

  c1#(b1(x1))

  →

  c1#(x1)

  (53)

  1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [b1(x1)]	=	x1 + 1
  [c1#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  c1#(b1(x1))

  →

  c1#(x1)

  (53)

  and no rules could be deleted.

  1.1.1.1.1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 2^nd component contains the pair

  c2#(a2(x1))

  →

  c2#(x1)

  (54)

  1.1.1.1.1.1.2 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [a2(x1)]	=	x1 + 1
  [c2#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  c2#(a2(x1))

  →

  c2#(x1)

  (54)

  and no rules could be deleted.

  1.1.1.1.1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 3^rd component contains the pair

  b0#(c0(x1))

  →

  b0#(x1)

  (55)

  1.1.1.1.1.1.3 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [c0(x1)]	=	x1 + 1
  [b0#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  b0#(c0(x1))

  →

  b0#(x1)

  (55)

  and no rules could be deleted.

  1.1.1.1.1.1.3.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 4^th component contains the pair

  b2#(a2(x1))

  →

  b2#(x1)

  (71)

  1.1.1.1.1.1.4 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [a2(x1)]	=	x1 + 1
  [b2#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  b2#(a2(x1))

  →

  b2#(x1)

  (71)

  and no rules could be deleted.

  1.1.1.1.1.1.4.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 5^th component contains the pair

  a0#(c0(x1))

  →

  a0#(x1)

  (72)

  1.1.1.1.1.1.5 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [c0(x1)]	=	x1 + 1
  [a0#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  a0#(c0(x1))

  →

  a0#(x1)

  (72)

  and no rules could be deleted.

  1.1.1.1.1.1.5.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.

• The 6^th component contains the pair

  a1#(b1(x1))

  →

  a1#(x1)

  (74)

  1.1.1.1.1.1.6 Monotonic Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

  [b1(x1)]	=	x1 + 1
  [a1#(x1)]	=	x1 + 0

  having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

  a1#(b1(x1))

  →

  a1#(x1)

  (74)

  and no rules could be deleted.

  1.1.1.1.1.1.6.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.