Certification Problem

Input (COPS 332)

The rewrite relation of the following conditional TRS is considered.

even(0) true
even(s(x)) false | odd(x) ≈ false
even(s(x)) true | odd(x) ≈ true
odd(0) false
odd(s(x)) false | even(x) ≈ false
odd(s(x)) true | even(x) ≈ true

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Unraveling

To prove that the CTRS is confluent, we show confluence of the following unraveled system.

For even(0)true we get
For even(s(x))trueodd(x)true we get
For even(s(x))falseodd(x)false we get
For odd(0)false we get
For odd(s(x))falseeven(x)false we get
For odd(s(x))trueeven(x)true we get

1.1 Redundant Rules Transformation

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

U2(true,x) true (8)
U2(false,x) false (7)
odd(s(x)) U2(even(x),x) (6)
odd(0) false (5)
U1(false,x) false (4)
U1(true,x) true (3)
even(s(x)) U1(odd(x),x) (2)
even(0) true (1)

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

1.1.1 Critical Pair Closing System

Confluence is proven using the following terminating critical-pair-closing-system R:

There are no rules.

1.1.1.1 R is empty

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