Certification Problem

Input (COPS 944)

We consider the TRS containing the following rules:

C(x)	→	c(x)	(1)
c(c(x))	→	x	(2)
b(b(x))	→	B(x)	(3)
B(B(x))	→	b(x)	(4)
c(B(c(b(c(x)))))	→	B(c(b(c(B(c(b(x)))))))	(5)
b(B(x))	→	x	(6)
B(b(x))	→	x	(7)
c(C(x))	→	x	(8)
C(c(x))	→	x	(9)

The underlying signature is as follows:

{C/1, c/1, b/1, B/1}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2020)

1 Locally confluent and terminating

Confluence is proven by showing local confluence and termination.

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[c(x₁)]	=	2 · x₁ + 1
[B(x₁)]	=	1 · x₁ + 0
[C(x₁)]	=	2 · x₁ + 1
[b(x₁)]	=	1 · x₁ + 0

all of the following rules can be deleted.

c(c(x))	→	x	(2)
c(C(x))	→	x	(8)
C(c(x))	→	x	(9)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[B(x₁)]	=	1 · x₁ + 0
[C(x₁)]	=	2 · x₁ + 4
[b(x₁)]	=	1 · x₁ + 0

all of the following rules can be deleted.

C(x)

→

c(x)

(1)

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

b(b(x))	→	B(x)	(3)
B(B(x))	→	b(x)	(4)
c(b(c(B(c(x)))))	→	b(c(B(c(b(c(B(x)))))))	(10)
B(b(x))	→	x	(7)
b(B(x))	→	x	(6)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

b^#(b(x))	→	B^#(x)	(11)
B^#(B(x))	→	b^#(x)	(12)
c^#(b(c(B(c(x)))))	→	B^#(x)	(13)
c^#(b(c(B(c(x)))))	→	c^#(B(x))	(14)
c^#(b(c(B(c(x)))))	→	b^#(c(B(x)))	(15)
c^#(b(c(B(c(x)))))	→	c^#(b(c(B(x))))	(16)
c^#(b(c(B(c(x)))))	→	B^#(c(b(c(B(x)))))	(17)
c^#(b(c(B(c(x)))))	→	c^#(B(c(b(c(B(x))))))	(18)
c^#(b(c(B(c(x)))))	→	b^#(c(B(c(b(c(B(x)))))))	(19)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

c^#(b(c(B(c(x)))))	→	c^#(B(c(b(c(B(x))))))	(18)
c^#(b(c(B(c(x)))))	→	c^#(B(x))	(14)
c^#(b(c(B(c(x)))))	→	c^#(b(c(B(x))))	(16)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(c^#)	=	3	weight(c^#)	=	1
prec(B)	=	2	weight(B)	=	1
prec(b)	=	1	weight(b)	=	1
prec(c)	=	0	weight(c)	=	1

in combination with the following argument filter

π(c^#)	=	1
π(B)	=	1
π(b)	=	1
π(c)	=	[1]

together with the usable rules

b(b(x))	→	B(x)	(3)
B(B(x))	→	b(x)	(4)
c(b(c(B(c(x)))))	→	b(c(B(c(b(c(B(x)))))))	(10)
B(b(x))	→	x	(7)
b(B(x))	→	x	(6)

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

c^#(b(c(B(c(x)))))	→	c^#(B(x))	(14)
c^#(b(c(B(c(x)))))	→	c^#(b(c(B(x))))	(16)

could be deleted.

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

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

[c(x₁)]

2	0
0	0

· x₁ +

0	0
0	0

[B(x₁)]

0	1
2	2

· x₁ +

0	0
1	0

[c^#(x₁)]

1	0
0	0

· x₁ +

0	0
0	0

[b(x₁)]

0	1
1	2

· x₁ +

1	0
0	0

together with the usable rules

b(b(x))	→	B(x)	(3)
B(B(x))	→	b(x)	(4)
c(b(c(B(c(x)))))	→	b(c(B(c(b(c(B(x)))))))	(10)
B(b(x))	→	x	(7)
b(B(x))	→	x	(6)

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

c^#(b(c(B(c(x)))))

→

c^#(B(c(b(c(B(x))))))

(18)

could be deleted.

1.1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

B^#(B(x)) → b^#(x) (12)

b^#(b(x)) → B^#(x) (11)

1.1.1.1.1.1.2 Subterm Criterion Processor
We use the projection

π(B^#) = 1

π(b^#) = 1

and remove the pairs:

B^#(B(x)) → b^#(x) (12)

b^#(b(x)) → B^#(x) (11)

1.1.1.1.1.1.2.1 P is empty

There are no pairs anymore.

1.2 Local Confluence Proof

All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.

π(B^#)	=	1
π(b^#)	=	1

Certification Problem

Input (COPS 944)

Property / Task

Answer / Result

Proof (by csi @ CoCo 2020)

1 Locally confluent and terminating

1.1 Rule Removal

1.1.1 Rule Removal

1.1.1.1 String Reversal

1.1.1.1.1 Dependency Pair Transformation

1.1.1.1.1.1 Dependency Graph Processor

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

1.1.1.1.1.1.1.1.1 P is empty

1.1.1.1.1.1.2 Subterm Criterion Processor

1.1.1.1.1.1.2.1 P is empty

1.2 Local Confluence Proof