MAYBE
Termination w.r.t. Q proof of ../tpdb/TRS/higher-order/ToyamaRTA04/Ex6Recursor.trs
Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
Q is empty.
↳ QTRS
↳ Overlay + Local Confluence
Q restricted rewrite system:
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
Q is empty.
The TRS is overlay and locally confluent. By [19] we can switch to innermost.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y)) at position [1] we obtained the following new rules:
APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y)) we obtained the following new rules:
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))
APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y) we obtained the following new rules:
APP(app(app(rec, x0), x1), app(s, app(s, 0))) → APP(app(app(rec, x0), x1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, app(s, y_2))) → APP(app(app(rec, x0), x1), app(s, y_2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, app(s, y_3)))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3)))
APP(app(app(rec, x0), x1), app(s, app(s, app(s, y_2)))) → APP(app(app(rec, x0), x1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, y_3))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, 0))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ Narrowing
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
APP(app(app(rec, x0), x1), app(s, app(s, y_2))) → APP(app(app(rec, x0), x1), app(s, y_2))
APP(app(app(rec, x0), x1), app(s, app(s, 0))) → APP(app(app(rec, x0), x1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, app(s, y_3)))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, app(s, app(s, y_2)))) → APP(app(app(rec, x0), x1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, y_3))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, 0))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
The TRS R consists of the following rules:
app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))
The set Q consists of the following terms:
app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))
We have to consider all minimal (P,Q,R)-chains.