Certification Problem

Input (COPS 370)

The rewrite relation of the following conditional TRS is considered.

a c
a d
b c
b d
c e
d e
k e
l e
s(c) t(k)
s(c) t(l)
s(e) t(e)
g(x,x) h(x,x)
f(x) pair(x,y) | s(x) ≈ t(y)

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Quasi-reductive SDTRS where all CCPs are joinable

The given strongly deterministic oriented 3-CTRS is quasi-reductive and all CCPs are joinable.

1.1 Quasi-Reductive CTRS

The given CTRS is quasi-reductive

1.1.1 Unraveling

To prove that the CTRS is quasi-reductive, we show termination of the following unraveled system.

For s(c)t(l) we get
For s(c)t(k) we get
For ce we get
For ke we get
For bc we get
For le we get
For ac we get
For bd we get
For f(x)pair(x,y)s(x)t(y) we get
For ad we get
For g(x,x)h(x,x) we get
For s(e)t(e) we get
For de we get

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[k] = 0
[d] = 16
[s(x1)] = 2 · x1 + 6
[t(x1)] = 2 · x1 + 6
[e] = 0
[U1(x1, x2)] = 2 · x1 + 20 · x2 + 1
[c] = 16
[a] = 25
[g(x1, x2)] = 16 · x1 + 24 · x2 + 0
[pair(x1, x2)] = 2 · x1 + 4 · x2 + 13
[f(x1)] = 24 · x1 + 13
[h(x1, x2)] = 26 · x1 + 10 · x2 + 0
[b] = 16
[l] = 0
all of the following rules can be deleted.
s(c) t(l) (1)
s(c) t(k) (2)
c e (3)
a c (7)
a d (11)
d e (14)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[k] = 28
[d] = 0
[s(x1)] = 5 · x1 + 0
[t(x1)] = 4 · x1 + 22
[e] = 25
[U1(x1, x2)] = 5 · x1 + 1 · x2 + 8
[c] = 16
[g(x1, x2)] = 1 · x1 + 4 · x2 + 16
[pair(x1, x2)] = 1 · x1 + 8 · x2 + 0
[f(x1)] = 26 · x1 + 10
[h(x1, x2)] = 2 · x1 + 1 · x2 + 0
[b] = 16
[l] = 28
all of the following rules can be deleted.
k e (4)
l e (6)
b d (8)
f(x) U1(s(x),x) (9)
U1(t(y),x) pair(x,y) (10)
g(x,x) h(x,x) (12)
s(e) t(e) (13)

1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(b) = 1 weight(b) = 1
prec(c) = 0 weight(c) = 1
all of the following rules can be deleted.
b c (5)

1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.

1.2 All CCPs are joinable

A CCP is joinable if it is context-joinable, infeasible, or unfeasible.