The rewrite relation of the following conditional TRS is considered.
| lte(0,n) | → | true | |
| lte(s(m),0) | → | false | |
| lte(s(m),s(n)) | → | lte(m,n) | |
| insert(nil,m) | → | cons(m,nil) | |
| insert(cons(n,l),m) | → | cons(m,cons(n,l)) | | lte(m,n) ≈ true |
| insert(cons(n,l),m) | → | cons(n,insert(l,m)) | | lte(m,n) ≈ false |
| ordered(nil) | → | true | |
| ordered(cons(m,nil)) | → | true | |
| ordered(cons(m,cons(n,l))) | → | ordered(cons(n,l)) | | lte(m,n) ≈ true |
| ordered(cons(m,cons(n,l))) | → | false | | lte(m,n) ≈ false |
To prove that the CTRS is confluent, we show confluence of the following unraveled system.
| For | ordered(cons(m,cons(n,l)))ordered(cons(n,l))lte(m,n)true we get | ||
| For | lte(s(m),s(n))lte(m,n) we get | ||
| For | ordered(cons(m,nil))true we get | ||
| For | ordered(nil)true we get | ||
| For | ordered(cons(m,cons(n,l)))falselte(m,n)false we get | ||
| For | insert(cons(n,l),m)cons(n,insert(l,m))lte(m,n)false we get | ||
| For | lte(s(m),0)false we get | ||
| For | lte(0,n)true we get | ||
| For | insert(nil,m)cons(m,nil) we get | ||
| For | insert(cons(n,l),m)cons(m,cons(n,l))lte(m,n)true we get | ||
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:
| U1(true,n,l,m) | → | cons(m,cons(n,l)) | (12) |
| insert(nil,m) | → | cons(m,nil) | (11) |
| lte(0,n) | → | true | (10) |
| lte(s(m),0) | → | false | (9) |
| U1(false,n,l,m) | → | cons(n,insert(l,m)) | (8) |
| insert(cons(n,l),m) | → | U1(lte(m,n),n,l,m) | (7) |
| U2(false,m,n,l) | → | false | (6) |
| ordered(nil) | → | true | (5) |
| ordered(cons(m,nil)) | → | true | (4) |
| lte(s(m),s(n)) | → | lte(m,n) | (3) |
| U2(true,m,n,l) | → | ordered(cons(n,l)) | (2) |
| ordered(cons(m,cons(n,l))) | → | U2(lte(m,n),m,n,l) | (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.