YES Confluence Proof

Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

+(0,y) → y
+(s(x),y) → s(+(x,y))
inc(x) → s(x)
+(x,y) → +(y,x)
inc(+(x,y)) → +(inc(x),y)

Proof

1 Redundant Rules Transformation

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

inc(+(x,y)) → +(inc(x),y)
+(x,y) → +(y,x)
inc(x) → s(x)
+(s(x),y) → s(+(x,y))
+(0,y) → y
inc(s(+(x75,y))) → s(s(+(x75,y)))
+(y,0) → y
+(y,s(x)) → s(+(x,y))
inc(+(y,x)) → s(+(x,y))
inc(+(y,x)) → +(inc(x),y)
+(inc(x66),x67) → s(+(x66,x67))
+(inc(0),y) → s(y)
+(y,s(x77)) → s(+(x77,y))
+(inc(s(x75)),y) → s(s(+(x75,y)))
+(inc(x),y) → s(+(x,y))

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

1.1 Redundant Rules Transformation

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

+(inc(x),y) → s(+(x,y))
+(inc(s(x75)),y) → s(s(+(x75,y)))
+(y,s(x77)) → s(+(x77,y))
+(inc(0),y) → s(y)
inc(+(y,x)) → +(inc(x),y)
inc(+(y,x)) → s(+(x,y))
+(y,0) → y
+(0,y) → y
+(s(x),y) → s(+(x,y))
inc(x) → s(x)
+(x,y) → +(y,x)
inc(+(x,y)) → +(inc(x),y)

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

1.1.1 Redundant Rules Transformation

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

+(inc(x),y) → s(+(x,y))
+(inc(s(x75)),y) → s(s(+(x75,y)))
+(y,s(x77)) → s(+(x77,y))
+(inc(0),y) → s(y)
inc(+(y,x)) → +(inc(x),y)
inc(+(y,x)) → s(+(x,y))
+(y,0) → y
+(0,y) → y
+(s(x),y) → s(+(x,y))
inc(x) → s(x)
+(x,y) → +(y,x)
inc(+(x,y)) → +(inc(x),y)
+(inc(y),x) → s(+(x,y))
+(inc(y),x) → s(+(y,x))
+(+(inc(x685),x686),y) → s(+(+(x685,x686),y))
+(y,inc(0)) → s(y)
+(y,inc(s(x75))) → s(s(+(x75,y)))
+(y,inc(x)) → s(+(x,y))
+(s(0),y) → s(y)
+(s(s(x75)),y) → s(s(+(x75,y)))
s(+(x647,s(x77))) → s(s(+(x647,x77)))
s(+(x647,s(x77))) → s(s(+(x77,x647)))
+(+(inc(x617),x616),y) → s(+(+(x617,x616),y))
s(+(x604,s(x))) → s(s(+(x604,x)))
s(+(x604,s(x))) → s(s(+(x,x604)))
s(+(x596,inc(0))) → s(s(x596))
s(+(x594,inc(s(x75)))) → s(s(s(+(x75,x594))))
s(+(x592,inc(x))) → s(s(+(x,x592)))
inc(s(s(+(x581,x)))) → s(s(s(+(x581,x))))
s(s(+(x579,s(x77)))) → s(s(s(+(x579,x77))))
inc(s(+(x567,x))) → s(s(+(x567,x)))
s(+(x563,s(x77))) → s(s(+(x563,x77)))
+(inc(x),y) → s(+(y,x))
+(inc(x),s(x649)) → s(s(+(x649,x)))
s(+(x77,s(x647))) → s(s(+(x647,x77)))
s(+(x77,s(x647))) → s(s(+(x77,x647)))
+(inc(inc(0)),y) → s(s(y))
s(+(x,inc(0))) → s(s(x))
+(inc(x),inc(0)) → s(s(x))
s(+(x77,inc(0))) → s(s(x77))
+(inc(x),s(x608)) → s(s(+(x608,x)))
s(+(x,s(x604))) → s(s(+(x604,x)))
s(+(x,s(x604))) → s(s(+(x,x604)))
s(s(+(x75,s(x594)))) → s(s(s(+(x75,x594))))
s(+(x,s(x592))) → s(s(+(x,x592)))
+(inc(inc(s(x589))),y) → s(s(s(+(x589,y))))
+(y,inc(s(x587))) → s(s(+(x587,y)))
s(+(x,inc(s(x583)))) → s(s(s(+(x583,x))))
+(inc(x),inc(s(x581))) → s(s(s(+(x581,x))))
s(+(x77,inc(s(x579)))) → s(s(s(+(x579,x77))))
+(inc(inc(x575)),y) → s(s(+(x575,y)))
+(y,inc(x573)) → s(+(x573,y))
s(+(x,inc(x569))) → s(s(+(x569,x)))
+(inc(x),inc(x567)) → s(s(+(x567,x)))
s(+(x77,inc(x563))) → s(s(+(x563,x77)))

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

1.1.1.1 Decreasing Diagrams

1.1.1.1.1 Relative Termination Proof

The duplicating rules (R) terminate relative to the other rules (S).

1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S is relative terminating.

1.1.1.1.2 Rule Labeling

Confluence is proven, because all critical peaks can be joined decreasingly using the following rule labeling function (rules that are not shown have label 0). All critical pairs are joinable:

Tool configuration

csi