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

0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
  ↳7 QDP
    ↳8 QDPOrderProof (⇔)
    ↳9 QDP
    ↳10 PisEmptyProof (⇔)
    ↳11 TRUE
  ↳12 QDP
    ↳13 QDPOrderProof (⇔)
    ↳14 QDP
    ↳15 PisEmptyProof (⇔)
    ↳16 TRUE
  ↳17 QDP
    ↳18 QDPOrderProof (⇔)
    ↳19 QDP
    ↳20 PisEmptyProof (⇔)
    ↳21 TRUE
  ↳22 QDP

(0) Obligation:

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

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

TABLE → GEN(s(0))
GEN(x) → IF1(le(x, 10), x)
GEN(x) → LE(x, 10)
GEN(x) → 101
IF1(true, x) → IF2(x, x)
IF2(x, y) → IF3(le(y, 10), x, y)
IF2(x, y) → LE(y, 10)
IF2(x, y) → 101
IF3(true, x, y) → TIMES(x, y)
IF3(true, x, y) → IF2(x, s(y))
IF3(false, x, y) → GEN(s(x))
LE(s(x), s(y)) → LE(x, y)
PLUS(s(x), y) → PLUS(x, y)
TIMES(s(x), y) → PLUS(y, times(x, y))
TIMES(s(x), y) → TIMES(x, y)

The TRS R consists of the following rules:

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUS(s(x), y) → PLUS(x, y)

The TRS R consists of the following rules:

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


PLUS(s(x), y) → PLUS(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x1
s(x1)  =  s(x1)

Lexicographic Path Order [LPO].
Precedence:
trivial

The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

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

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(10) PisEmptyProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

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

TIMES(s(x), y) → TIMES(x, y)

The TRS R consists of the following rules:

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TIMES(s(x), y) → TIMES(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TIMES(x1, x2)  =  x1
s(x1)  =  s(x1)

Lexicographic Path Order [LPO].
Precedence:
trivial

The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

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

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(15) PisEmptyProof (EQUIVALENT transformation)

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

(16) TRUE

(17) Obligation:

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

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


LE(s(x), s(y)) → LE(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
LE(x1, x2)  =  x2
s(x1)  =  s(x1)

Lexicographic Path Order [LPO].
Precedence:
trivial

The following usable rules [FROCOS05] were oriented: none

(19) Obligation:

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

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) Obligation:

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

IF1(true, x) → IF2(x, x)
IF2(x, y) → IF3(le(y, 10), x, y)
IF3(true, x, y) → IF2(x, s(y))
IF3(false, x, y) → GEN(s(x))
GEN(x) → IF1(le(x, 10), x)

The TRS R consists of the following rules:

table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))

The set Q consists of the following terms:

table
gen(x0)
if1(false, x0)
if1(true, x0)
if2(x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
10

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