(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) 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.
(9) 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.
(10) 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.