Termination w.r.t. Q proof of /tmp/tmp48U9NR/13.trs

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

  ↳5 QDP

    ↳6 QDPOrderProof (⇔)

    ↳7 QDP

    ↳8 DependencyGraphProof (⇔)

    ↳9 AND

      ↳10 QDP

      ↳11 QDP

        ↳12 QDPOrderProof (⇔)

        ↳13 QDP

        ↳14 QDPOrderProof (⇔)

        ↳15 QDP

        ↳16 PisEmptyProof (⇔)

        ↳17 TRUE

  ↳18 QDP

    ↳19 QDPOrderProof (⇔)

    ↳20 QDP

    ↳21 QDPOrderProof (⇔)

    ↳22 QDP

  ↳23 QDP

    ↳24 QDPOrderProof (⇔)

    ↳25 QDP

    ↳26 QDPOrderProof (⇔)

    ↳27 QDP

    ↳28 PisEmptyProof (⇔)

    ↳29 TRUE

(0) Obligation:

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

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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:

+¹(O(x), O(y)) → O¹(+(x, y))
+¹(O(x), O(y)) → +¹(x, y)
+¹(O(x), I(y)) → +¹(x, y)
+¹(I(x), O(y)) → +¹(x, y)
+¹(I(x), I(y)) → O¹(+(+(x, y), I(0)))
+¹(I(x), I(y)) → +¹(+(x, y), I(0))
+¹(I(x), I(y)) → +¹(x, y)
*¹(O(x), y) → O¹(*(x, y))
*¹(O(x), y) → *¹(x, y)
*¹(I(x), y) → +¹(O(*(x, y)), y)
*¹(I(x), y) → O¹(*(x, y))
*¹(I(x), y) → *¹(x, y)
-¹(O(x), O(y)) → O¹(-(x, y))
-¹(O(x), O(y)) → -¹(x, y)
-¹(O(x), I(y)) → -¹(-(x, y), I(1))
-¹(O(x), I(y)) → -¹(x, y)
-¹(I(x), O(y)) → -¹(x, y)
-¹(I(x), I(y)) → O¹(-(x, y))
-¹(I(x), I(y)) → -¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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 3 SCCs with 7 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

-¹(O(x), I(y)) → -¹(-(x, y), I(1))
-¹(O(x), I(y)) → -¹(x, y)
-¹(O(x), O(y)) → -¹(x, y)
-¹(I(x), O(y)) → -¹(x, y)
-¹(I(x), I(y)) → -¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(O(x), I(y)) → -¹(x, y)
-¹(I(x), I(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
-¹(x1, x2) = -¹(x2)
O(x1) = x1
I(x1) = I(x1)
-(x1, x2) = -(x1, x2)
1 = 1
0 = 0

Recursive path order with status [RPO].
Precedence:

-^1₁ > 1
I₁ > 1
-₂ > 0 > 1

Status:

-₂: multiset
-^1₁: [1]
1: multiset
0: multiset
I₁: [1]

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

-¹(O(x), I(y)) → -¹(-(x, y), I(1))
-¹(O(x), O(y)) → -¹(x, y)
-¹(I(x), O(y)) → -¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(8) DependencyGraphProof (EQUIVALENT transformation)

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

(9) Complex Obligation (AND)

(10) Obligation:

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

-¹(O(x), I(y)) → -¹(-(x, y), I(1))

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(11) Obligation:

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

-¹(I(x), O(y)) → -¹(x, y)
-¹(O(x), O(y)) → -¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(I(x), O(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
-¹(x1, x2) = -¹(x1)
I(x1) = I(x1)
O(x1) = x1

Recursive path order with status [RPO].
Precedence:

I₁ > -^1₁

Status:

-^1₁: [1]
I₁: multiset

The following usable rules [FROCOS05] were oriented: none

(13) Obligation:

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

-¹(O(x), O(y)) → -¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

-¹(O(x), O(y)) → -¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
-¹(x1, x2) = x1
O(x1) = O(x1)

Recursive path order with status [RPO].
Precedence:

trivial

Status:

O₁: multiset

The following usable rules [FROCOS05] were oriented: none

(15) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(16) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(17) TRUE

(18) Obligation:

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

+¹(O(x), I(y)) → +¹(x, y)
+¹(O(x), O(y)) → +¹(x, y)
+¹(I(x), O(y)) → +¹(x, y)
+¹(I(x), I(y)) → +¹(+(x, y), I(0))
+¹(I(x), I(y)) → +¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(O(x), O(y)) → +¹(x, y)
+¹(I(x), O(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
+¹(x1, x2) = +¹(x2)
O(x1) = O(x1)
I(x1) = x1
+(x1, x2) = +(x1)
0 = 0

Recursive path order with status [RPO].
Precedence:

O₁ > +^1₁ > 0
O₁ > +₁ > 0

Status:

0: multiset
+₁: multiset
O₁: [1]
+^1₁: multiset

The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

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

+¹(O(x), I(y)) → +¹(x, y)
+¹(I(x), I(y)) → +¹(+(x, y), I(0))
+¹(I(x), I(y)) → +¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

+¹(O(x), I(y)) → +¹(x, y)
+¹(I(x), I(y)) → +¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
+¹(x1, x2) = +¹(x2)
O(x1) = O
I(x1) = I(x1)
+(x1, x2) = +
0 = 0

Recursive path order with status [RPO].
Precedence:

O > +^1₁ > I₁ > 0
+ > I₁ > 0

Status:

+: multiset
0: multiset
O: multiset
I₁: [1]
+^1₁: [1]

The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

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

+¹(I(x), I(y)) → +¹(+(x, y), I(0))

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(23) Obligation:

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

*¹(I(x), y) → *¹(x, y)
*¹(O(x), y) → *¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(I(x), y) → *¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
*¹(x1, x2) = *¹(x1, x2)
I(x1) = I(x1)
O(x1) = x1

Recursive path order with status [RPO].
Precedence:

I₁ > *^1₂

Status:

*^1₂: [1,2]
I₁: multiset

The following usable rules [FROCOS05] were oriented: none

(25) Obligation:

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

*¹(O(x), y) → *¹(x, y)

The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

*¹(O(x), y) → *¹(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Recursive path order with status [RPO].
Precedence:

O₁ > *^1₂

Status:

*^1₂: [2,1]
O₁: multiset

The following usable rules [FROCOS05] were oriented: none

(27) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

O(0) → 0
+(0, x) → x
+(x, 0) → x
+(O(x), O(y)) → O(+(x, y))
+(O(x), I(y)) → I(+(x, y))
+(I(x), O(y)) → I(+(x, y))
+(I(x), I(y)) → O(+(+(x, y), I(0)))
*(0, x) → 0
*(x, 0) → 0
*(O(x), y) → O(*(x, y))
*(I(x), y) → +(O(*(x, y)), y)
-(x, 0) → x
-(0, x) → 0
-(O(x), O(y)) → O(-(x, y))
-(O(x), I(y)) → I(-(-(x, y), I(1)))
-(I(x), O(y)) → I(-(x, y))
-(I(x), I(y)) → O(-(x, y))

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

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) DependencyGraphProof (EQUIVALENT transformation)

(9) Complex Obligation (AND)

(10) Obligation:

(11) Obligation:

(12) QDPOrderProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) PisEmptyProof (EQUIVALENT transformation)

(17) TRUE

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPOrderProof (EQUIVALENT transformation)

(22) Obligation:

(23) Obligation:

(24) QDPOrderProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) PisEmptyProof (EQUIVALENT transformation)

(29) TRUE