The rewrite relation of the following TRS is considered.
| implies(not(x),y) | → | or(x,y) | (1) |
| implies(not(x),or(y,z)) | → | implies(y,or(x,z)) | (2) |
| implies(x,or(y,z)) | → | or(y,implies(x,z)) | (3) |
final states:
{0, 1}
transitions:
| not0(0) | → | 0 |
| or0(0,0) | → | 0 |
| implies0(0,0) | → | 1 |
| or1(0,0) | → | 1 |
| or1(0,0) | → | 2 |
| implies1(0,2) | → | 1 |
| implies1(0,0) | → | 3 |
| or1(0,3) | → | 1 |
| or1(0,2) | → | 1 |
| or1(0,0) | → | 3 |
| implies1(0,2) | → | 3 |
| or1(0,3) | → | 3 |
| implies2(0,0) | → | 4 |
| or2(0,4) | → | 1 |
| or1(0,2) | → | 3 |
| or2(0,4) | → | 3 |
| or1(0,0) | → | 4 |
| implies1(0,2) | → | 4 |
| or1(0,3) | → | 4 |
| or1(0,2) | → | 4 |
| or2(0,4) | → | 4 |