Termination w.r.t. Q proof of /tmp/aproveUyQFNp.trs

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 DependencyPairsProof (⇔, 90 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 QDPSizeChangeProof (⇔, 0 ms)

        ↳9 YES

    ↳10 QDP

        ↳11 UsableRulesProof (⇔, 0 ms)

        ↳12 QDP

        ↳13 TransformationProof (⇔, 0 ms)

        ↳14 QDP

        ↳15 DependencyGraphProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 TransformationProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 DependencyGraphProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 TransformationProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 DependencyGraphProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 QDPOrderProof (⇔, 14.2 s)

        ↳26 QDP

        ↳27 QDPOrderProof (⇔, 3281 ms)

        ↳28 QDP

        ↳29 QDPOrderProof (⇔, 3185 ms)

        ↳30 QDP

        ↳31 QDPOrderProof (⇔, 31.7 s)

        ↳32 QDP

        ↳33 DependencyGraphProof (⇔, 0 ms)

        ↳34 AND

            ↳35 QDP

                ↳36 QDPOrderProof (⇔, 22.6 s)

                ↳37 QDP

                ↳38 QDPOrderProof (⇔, 3316 ms)

                ↳39 QDP

                ↳40 UsableRulesProof (⇔, 0 ms)

                ↳41 QDP

                ↳42 MNOCProof (⇔, 0 ms)

                ↳43 QDP

                ↳44 DependencyGraphProof (⇔, 0 ms)

                ↳45 TRUE

            ↳46 QDP

                ↳47 UsableRulesProof (⇔, 0 ms)

                ↳48 QDP

                ↳49 QDPSizeChangeProof (⇔, 0 ms)

                ↳50 YES

    ↳51 QDP

        ↳52 UsableRulesReductionPairsProof (⇔, 71 ms)

        ↳53 QDP

        ↳54 QDPOrderProof (⇔, 34 ms)

        ↳55 QDP

        ↳56 QDPOrderProof (⇔, 0 ms)

        ↳57 QDP

        ↳58 QDPSizeChangeProof (⇔, 0 ms)

        ↳59 YES

    ↳60 QDP

        ↳61 UsableRulesProof (⇔, 0 ms)

        ↳62 QDP

        ↳63 QDPSizeChangeProof (⇔, 0 ms)

        ↳64 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(1) → D0(1)
S(d0(x)) → D1(x)
S(d1(x)) → D0(s(x))
S(d1(x)) → S(x)
PLUS(x, 1) → S(x)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → S(plus(x, d0(y)))
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d1(y)) → D0(y)
TIMES(x, d0(y)) → PLUS(d0(times(x, y)), times(x, 0))
TIMES(x, d0(y)) → D0(times(x, y))
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, 0)
TIMES(x, d1(y)) → PLUS(d0(times(x, y)), times(x, 1))
TIMES(x, d1(y)) → D0(times(x, y))
TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d1(y)) → TIMES(x, 1)
P(0) → M(1)
P(d0(x)) → D1(p(x))
P(d0(x)) → P(x)
P(d1(x)) → D0(x)
P(m(x)) → M(s(x))
P(m(x)) → S(x)
S(m(d0(x))) → M(d1(p(x)))
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)
S(m(d1(x))) → M(d0(x))
S(m(d1(x))) → D0(x)
D0(m(x)) → M(d0(x))
D0(m(x)) → D0(x)
D1(m(x)) → M(d1(p(x)))
D1(m(x)) → D1(p(x))
D1(m(x)) → P(x)
PLUS(x, m(y)) → M(plus(m(x), y))
PLUS(x, m(y)) → PLUS(m(x), y)
PLUS(x, m(y)) → M(x)
TIMES(x, m(y)) → M(times(x, y))
TIMES(x, m(y)) → TIMES(x, y)
2¹ → S(1)
3¹ → S(2)
3¹ → 2¹
4¹ → S(3)
4¹ → 3¹
5¹ → S(4)
5¹ → 4¹
6¹ → S(5)
6¹ → 5¹
7¹ → S(6)
7¹ → 6¹
8¹ → S(7)
8¹ → 7¹
9¹ → S(8)
9¹ → 8¹
DD0(x) → PLUS(times(x, s(9)), 0)
DD0(x) → TIMES(x, s(9))
DD0(x) → S(9)
DD0(x) → 9¹
DD1(x) → PLUS(times(x, s(9)), 1)
DD1(x) → TIMES(x, s(9))
DD1(x) → S(9)
DD1(x) → 9¹
DD2(x) → PLUS(times(x, s(9)), 2)
DD2(x) → TIMES(x, s(9))
DD2(x) → S(9)
DD2(x) → 9¹
DD2(x) → 2¹
DD3(x) → PLUS(times(x, s(9)), 3)
DD3(x) → TIMES(x, s(9))
DD3(x) → S(9)
DD3(x) → 9¹
DD3(x) → 3¹
DD4(x) → PLUS(times(x, s(9)), 4)
DD4(x) → TIMES(x, s(9))
DD4(x) → S(9)
DD4(x) → 9¹
DD4(x) → 4¹
DD5(x) → PLUS(times(x, s(9)), 5)
DD5(x) → TIMES(x, s(9))
DD5(x) → S(9)
DD5(x) → 9¹
DD5(x) → 5¹
DD6(x) → PLUS(times(x, s(9)), 6)
DD6(x) → TIMES(x, s(9))
DD6(x) → S(9)
DD6(x) → 9¹
DD6(x) → 6¹
DD7(x) → PLUS(times(x, s(9)), 7)
DD7(x) → TIMES(x, s(9))
DD7(x) → S(9)
DD7(x) → 9¹
DD7(x) → 7¹
DD8(x) → PLUS(times(x, s(9)), 8)
DD8(x) → TIMES(x, s(9))
DD8(x) → S(9)
DD8(x) → 9¹
DD8(x) → 8¹
DD9(x) → PLUS(times(x, s(9)), 9)
DD9(x) → TIMES(x, s(9))
DD9(x) → S(9)
DD9(x) → 9¹

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 84 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D0(m(x)) → D0(x)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D0(m(x)) → D0(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

D0(m(x)) → D0(x)
The graph contains the following edges 1 > 1

(9) YES

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d0(x)) → D1(x)
D1(m(x)) → D1(p(x))
D1(m(x)) → P(x)
P(d0(x)) → D1(p(x))
P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(11) UsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d0(x)) → D1(x)
D1(m(x)) → D1(p(x))
D1(m(x)) → P(x)
P(d0(x)) → D1(p(x))
P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule D1(m(x)) → D1(p(x)) at position [0] we obtained the following new rules [LPAR04]:

D1(m(0)) → D1(m(1)) → D1(m(0)) → D1(m(1))
D1(m(1)) → D1(0) → D1(m(1)) → D1(0)
D1(m(d0(x0))) → D1(d1(p(x0))) → D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0)) → D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0))) → D1(m(m(x0))) → D1(m(s(x0)))

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(x)) → D1(p(x))
P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)
D1(m(0)) → D1(m(1))
D1(m(1)) → D1(0)
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(x)) → P(x)
P(d0(x)) → D1(p(x))
D1(m(0)) → D1(m(1))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d0(x)) → D1(x)
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule P(d0(x)) → D1(p(x)) at position [0] we obtained the following new rules [LPAR04]:

P(d0(0)) → D1(m(1)) → P(d0(0)) → D1(m(1))
P(d0(1)) → D1(0) → P(d0(1)) → D1(0)
P(d0(d0(x0))) → D1(d1(p(x0))) → P(d0(d0(x0))) → D1(d1(p(x0)))
P(d0(d1(x0))) → D1(d0(x0)) → P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0))) → P(d0(m(x0))) → D1(m(s(x0)))

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(x)) → P(x)
D1(m(0)) → D1(m(1))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d0(x)) → D1(x)
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)
P(d0(0)) → D1(m(1))
P(d0(1)) → D1(0)
P(d0(d0(x0))) → D1(d1(p(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(0)) → D1(m(1))
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(0)) → D1(m(1))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → D1(p(x))
S(m(d0(x))) → P(x)

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule S(m(d0(x))) → D1(p(x)) at position [0] we obtained the following new rules [LPAR04]:

S(m(d0(0))) → D1(m(1)) → S(m(d0(0))) → D1(m(1))
S(m(d0(1))) → D1(0) → S(m(d0(1))) → D1(0)
S(m(d0(d0(x0)))) → D1(d1(p(x0))) → S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0)) → S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0))) → S(m(d0(m(x0)))) → D1(m(s(x0)))

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → P(x)
P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(0)) → D1(m(1))
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(0)) → D1(m(1))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(0))) → D1(m(1))
S(m(d0(1))) → D1(0)
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(x)) → P(x)
P(d0(0)) → D1(m(1))
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(0)) → D1(m(1))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(0))) → D1(m(1))
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

D1(m(0)) → D1(m(1))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(P(x₁)) = 0A +
[ -I, -I, 0A ]

· x₁

POL(m(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A -I 0A \

| -I -I 0A |

\ 0A 0A 0A /

· x₁

POL(S(x₁)) = 0A +
[ -I, 0A, -I ]

· x₁

POL(d0(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A -I 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(D1(x₁)) = 0A +
[ 0A, 0A, -I ]

· x₁

POL(0) =
/ 1A \

| 0A |

\ 0A /

POL(1) =
/ 0A \

| 1A |

\ -I /

POL(d1(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(p(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(s(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(x)) → P(x)
P(d0(0)) → D1(m(1))
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(0))) → D1(m(1))
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

S(m(d0(0))) → D1(m(1))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(P(x₁)) = 0A +
[ -I, -I, 0A ]

· x₁

POL(m(x₁)) =
/ -I \

| 1A |

\ -I /

+
/ 0A -I 0A \

| 0A -I 0A |

\ -I 0A -I /

· x₁

POL(S(x₁)) = 0A +
[ -I, 0A, -I ]

· x₁

POL(d0(x₁)) =
/ 0A \

| 1A |

\ 0A /

+
/ -I 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(D1(x₁)) = 0A +
[ 0A, -I, 0A ]

· x₁

POL(0) =
/ 0A \

| -I |

\ -I /

POL(1) =
/ 0A \

| -I |

\ 0A /

POL(d1(x₁)) =
/ 0A \

| 0A |

\ 1A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A -I /

· x₁

POL(p(x₁)) =
/ 1A \

| 1A |

\ 1A /

+
/ 0A -I 0A \

| 0A -I 0A |

\ 0A -I 0A /

· x₁

POL(s(x₁)) =
/ -I \

| 1A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(x)) → P(x)
P(d0(0)) → D1(m(1))
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

P(d0(0)) → D1(m(1))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(P(x₁)) = 0A +
[ 0A, -I, 0A ]

· x₁

POL(m(x₁)) =
/ 1A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A -I /

· x₁

POL(S(x₁)) = 0A +
[ -I, -I, 0A ]

· x₁

POL(d0(x₁)) =
/ -I \

| 1A |

\ 0A /

+
/ 0A -I 0A \

| 0A -I 0A |

\ 0A 0A 0A /

· x₁

POL(D1(x₁)) = 0A +
[ -I, 0A, 0A ]

· x₁

POL(0) =
/ 1A \

| 0A |

\ -I /

POL(1) =
/ 0A \

| 0A |

\ -I /

POL(d1(x₁)) =
/ 0A \

| 0A |

\ 1A /

+
/ 0A 0A 0A \

| 0A -I 0A |

\ 0A 0A 0A /

· x₁

POL(p(x₁)) =
/ 1A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(s(x₁)) =
/ -I \

| 1A |

\ 0A /

+
/ 0A -I 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(m(x)) → S(x)
S(d0(x)) → D1(x)
D1(m(x)) → P(x)
P(d0(x)) → P(x)
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

D1(m(x)) → P(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(P(x₁)) = 0A +
[ 0A, 0A, 0A, -I ]

· x₁

POL(m(x₁)) =
/ -I \

| -I |

| 0A |

\ 0A /

+
/ 0A -I -I -I \

| 0A 0A -I -I |

| 0A -I -I 0A |

\ 0A -I 0A -I /

· x₁

POL(S(x₁)) = 0A +
[ 0A, 0A, -I, 0A ]

· x₁

POL(d0(x₁)) =
/ 0A \

| 0A |

| 0A |

\ 0A /

+
/ -I 0A 0A 0A \

| 0A 0A 0A 0A |

| 0A 1A 1A 0A |

\ 0A 1A 0A 1A /

· x₁

POL(D1(x₁)) = -I +
[ 0A, 1A, 0A, 1A ]

· x₁

POL(d1(x₁)) =
/ 0A \

| 0A |

| 0A |

\ 0A /

+
/ 0A 0A -I 0A \

| 0A 1A 0A 1A |

| 0A 0A -I 0A |

\ 0A 0A -I 0A /

· x₁

POL(p(x₁)) =
/ -I \

| -I |

| 0A |

\ -I /

+
/ 0A 0A 0A -I \

| -I 0A 0A -I |

| 0A 1A 1A 0A |

\ -I 0A 0A -I /

· x₁

POL(s(x₁)) =
/ 0A \

| -I |

| -I |

\ 0A /

+
/ 0A 0A -I 0A \

| -I 0A -I 0A |

| -I 0A -I 0A |

\ 0A 1A 0A 1A /

· x₁

POL(0) =
/ 0A \

| -I |

| 0A |

\ -I /

POL(1) =
/ 0A \

| -I |

| -I |

\ 0A /

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(m(x)) → S(x)
S(d0(x)) → D1(x)
P(d0(x)) → P(x)
P(d0(d0(x0))) → D1(d1(p(x0)))
D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))
P(d0(d1(x0))) → D1(d0(x0))
P(d0(m(x0))) → D1(m(s(x0)))
S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
S(m(d0(d0(x0)))) → D1(d1(p(x0)))
S(m(d0(d1(x0)))) → D1(d0(x0))
S(m(d0(m(x0)))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 7 less nodes.

(34) Complex Obligation (AND)

(35) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))
D1(m(m(x0))) → D1(m(s(x0)))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

D1(m(m(x0))) → D1(m(s(x0)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(D1(x₁)) = -I +
[ 0A, 0A, 0A, -I ]

· x₁

POL(m(x₁)) =
/ 0A \

| 0A |

| 0A |

\ 0A /

+
/ 0A 0A -I 0A \

| 0A 0A 0A 1A |

| 0A 0A -I 0A |

\ 0A 1A -I -I /

· x₁

POL(d0(x₁)) =
/ 0A \

| 0A |

| 1A |

\ 0A /

+
/ 0A 0A 0A 0A \

| -I 1A -I 0A |

| 0A 1A 0A -I |

\ 0A 0A 0A 1A /

· x₁

POL(d1(x₁)) =
/ -I \

| 0A |

| 1A |

\ 0A /

+
/ 0A 0A 0A -I \

| 0A 1A 0A -I |

| 0A 0A 0A 0A |

\ -I 1A -I 0A /

· x₁

POL(p(x₁)) =
/ 0A \

| -I |

| 0A |

\ 0A /

+
/ 0A 0A 0A 0A \

| -I -I -I 0A |

| 0A 0A 0A 0A |

\ 0A 0A 0A 1A /

· x₁

POL(s(x₁)) =
/ -I \

| -I |

| 0A |

\ -I /

+
/ 0A 0A -I -I \

| 0A 1A -I -I |

| 0A 1A -I -I |

\ -I 0A -I -I /

· x₁

POL(0) =
/ 0A \

| -I |

| 0A |

\ 0A /

POL(1) =
/ 0A \

| 0A |

| 0A |

\ -I /

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(d0(x0))) → D1(d1(p(x0)))
D1(m(d1(x0))) → D1(d0(x0))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

D1(m(d0(x0))) → D1(d1(p(x0)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(D1(x₁)) = -I +
[ 0A, -I, 0A ]

· x₁

POL(m(x₁)) =
/ 1A \

| 2A |

\ 1A /

+
/ 0A 0A 1A \

| 1A 0A 0A |

\ 1A 0A 0A /

· x₁

POL(d0(x₁)) =
/ -I \

| 0A |

\ -I /

+
/ 0A -I -I \

| 0A 0A 0A |

\ -I -I 0A /

· x₁

POL(d1(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I 0A \

| 0A 0A -I |

\ -I -I 0A /

· x₁

POL(p(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 1A 0A 0A \

| 1A 0A -I |

\ 0A -I -I /

· x₁

POL(0) =
/ 1A \

| 0A |

\ 0A /

POL(1) =
/ 0A \

| -I |

\ -I /

POL(s(x₁)) =
/ 0A \

| 0A |

\ 1A /

+
/ -I -I 0A \

| 0A 0A 1A |

\ 0A 0A 1A /

· x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))
s(0) → 1
s(1) → d0(1)
s(m(1)) → 0
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(d0(x))) → m(d1(p(x)))

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(d1(x0))) → D1(d0(x0))

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(40) UsableRulesProof (EQUIVALENT transformation)

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(d1(x0))) → D1(d0(x0))

The TRS R consists of the following rules:

d0(0) → 0
d0(m(x)) → m(d0(x))
m(0) → 0
m(m(x)) → x

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D1(m(d1(x0))) → D1(d0(x0))

The TRS R consists of the following rules:

d0(0) → 0
d0(m(x)) → m(d0(x))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d0(m(x0))
m(0)
m(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(44) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(45) TRUE

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
P(d0(x)) → P(x)
P(m(x)) → S(x)

The TRS R consists of the following rules:

p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) UsableRulesProof (EQUIVALENT transformation)

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d1(x)) → S(x)
S(m(d0(x))) → P(x)
P(d0(x)) → P(x)
P(m(x)) → S(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

S(d1(x)) → S(x)
The graph contains the following edges 1 > 1
S(m(d0(x))) → P(x)
The graph contains the following edges 1 > 1
P(m(x)) → S(x)
The graph contains the following edges 1 > 1
P(d0(x)) → P(x)
The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, m(y)) → PLUS(m(x), y)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(52) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0
POL(1) = 0
POL(PLUS(x₁, x₂)) = x₁ + x₂
POL(d0(x₁)) = 2·x₁
POL(d1(x₁)) = 2·x₁
POL(m(x₁)) = x₁
POL(p(x₁)) = x₁
POL(plus(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = x₁

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, m(y)) → PLUS(m(x), y)

The TRS R consists of the following rules:

m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, m(y)) → m(plus(m(x), y))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PLUS(x, m(y)) → PLUS(m(x), y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2) = x2
d0(x1) = x1
d1(x1) = x1
m(x1) = m(x1)
0 = 0

Knuth-Bendix order [KBO] with precedence:

trivial

and weight map:

0=1
m_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

d0(0) → 0
d0(m(x)) → m(d0(x))
m(0) → 0
m(m(x)) → x

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d1(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, m(y)) → m(plus(m(x), y))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PLUS(x, d1(y)) → PLUS(x, d0(y))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2) = x2
d0(x1) = x1
d1(x1) = d1(x1)
0 = 0
m(x1) = x1

Knuth-Bendix order [KBO] with precedence:

trivial

and weight map:

0=1
d1_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

d0(0) → 0
d0(m(x)) → m(d0(x))
m(0) → 0
m(m(x)) → x

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)

The TRS R consists of the following rules:

m(0) → 0
m(m(x)) → x
d0(0) → 0
d0(m(x)) → m(d0(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, m(y)) → m(plus(m(x), y))
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
d1(0) → 1
d1(m(x)) → m(d1(p(x)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(58) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PLUS(x, d0(y)) → PLUS(x, y)
The graph contains the following edges 1 >= 1, 2 > 2
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
The graph contains the following edges 2 > 2

(59) YES

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, m(y)) → TIMES(x, y)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
s(0) → 1
s(1) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, d0(y)) → plus(plus(x, y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
times(x, 0) → 0
times(x, 1) → x
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(d0(x)) → d1(p(x))
p(d1(x)) → d0(x)
p(m(x)) → m(s(x))
s(m(1)) → 0
s(m(d0(x))) → m(d1(p(x)))
s(m(d1(x))) → m(d0(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))
2 → s(1)
3 → s(2)
4 → s(3)
5 → s(4)
6 → s(5)
7 → s(6)
8 → s(7)
9 → s(8)
dd0(x) → plus(times(x, s(9)), 0)
dd1(x) → plus(times(x, s(9)), 1)
dd2(x) → plus(times(x, s(9)), 2)
dd3(x) → plus(times(x, s(9)), 3)
dd4(x) → plus(times(x, s(9)), 4)
dd5(x) → plus(times(x, s(9)), 5)
dd6(x) → plus(times(x, s(9)), 6)
dd7(x) → plus(times(x, s(9)), 7)
dd8(x) → plus(times(x, s(9)), 8)
dd9(x) → plus(times(x, s(9)), 9)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(61) UsableRulesProof (EQUIVALENT transformation)

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, m(y)) → TIMES(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(63) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

TIMES(x, d1(y)) → TIMES(x, y)
The graph contains the following edges 1 >= 1, 2 > 2
TIMES(x, d0(y)) → TIMES(x, y)
The graph contains the following edges 1 >= 1, 2 > 2
TIMES(x, m(y)) → TIMES(x, y)
The graph contains the following edges 1 >= 1, 2 > 2

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) UsableRulesProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPSizeChangeProof (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) UsableRulesProof (EQUIVALENT transformation)

(12) Obligation:

(13) TransformationProof (EQUIVALENT transformation)

(14) Obligation:

(15) DependencyGraphProof (EQUIVALENT transformation)

(16) Obligation:

(17) TransformationProof (EQUIVALENT transformation)

(18) Obligation:

(19) DependencyGraphProof (EQUIVALENT transformation)

(20) Obligation:

(21) TransformationProof (EQUIVALENT transformation)

(22) Obligation:

(23) DependencyGraphProof (EQUIVALENT transformation)

(24) Obligation:

(25) QDPOrderProof (EQUIVALENT transformation)

(26) Obligation:

(27) QDPOrderProof (EQUIVALENT transformation)

(28) Obligation:

(29) QDPOrderProof (EQUIVALENT transformation)

(30) Obligation:

(31) QDPOrderProof (EQUIVALENT transformation)

(32) Obligation:

(33) DependencyGraphProof (EQUIVALENT transformation)

(34) Complex Obligation (AND)

(35) Obligation:

(36) QDPOrderProof (EQUIVALENT transformation)

(37) Obligation:

(38) QDPOrderProof (EQUIVALENT transformation)

(39) Obligation:

(40) UsableRulesProof (EQUIVALENT transformation)

(41) Obligation:

(42) MNOCProof (EQUIVALENT transformation)

(43) Obligation:

(44) DependencyGraphProof (EQUIVALENT transformation)

(45) TRUE

(46) Obligation:

(47) UsableRulesProof (EQUIVALENT transformation)

(48) Obligation:

(49) QDPSizeChangeProof (EQUIVALENT transformation)

(50) YES

(51) Obligation:

(52) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(53) Obligation:

(54) QDPOrderProof (EQUIVALENT transformation)

(55) Obligation:

(56) QDPOrderProof (EQUIVALENT transformation)

(57) Obligation:

(58) QDPSizeChangeProof (EQUIVALENT transformation)

(59) YES

(60) Obligation:

(61) UsableRulesProof (EQUIVALENT transformation)

(62) Obligation:

(63) QDPSizeChangeProof (EQUIVALENT transformation)

(64) YES