The rewrite relation of the following equational TRS is considered.
[mult(x1, x2)] |
= |
1 · x2 + 1 · x1 + 2 · x1 · x2
|
[plus(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[union(x1, x2)] |
= |
1 · x2 + 1 · x1 + 2 · x1 · x2
|
[empty] |
= |
2 |
[0(x1)] |
= |
1 · x1
|
[z] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[tt] |
= |
0 |
[U12(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U21(x1, x2, x3)] |
= |
1 + 3 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U22(x1, x2, x3)] |
= |
1 + 2 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U31(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[U32(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[U41(x1, x2, x3)] |
= |
1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[U42(x1, x2, x3)] |
= |
1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[1(x1)] |
= |
1 + 1 · x1
|
[U51(x1, x2, x3)] |
= |
2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[U52(x1, x2, x3)] |
= |
1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
|
[U61(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U62(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[prod(x1)] |
= |
1 · x1
|
[U71(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U72(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[sum(x1)] |
= |
2 · x1
|
[singl(x1)] |
= |
3 · x1 + 3 · x1 · x1
|
the
rules
[mult(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[plus(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[union(x1, x2)] |
= |
1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
|
[0(x1)] |
= |
1 · x1
|
[z] |
= |
0 |
[U11(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[tt] |
= |
0 |
[U12(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U21(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U22(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U31(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U32(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U41(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U42(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[1(x1)] |
= |
1 · x1
|
[U52(x1, x2, x3)] |
= |
1 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U61(x1, x2, x3)] |
= |
2 · x3 + 3 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U62(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[prod(x1)] |
= |
2 · x1
|
[U71(x1, x2, x3)] |
= |
2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U72(x1, x2, x3)] |
= |
2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[sum(x1)] |
= |
1 + 1 · x1
|
[U51(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[singl(x1)] |
= |
3 · x1 + 3 · x1 · x1
|
the
rules
[mult(x1, x2)] |
= |
1 · x2 + 1 · x1 + 1 · x1 · x2
|
[plus(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[union(x1, x2)] |
= |
1 · x2 + 1 · x1 + 1 · x1 · x2
|
[0(x1)] |
= |
2 + 2 · x1
|
[z] |
= |
0 |
[U11(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[tt] |
= |
0 |
[U12(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U21(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U22(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U31(x1, x2, x3)] |
= |
3 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U32(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U41(x1, x2, x3)] |
= |
1 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U42(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[1(x1)] |
= |
2 · x1
|
[U52(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U61(x1, x2, x3)] |
= |
1 + 1 · x3 + 1 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U62(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[prod(x1)] |
= |
1 · x1
|
[U71(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U72(x1, x2, x3)] |
= |
2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[sum(x1)] |
= |
2 · x1
|
[U51(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[singl(x1)] |
= |
3 + 3 · x1 + 3 · x1 · x1
|
the
rules
[mult(x1, x2)] |
= |
2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
|
[plus(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[union(x1, x2)] |
= |
1 · x2 + 1 · x1 + 3 · x1 · x2
|
[U11(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[tt] |
= |
0 |
[U12(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[0(x1)] |
= |
1 · x1
|
[U21(x1, x2, x3)] |
= |
2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U22(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U32(x1, x2, x3)] |
= |
1 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U42(x1, x2, x3)] |
= |
1 + 2 · x3 + 2 · x2 + 2 · x1 + 3 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[1(x1)] |
= |
2 · x1
|
[U52(x1, x2, x3)] |
= |
3 + 2 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[z] |
= |
0 |
[U62(x1, x2, x3)] |
= |
2 + 2 · x3 + 3 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[prod(x1)] |
= |
1 · x1
|
[U71(x1, x2, x3)] |
= |
3 · x3 + 3 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U72(x1, x2, x3)] |
= |
3 · x3 + 3 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[sum(x1)] |
= |
3 · x1
|
[U51(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
the
rules
[mult(x1, x2)] |
= |
1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
|
[plus(x1, x2)] |
= |
1 · x2 + 1 · x1
|
[union(x1, x2)] |
= |
1 · x2 + 1 · x1 + 2 · x1 · x2
|
[U11(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[tt] |
= |
0 |
[U12(x1, x2, x3)] |
= |
2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[0(x1)] |
= |
1 + 1 · x1
|
[U62(x1, x2, x3)] |
= |
1 + 2 · x3 + 2 · x2 + 2 · x1 + 3 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[prod(x1)] |
= |
1 · x1
|
[U71(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[U72(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[sum(x1)] |
= |
1 · x1
|
[1(x1)] |
= |
3 + 2 · x1 + 3 · x1 · x1
|
[U21(x1, x2, x3)] |
= |
2 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
[z] |
= |
1 |
[U51(x1, x2, x3)] |
= |
1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
|
the
rulesThere are no rules in the TRS. Hence, it is AC-terminating.