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 |
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 | ||
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 .
Confluence is proven using the following terminating critical-pair-closing-system R:
There are no rules.
There are no rules in the TRS. Hence, it is terminating.