YES Confluence Proof

Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

+(x,0) → x
+(x,s(y)) → s(+(x,y))
+(x,p(y)) → p(+(x,y))
+(0,y) → y
+(s(x),y) → s(+(x,y))
+(p(x),y) → p(+(x,y))
s(p(x)) → x
p(s(x)) → x
-(0) → 0
-(s(x)) → p(-(x))
-(p(x)) → s(-(x))
+(+(x,y),z) → +(x,+(y,z))
+(x,+(y,z)) → +(+(x,y),z)
-(+(x,y)) → +(-(x),-(y))

Proof

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

+(x,0) → x
+(x,s(y)) → s(+(x,y))
+(x,p(y)) → p(+(x,y))
+(0,y) → y
+(s(x),y) → s(+(x,y))
+(p(x),y) → p(+(x,y))
s(p(x)) → x
p(s(x)) → x
-(0) → 0
-(s(x)) → p(-(x))
-(p(x)) → s(-(x))
+(x,+(y,z)) → +(+(x,y),z)
-(+(x,y)) → +(-(x),-(y))

All redundant rules that were added or removed can be simulated in 4 steps .

1.1 Locally confluent and terminating

Confluence is proven by showing local confluence and termination.

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[-(x1)] = 4 · x1 + 0
[+(x1, x2)] = 1 · x1 + 1 · x2 + 3
[p(x1)] = 1 · x1 + 4
[0] = 0
[s(x1)] = 1 · x1 + 1
the rules
+(x,s(y)) → s(+(x,y))
+(x,p(y)) → p(+(x,y))
+(s(x),y) → s(+(x,y))
+(p(x),y) → p(+(x,y))
-(0) → 0
-(s(x)) → p(-(x))
+(x,+(y,z)) → +(+(x,y),z)
remain.

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[-(x1)] = 1 · x1 + 4
[+(x1, x2)] = 1 · x1 + 3 · x2 + 2
[p(x1)] = 1 · x1 + 0
[0] = 0
[s(x1)] = 1 · x1 + 4
the rules
+(x,p(y)) → p(+(x,y))
+(s(x),y) → s(+(x,y))
+(p(x),y) → p(+(x,y))
remain.

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[+(x1, x2)] = 4 · x1 + 1 · x2 + 1
[p(x1)] = 1 · x1 + 3
[s(x1)] = 1 · x1 + 0
the rules
+(x,p(y)) → p(+(x,y))
+(s(x),y) → s(+(x,y))
remain.

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[+(x1, x2)] = 4 · x1 + 1 · x2 + 7
[p(x1)] = 1 · x1 + 0
[s(x1)] = 1 · x1 + 1
the rule
+(x,p(y)) → p(+(x,y))
remains.

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[+(x1, x2)] = 1 · x1 + 4 · x2 + 0
[p(x1)] = 1 · x1 + 5
all rules could be removed.

1.1.1.1.1.1.1.1 R is empty

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

1.1.2 Local Confluence Proof

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

Tool configuration

csi