Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
F(true, x, y, z) → GT(x, plus(y, z))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
GT(s(u), s(v)) → GT(u, v)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y, z) → PLUS(y, z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(true, x, y, z) → GT(x, plus(y, z))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
GT(s(u), s(v)) → GT(u, v)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y, z) → PLUS(y, z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 2 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
GT(s(u), s(v)) → GT(u, v)
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
GT(s(u), s(v)) → GT(u, v)
R is empty.
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
GT(s(u), s(v)) → GT(u, v)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] 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:
- GT(s(u), s(v)) → GT(u, v)
The graph contains the following edges 1 > 1, 2 > 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
PLUS(n, s(m)) → PLUS(n, m)
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
PLUS(n, s(m)) → PLUS(n, m)
R is empty.
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
PLUS(n, s(m)) → PLUS(n, m)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] 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(n, s(m)) → PLUS(n, m)
The graph contains the following edges 1 >= 1, 2 > 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
f(true, x, y, z) → f(gt(x, plus(y, z)), x, s(y), z)
f(true, x, y, z) → f(gt(x, plus(y, z)), x, y, s(z))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
f(true, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
f(true, x0, x1, x2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) at position [0] we obtained the following new rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1))
F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0)
F(true, 0, y1, y2) → F(false, 0, s(y1), y2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0)
F(true, 0, y1, y2) → F(false, 0, s(y1), y2)
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1))
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) at position [0] we obtained the following new rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1)))
F(true, y0, x0, 0) → F(gt(y0, x0), y0, x0, s(0))
F(true, 0, y1, y2) → F(false, 0, y1, s(y2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1)))
F(true, y0, x0, 0) → F(gt(y0, x0), y0, x0, s(0))
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1))
F(true, 0, y1, y2) → F(false, 0, y1, s(y2))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 2 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1)))
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, s(x0), s(x1)) we obtained the following new rules:
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, s(z1), s(s(z2)))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, s(z1), s(s(z2)))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, s(z1), s(s(z2))) at position [0,1,0] we obtained the following new rules:
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, s(z1), s(s(z2)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, s(z1), s(s(z2)))
F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1)))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, y0, x0, s(x1)) → F(gt(y0, s(plus(x0, x1))), y0, x0, s(s(x1))) we obtained the following new rules:
F(true, z0, s(s(z1)), s(z2)) → F(gt(z0, s(plus(s(s(z1)), z2))), z0, s(s(z1)), s(s(z2)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, z1, s(s(s(z2))))
F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(plus(s(z1), s(z2)))), z0, s(z1), s(s(s(z2))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, z0, s(s(z1)), s(z2)) → F(gt(z0, s(plus(s(s(z1)), z2))), z0, s(s(z1)), s(s(z2)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, s(z1), s(s(z2)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, z1, s(s(s(z2))))
F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(plus(s(z1), s(z2)))), z0, s(z1), s(s(s(z2))))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, z0, z1, s(s(z2))) → F(gt(z0, s(plus(z1, s(z2)))), z0, z1, s(s(s(z2)))) at position [0,1,0] we obtained the following new rules:
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, z1, s(s(s(z2))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, s(z1), s(s(z2)))
F(true, z0, s(s(z1)), s(z2)) → F(gt(z0, s(plus(s(s(z1)), z2))), z0, s(s(z1)), s(s(z2)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, z1, s(s(s(z2))))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(plus(s(z1), s(z2)))), z0, s(z1), s(s(s(z2))))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(plus(s(z1), s(z2)))), z0, s(z1), s(s(s(z2)))) at position [0,1,0] we obtained the following new rules:
F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(s(plus(s(z1), z2)))), z0, s(z1), s(s(s(z2))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, z0, s(s(z1)), s(z2)) → F(gt(z0, s(plus(s(s(z1)), z2))), z0, s(s(z1)), s(s(z2)))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, s(z1), s(s(z2)))
F(true, z0, s(z1), s(s(z2))) → F(gt(z0, s(s(plus(s(z1), z2)))), z0, s(z1), s(s(s(z2))))
F(true, z0, z1, s(s(z2))) → F(gt(z0, s(s(plus(z1, z2)))), z0, z1, s(s(s(z2))))
F(true, z0, s(z1), s(z2)) → F(gt(z0, s(plus(s(z1), z2))), z0, s(s(z1)), s(z2))
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0)
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0)
The TRS R consists of the following rules:
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
plus(x0, s(x1))
plus(x0, 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0)
The TRS R consists of the following rules:
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, y0, x0, 0) → F(gt(y0, x0), y0, s(x0), 0) we obtained the following new rules:
F(true, z0, s(z1), 0) → F(gt(z0, s(z1)), z0, s(s(z1)), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
F(true, z0, s(z1), 0) → F(gt(z0, s(z1)), z0, s(s(z1)), 0)
The TRS R consists of the following rules:
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
gt(s(x0), s(x1))
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus with the following steps:
Note that final constraints are written in bold face.
For Pair F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) the following chains were created:
- We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z), F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) which results in the following constraint:
- (1) (F(gt(x0, plus(x1, x2)), x0, s(x1), x2)=F(true, x3, x4, x5) ⇒ F(true, x0, x1, x2)≥F(gt(x0, plus(x1, x2)), x0, s(x1), x2))
We simplified constraint (1) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (2) (plus(x1, x2)=x24∧gt(x0, x24)=true ⇒ F(true, x0, x1, x2)≥F(gt(x0, plus(x1, x2)), x0, s(x1), x2))
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on gt(x0, x24)=true which results in the following new constraints:
- (3) (true=true∧plus(x1, x2)=0 ⇒ F(true, s(x26), x1, x2)≥F(gt(s(x26), plus(x1, x2)), s(x26), s(x1), x2))
- (4) (gt(x27, x28)=true∧plus(x1, x2)=s(x28)∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, x29, x30)≥F(gt(x27, plus(x29, x30)), x27, s(x29), x30)) ⇒ F(true, s(x27), x1, x2)≥F(gt(s(x27), plus(x1, x2)), s(x27), s(x1), x2))
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
- (5) (plus(x1, x2)=0 ⇒ F(true, s(x26), x1, x2)≥F(gt(s(x26), plus(x1, x2)), s(x26), s(x1), x2))
We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on plus(x1, x2)=s(x28) which results in the following new constraints:
- (6) (x34=s(x28)∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, x29, x30)≥F(gt(x27, plus(x29, x30)), x27, s(x29), x30)) ⇒ F(true, s(x27), x34, 0)≥F(gt(s(x27), plus(x34, 0)), s(x27), s(x34), 0))
- (7) (s(plus(x35, x36))=s(x28)∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, x29, x30)≥F(gt(x27, plus(x29, x30)), x27, s(x29), x30))∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, x39, x40)≥F(gt(x38, plus(x39, x40)), x38, s(x39), x40)) ⇒ F(true, s(x38), x35, x36)≥F(gt(s(x38), plus(x35, x36)), s(x38), s(x35), x36)) ⇒ F(true, s(x27), x35, s(x36))≥F(gt(s(x27), plus(x35, s(x36))), s(x27), s(x35), s(x36)))
We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on plus(x1, x2)=0 which results in the following new constraint:
- (8) (x31=0 ⇒ F(true, s(x26), x31, 0)≥F(gt(s(x26), plus(x31, 0)), s(x26), s(x31), 0))
We simplified constraint (8) using rule (III) which results in the following new constraint:
- (9) (F(true, s(x26), 0, 0)≥F(gt(s(x26), plus(0, 0)), s(x26), s(0), 0))
We simplified constraint (6) using rules (III), (IV) which results in the following new constraint:
- (10) (gt(x27, x28)=true ⇒ F(true, s(x27), s(x28), 0)≥F(gt(s(x27), plus(s(x28), 0)), s(x27), s(s(x28)), 0))
We simplified constraint (7) using rules (I), (II) which results in the following new constraint:
- (11) (plus(x35, x36)=x28∧gt(x27, x28)=true∧(∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, x29, x30)≥F(gt(x27, plus(x29, x30)), x27, s(x29), x30))∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, x39, x40)≥F(gt(x38, plus(x39, x40)), x38, s(x39), x40)) ⇒ F(true, s(x38), x35, x36)≥F(gt(s(x38), plus(x35, x36)), s(x38), s(x35), x36)) ⇒ F(true, s(x27), x35, s(x36))≥F(gt(s(x27), plus(x35, s(x36))), s(x27), s(x35), s(x36)))
We simplified constraint (10) using rule (V) (with possible (I) afterwards) using induction on gt(x27, x28)=true which results in the following new constraints:
- (12) (true=true ⇒ F(true, s(s(x42)), s(0), 0)≥F(gt(s(s(x42)), plus(s(0), 0)), s(s(x42)), s(s(0)), 0))
- (13) (gt(x43, x44)=true∧(gt(x43, x44)=true ⇒ F(true, s(x43), s(x44), 0)≥F(gt(s(x43), plus(s(x44), 0)), s(x43), s(s(x44)), 0)) ⇒ F(true, s(s(x43)), s(s(x44)), 0)≥F(gt(s(s(x43)), plus(s(s(x44)), 0)), s(s(x43)), s(s(s(x44))), 0))
We simplified constraint (12) using rules (I), (II) which results in the following new constraint:
- (14) (F(true, s(s(x42)), s(0), 0)≥F(gt(s(s(x42)), plus(s(0), 0)), s(s(x42)), s(s(0)), 0))
We simplified constraint (13) using rule (VI) where we applied the induction hypothesis (gt(x43, x44)=true ⇒ F(true, s(x43), s(x44), 0)≥F(gt(s(x43), plus(s(x44), 0)), s(x43), s(s(x44)), 0)) with σ = [ ] which results in the following new constraint:
- (15) (F(true, s(x43), s(x44), 0)≥F(gt(s(x43), plus(s(x44), 0)), s(x43), s(s(x44)), 0) ⇒ F(true, s(s(x43)), s(s(x44)), 0)≥F(gt(s(s(x43)), plus(s(s(x44)), 0)), s(s(x43)), s(s(s(x44))), 0))
We simplified constraint (11) using rule (VI) where we applied the induction hypothesis (∀x29,x30:gt(x27, x28)=true∧plus(x29, x30)=x28 ⇒ F(true, x27, x29, x30)≥F(gt(x27, plus(x29, x30)), x27, s(x29), x30)) with σ = [x29 / x35, x30 / x36] which results in the following new constraint:
- (16) (F(true, x27, x35, x36)≥F(gt(x27, plus(x35, x36)), x27, s(x35), x36)∧(∀x37,x38,x39,x40:plus(x35, x36)=s(x37)∧gt(x38, x37)=true∧(∀x39,x40:gt(x38, x37)=true∧plus(x39, x40)=x37 ⇒ F(true, x38, x39, x40)≥F(gt(x38, plus(x39, x40)), x38, s(x39), x40)) ⇒ F(true, s(x38), x35, x36)≥F(gt(s(x38), plus(x35, x36)), s(x38), s(x35), x36)) ⇒ F(true, s(x27), x35, s(x36))≥F(gt(s(x27), plus(x35, s(x36))), s(x27), s(x35), s(x36)))
We simplified constraint (16) using rule (IV) which results in the following new constraint:
- (17) (F(true, x27, x35, x36)≥F(gt(x27, plus(x35, x36)), x27, s(x35), x36) ⇒ F(true, s(x27), x35, s(x36))≥F(gt(s(x27), plus(x35, s(x36))), s(x27), s(x35), s(x36)))
- We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z), F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) which results in the following constraint:
- (18) (F(gt(x6, plus(x7, x8)), x6, s(x7), x8)=F(true, x9, x10, x11) ⇒ F(true, x6, x7, x8)≥F(gt(x6, plus(x7, x8)), x6, s(x7), x8))
We simplified constraint (18) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (19) (plus(x7, x8)=x45∧gt(x6, x45)=true ⇒ F(true, x6, x7, x8)≥F(gt(x6, plus(x7, x8)), x6, s(x7), x8))
We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on gt(x6, x45)=true which results in the following new constraints:
- (20) (true=true∧plus(x7, x8)=0 ⇒ F(true, s(x47), x7, x8)≥F(gt(s(x47), plus(x7, x8)), s(x47), s(x7), x8))
- (21) (gt(x48, x49)=true∧plus(x7, x8)=s(x49)∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, x51)≥F(gt(x48, plus(x50, x51)), x48, s(x50), x51)) ⇒ F(true, s(x48), x7, x8)≥F(gt(s(x48), plus(x7, x8)), s(x48), s(x7), x8))
We simplified constraint (20) using rules (I), (II) which results in the following new constraint:
- (22) (plus(x7, x8)=0 ⇒ F(true, s(x47), x7, x8)≥F(gt(s(x47), plus(x7, x8)), s(x47), s(x7), x8))
We simplified constraint (21) using rule (V) (with possible (I) afterwards) using induction on plus(x7, x8)=s(x49) which results in the following new constraints:
- (23) (x55=s(x49)∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, x51)≥F(gt(x48, plus(x50, x51)), x48, s(x50), x51)) ⇒ F(true, s(x48), x55, 0)≥F(gt(s(x48), plus(x55, 0)), s(x48), s(x55), 0))
- (24) (s(plus(x56, x57))=s(x49)∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, x51)≥F(gt(x48, plus(x50, x51)), x48, s(x50), x51))∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, x61)≥F(gt(x59, plus(x60, x61)), x59, s(x60), x61)) ⇒ F(true, s(x59), x56, x57)≥F(gt(s(x59), plus(x56, x57)), s(x59), s(x56), x57)) ⇒ F(true, s(x48), x56, s(x57))≥F(gt(s(x48), plus(x56, s(x57))), s(x48), s(x56), s(x57)))
We simplified constraint (22) using rule (V) (with possible (I) afterwards) using induction on plus(x7, x8)=0 which results in the following new constraint:
- (25) (x52=0 ⇒ F(true, s(x47), x52, 0)≥F(gt(s(x47), plus(x52, 0)), s(x47), s(x52), 0))
We simplified constraint (25) using rule (III) which results in the following new constraint:
- (26) (F(true, s(x47), 0, 0)≥F(gt(s(x47), plus(0, 0)), s(x47), s(0), 0))
We simplified constraint (23) using rules (III), (IV) which results in the following new constraint:
- (27) (gt(x48, x49)=true ⇒ F(true, s(x48), s(x49), 0)≥F(gt(s(x48), plus(s(x49), 0)), s(x48), s(s(x49)), 0))
We simplified constraint (24) using rules (I), (II) which results in the following new constraint:
- (28) (plus(x56, x57)=x49∧gt(x48, x49)=true∧(∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, x51)≥F(gt(x48, plus(x50, x51)), x48, s(x50), x51))∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, x61)≥F(gt(x59, plus(x60, x61)), x59, s(x60), x61)) ⇒ F(true, s(x59), x56, x57)≥F(gt(s(x59), plus(x56, x57)), s(x59), s(x56), x57)) ⇒ F(true, s(x48), x56, s(x57))≥F(gt(s(x48), plus(x56, s(x57))), s(x48), s(x56), s(x57)))
We simplified constraint (27) using rule (V) (with possible (I) afterwards) using induction on gt(x48, x49)=true which results in the following new constraints:
- (29) (true=true ⇒ F(true, s(s(x63)), s(0), 0)≥F(gt(s(s(x63)), plus(s(0), 0)), s(s(x63)), s(s(0)), 0))
- (30) (gt(x64, x65)=true∧(gt(x64, x65)=true ⇒ F(true, s(x64), s(x65), 0)≥F(gt(s(x64), plus(s(x65), 0)), s(x64), s(s(x65)), 0)) ⇒ F(true, s(s(x64)), s(s(x65)), 0)≥F(gt(s(s(x64)), plus(s(s(x65)), 0)), s(s(x64)), s(s(s(x65))), 0))
We simplified constraint (29) using rules (I), (II) which results in the following new constraint:
- (31) (F(true, s(s(x63)), s(0), 0)≥F(gt(s(s(x63)), plus(s(0), 0)), s(s(x63)), s(s(0)), 0))
We simplified constraint (30) using rule (VI) where we applied the induction hypothesis (gt(x64, x65)=true ⇒ F(true, s(x64), s(x65), 0)≥F(gt(s(x64), plus(s(x65), 0)), s(x64), s(s(x65)), 0)) with σ = [ ] which results in the following new constraint:
- (32) (F(true, s(x64), s(x65), 0)≥F(gt(s(x64), plus(s(x65), 0)), s(x64), s(s(x65)), 0) ⇒ F(true, s(s(x64)), s(s(x65)), 0)≥F(gt(s(s(x64)), plus(s(s(x65)), 0)), s(s(x64)), s(s(s(x65))), 0))
We simplified constraint (28) using rule (VI) where we applied the induction hypothesis (∀x50,x51:gt(x48, x49)=true∧plus(x50, x51)=x49 ⇒ F(true, x48, x50, x51)≥F(gt(x48, plus(x50, x51)), x48, s(x50), x51)) with σ = [x51 / x57, x50 / x56] which results in the following new constraint:
- (33) (F(true, x48, x56, x57)≥F(gt(x48, plus(x56, x57)), x48, s(x56), x57)∧(∀x58,x59,x60,x61:plus(x56, x57)=s(x58)∧gt(x59, x58)=true∧(∀x60,x61:gt(x59, x58)=true∧plus(x60, x61)=x58 ⇒ F(true, x59, x60, x61)≥F(gt(x59, plus(x60, x61)), x59, s(x60), x61)) ⇒ F(true, s(x59), x56, x57)≥F(gt(s(x59), plus(x56, x57)), s(x59), s(x56), x57)) ⇒ F(true, s(x48), x56, s(x57))≥F(gt(s(x48), plus(x56, s(x57))), s(x48), s(x56), s(x57)))
We simplified constraint (33) using rule (IV) which results in the following new constraint:
- (34) (F(true, x48, x56, x57)≥F(gt(x48, plus(x56, x57)), x48, s(x56), x57) ⇒ F(true, s(x48), x56, s(x57))≥F(gt(s(x48), plus(x56, s(x57))), s(x48), s(x56), s(x57)))
For Pair F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) the following chains were created:
- We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)), F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z) which results in the following constraint:
- (35) (F(gt(x12, plus(x13, x14)), x12, x13, s(x14))=F(true, x15, x16, x17) ⇒ F(true, x12, x13, x14)≥F(gt(x12, plus(x13, x14)), x12, x13, s(x14)))
We simplified constraint (35) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (36) (plus(x13, x14)=x66∧gt(x12, x66)=true ⇒ F(true, x12, x13, x14)≥F(gt(x12, plus(x13, x14)), x12, x13, s(x14)))
We simplified constraint (36) using rule (V) (with possible (I) afterwards) using induction on gt(x12, x66)=true which results in the following new constraints:
- (37) (true=true∧plus(x13, x14)=0 ⇒ F(true, s(x68), x13, x14)≥F(gt(s(x68), plus(x13, x14)), s(x68), x13, s(x14)))
- (38) (gt(x69, x70)=true∧plus(x13, x14)=s(x70)∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, x71, x72)≥F(gt(x69, plus(x71, x72)), x69, x71, s(x72))) ⇒ F(true, s(x69), x13, x14)≥F(gt(s(x69), plus(x13, x14)), s(x69), x13, s(x14)))
We simplified constraint (37) using rules (I), (II) which results in the following new constraint:
- (39) (plus(x13, x14)=0 ⇒ F(true, s(x68), x13, x14)≥F(gt(s(x68), plus(x13, x14)), s(x68), x13, s(x14)))
We simplified constraint (38) using rule (V) (with possible (I) afterwards) using induction on plus(x13, x14)=s(x70) which results in the following new constraints:
- (40) (x76=s(x70)∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, x71, x72)≥F(gt(x69, plus(x71, x72)), x69, x71, s(x72))) ⇒ F(true, s(x69), x76, 0)≥F(gt(s(x69), plus(x76, 0)), s(x69), x76, s(0)))
- (41) (s(plus(x77, x78))=s(x70)∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, x71, x72)≥F(gt(x69, plus(x71, x72)), x69, x71, s(x72)))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, x81, x82)≥F(gt(x80, plus(x81, x82)), x80, x81, s(x82))) ⇒ F(true, s(x80), x77, x78)≥F(gt(s(x80), plus(x77, x78)), s(x80), x77, s(x78))) ⇒ F(true, s(x69), x77, s(x78))≥F(gt(s(x69), plus(x77, s(x78))), s(x69), x77, s(s(x78))))
We simplified constraint (39) using rule (V) (with possible (I) afterwards) using induction on plus(x13, x14)=0 which results in the following new constraint:
- (42) (x73=0 ⇒ F(true, s(x68), x73, 0)≥F(gt(s(x68), plus(x73, 0)), s(x68), x73, s(0)))
We simplified constraint (42) using rule (III) which results in the following new constraint:
- (43) (F(true, s(x68), 0, 0)≥F(gt(s(x68), plus(0, 0)), s(x68), 0, s(0)))
We simplified constraint (40) using rules (III), (IV) which results in the following new constraint:
- (44) (gt(x69, x70)=true ⇒ F(true, s(x69), s(x70), 0)≥F(gt(s(x69), plus(s(x70), 0)), s(x69), s(x70), s(0)))
We simplified constraint (41) using rules (I), (II) which results in the following new constraint:
- (45) (plus(x77, x78)=x70∧gt(x69, x70)=true∧(∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, x71, x72)≥F(gt(x69, plus(x71, x72)), x69, x71, s(x72)))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, x81, x82)≥F(gt(x80, plus(x81, x82)), x80, x81, s(x82))) ⇒ F(true, s(x80), x77, x78)≥F(gt(s(x80), plus(x77, x78)), s(x80), x77, s(x78))) ⇒ F(true, s(x69), x77, s(x78))≥F(gt(s(x69), plus(x77, s(x78))), s(x69), x77, s(s(x78))))
We simplified constraint (44) using rule (V) (with possible (I) afterwards) using induction on gt(x69, x70)=true which results in the following new constraints:
- (46) (true=true ⇒ F(true, s(s(x84)), s(0), 0)≥F(gt(s(s(x84)), plus(s(0), 0)), s(s(x84)), s(0), s(0)))
- (47) (gt(x85, x86)=true∧(gt(x85, x86)=true ⇒ F(true, s(x85), s(x86), 0)≥F(gt(s(x85), plus(s(x86), 0)), s(x85), s(x86), s(0))) ⇒ F(true, s(s(x85)), s(s(x86)), 0)≥F(gt(s(s(x85)), plus(s(s(x86)), 0)), s(s(x85)), s(s(x86)), s(0)))
We simplified constraint (46) using rules (I), (II) which results in the following new constraint:
- (48) (F(true, s(s(x84)), s(0), 0)≥F(gt(s(s(x84)), plus(s(0), 0)), s(s(x84)), s(0), s(0)))
We simplified constraint (47) using rule (VI) where we applied the induction hypothesis (gt(x85, x86)=true ⇒ F(true, s(x85), s(x86), 0)≥F(gt(s(x85), plus(s(x86), 0)), s(x85), s(x86), s(0))) with σ = [ ] which results in the following new constraint:
- (49) (F(true, s(x85), s(x86), 0)≥F(gt(s(x85), plus(s(x86), 0)), s(x85), s(x86), s(0)) ⇒ F(true, s(s(x85)), s(s(x86)), 0)≥F(gt(s(s(x85)), plus(s(s(x86)), 0)), s(s(x85)), s(s(x86)), s(0)))
We simplified constraint (45) using rule (VI) where we applied the induction hypothesis (∀x71,x72:gt(x69, x70)=true∧plus(x71, x72)=x70 ⇒ F(true, x69, x71, x72)≥F(gt(x69, plus(x71, x72)), x69, x71, s(x72))) with σ = [x71 / x77, x72 / x78] which results in the following new constraint:
- (50) (F(true, x69, x77, x78)≥F(gt(x69, plus(x77, x78)), x69, x77, s(x78))∧(∀x79,x80,x81,x82:plus(x77, x78)=s(x79)∧gt(x80, x79)=true∧(∀x81,x82:gt(x80, x79)=true∧plus(x81, x82)=x79 ⇒ F(true, x80, x81, x82)≥F(gt(x80, plus(x81, x82)), x80, x81, s(x82))) ⇒ F(true, s(x80), x77, x78)≥F(gt(s(x80), plus(x77, x78)), s(x80), x77, s(x78))) ⇒ F(true, s(x69), x77, s(x78))≥F(gt(s(x69), plus(x77, s(x78))), s(x69), x77, s(s(x78))))
We simplified constraint (50) using rule (IV) which results in the following new constraint:
- (51) (F(true, x69, x77, x78)≥F(gt(x69, plus(x77, x78)), x69, x77, s(x78)) ⇒ F(true, s(x69), x77, s(x78))≥F(gt(s(x69), plus(x77, s(x78))), s(x69), x77, s(s(x78))))
- We consider the chain F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)), F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z)) which results in the following constraint:
- (52) (F(gt(x18, plus(x19, x20)), x18, x19, s(x20))=F(true, x21, x22, x23) ⇒ F(true, x18, x19, x20)≥F(gt(x18, plus(x19, x20)), x18, x19, s(x20)))
We simplified constraint (52) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (53) (plus(x19, x20)=x87∧gt(x18, x87)=true ⇒ F(true, x18, x19, x20)≥F(gt(x18, plus(x19, x20)), x18, x19, s(x20)))
We simplified constraint (53) using rule (V) (with possible (I) afterwards) using induction on gt(x18, x87)=true which results in the following new constraints:
- (54) (true=true∧plus(x19, x20)=0 ⇒ F(true, s(x89), x19, x20)≥F(gt(s(x89), plus(x19, x20)), s(x89), x19, s(x20)))
- (55) (gt(x90, x91)=true∧plus(x19, x20)=s(x91)∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, x93)≥F(gt(x90, plus(x92, x93)), x90, x92, s(x93))) ⇒ F(true, s(x90), x19, x20)≥F(gt(s(x90), plus(x19, x20)), s(x90), x19, s(x20)))
We simplified constraint (54) using rules (I), (II) which results in the following new constraint:
- (56) (plus(x19, x20)=0 ⇒ F(true, s(x89), x19, x20)≥F(gt(s(x89), plus(x19, x20)), s(x89), x19, s(x20)))
We simplified constraint (55) using rule (V) (with possible (I) afterwards) using induction on plus(x19, x20)=s(x91) which results in the following new constraints:
- (57) (x97=s(x91)∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, x93)≥F(gt(x90, plus(x92, x93)), x90, x92, s(x93))) ⇒ F(true, s(x90), x97, 0)≥F(gt(s(x90), plus(x97, 0)), s(x90), x97, s(0)))
- (58) (s(plus(x98, x99))=s(x91)∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, x93)≥F(gt(x90, plus(x92, x93)), x90, x92, s(x93)))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, x103)≥F(gt(x101, plus(x102, x103)), x101, x102, s(x103))) ⇒ F(true, s(x101), x98, x99)≥F(gt(s(x101), plus(x98, x99)), s(x101), x98, s(x99))) ⇒ F(true, s(x90), x98, s(x99))≥F(gt(s(x90), plus(x98, s(x99))), s(x90), x98, s(s(x99))))
We simplified constraint (56) using rule (V) (with possible (I) afterwards) using induction on plus(x19, x20)=0 which results in the following new constraint:
- (59) (x94=0 ⇒ F(true, s(x89), x94, 0)≥F(gt(s(x89), plus(x94, 0)), s(x89), x94, s(0)))
We simplified constraint (59) using rule (III) which results in the following new constraint:
- (60) (F(true, s(x89), 0, 0)≥F(gt(s(x89), plus(0, 0)), s(x89), 0, s(0)))
We simplified constraint (57) using rules (III), (IV) which results in the following new constraint:
- (61) (gt(x90, x91)=true ⇒ F(true, s(x90), s(x91), 0)≥F(gt(s(x90), plus(s(x91), 0)), s(x90), s(x91), s(0)))
We simplified constraint (58) using rules (I), (II) which results in the following new constraint:
- (62) (plus(x98, x99)=x91∧gt(x90, x91)=true∧(∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, x93)≥F(gt(x90, plus(x92, x93)), x90, x92, s(x93)))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, x103)≥F(gt(x101, plus(x102, x103)), x101, x102, s(x103))) ⇒ F(true, s(x101), x98, x99)≥F(gt(s(x101), plus(x98, x99)), s(x101), x98, s(x99))) ⇒ F(true, s(x90), x98, s(x99))≥F(gt(s(x90), plus(x98, s(x99))), s(x90), x98, s(s(x99))))
We simplified constraint (61) using rule (V) (with possible (I) afterwards) using induction on gt(x90, x91)=true which results in the following new constraints:
- (63) (true=true ⇒ F(true, s(s(x105)), s(0), 0)≥F(gt(s(s(x105)), plus(s(0), 0)), s(s(x105)), s(0), s(0)))
- (64) (gt(x106, x107)=true∧(gt(x106, x107)=true ⇒ F(true, s(x106), s(x107), 0)≥F(gt(s(x106), plus(s(x107), 0)), s(x106), s(x107), s(0))) ⇒ F(true, s(s(x106)), s(s(x107)), 0)≥F(gt(s(s(x106)), plus(s(s(x107)), 0)), s(s(x106)), s(s(x107)), s(0)))
We simplified constraint (63) using rules (I), (II) which results in the following new constraint:
- (65) (F(true, s(s(x105)), s(0), 0)≥F(gt(s(s(x105)), plus(s(0), 0)), s(s(x105)), s(0), s(0)))
We simplified constraint (64) using rule (VI) where we applied the induction hypothesis (gt(x106, x107)=true ⇒ F(true, s(x106), s(x107), 0)≥F(gt(s(x106), plus(s(x107), 0)), s(x106), s(x107), s(0))) with σ = [ ] which results in the following new constraint:
- (66) (F(true, s(x106), s(x107), 0)≥F(gt(s(x106), plus(s(x107), 0)), s(x106), s(x107), s(0)) ⇒ F(true, s(s(x106)), s(s(x107)), 0)≥F(gt(s(s(x106)), plus(s(s(x107)), 0)), s(s(x106)), s(s(x107)), s(0)))
We simplified constraint (62) using rule (VI) where we applied the induction hypothesis (∀x92,x93:gt(x90, x91)=true∧plus(x92, x93)=x91 ⇒ F(true, x90, x92, x93)≥F(gt(x90, plus(x92, x93)), x90, x92, s(x93))) with σ = [x93 / x99, x92 / x98] which results in the following new constraint:
- (67) (F(true, x90, x98, x99)≥F(gt(x90, plus(x98, x99)), x90, x98, s(x99))∧(∀x100,x101,x102,x103:plus(x98, x99)=s(x100)∧gt(x101, x100)=true∧(∀x102,x103:gt(x101, x100)=true∧plus(x102, x103)=x100 ⇒ F(true, x101, x102, x103)≥F(gt(x101, plus(x102, x103)), x101, x102, s(x103))) ⇒ F(true, s(x101), x98, x99)≥F(gt(s(x101), plus(x98, x99)), s(x101), x98, s(x99))) ⇒ F(true, s(x90), x98, s(x99))≥F(gt(s(x90), plus(x98, s(x99))), s(x90), x98, s(s(x99))))
We simplified constraint (67) using rule (IV) which results in the following new constraint:
- (68) (F(true, x90, x98, x99)≥F(gt(x90, plus(x98, x99)), x90, x98, s(x99)) ⇒ F(true, s(x90), x98, s(x99))≥F(gt(s(x90), plus(x98, s(x99))), s(x90), x98, s(s(x99))))
To summarize, we get the following constraints P≥ for the following pairs.
- F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
- (F(true, s(x26), 0, 0)≥F(gt(s(x26), plus(0, 0)), s(x26), s(0), 0))
- (F(true, s(s(x42)), s(0), 0)≥F(gt(s(s(x42)), plus(s(0), 0)), s(s(x42)), s(s(0)), 0))
- (F(true, s(x43), s(x44), 0)≥F(gt(s(x43), plus(s(x44), 0)), s(x43), s(s(x44)), 0) ⇒ F(true, s(s(x43)), s(s(x44)), 0)≥F(gt(s(s(x43)), plus(s(s(x44)), 0)), s(s(x43)), s(s(s(x44))), 0))
- (F(true, x27, x35, x36)≥F(gt(x27, plus(x35, x36)), x27, s(x35), x36) ⇒ F(true, s(x27), x35, s(x36))≥F(gt(s(x27), plus(x35, s(x36))), s(x27), s(x35), s(x36)))
- (F(true, s(x47), 0, 0)≥F(gt(s(x47), plus(0, 0)), s(x47), s(0), 0))
- (F(true, s(s(x63)), s(0), 0)≥F(gt(s(s(x63)), plus(s(0), 0)), s(s(x63)), s(s(0)), 0))
- (F(true, s(x64), s(x65), 0)≥F(gt(s(x64), plus(s(x65), 0)), s(x64), s(s(x65)), 0) ⇒ F(true, s(s(x64)), s(s(x65)), 0)≥F(gt(s(s(x64)), plus(s(s(x65)), 0)), s(s(x64)), s(s(s(x65))), 0))
- (F(true, x48, x56, x57)≥F(gt(x48, plus(x56, x57)), x48, s(x56), x57) ⇒ F(true, s(x48), x56, s(x57))≥F(gt(s(x48), plus(x56, s(x57))), s(x48), s(x56), s(x57)))
- F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
- (F(true, s(x68), 0, 0)≥F(gt(s(x68), plus(0, 0)), s(x68), 0, s(0)))
- (F(true, s(s(x84)), s(0), 0)≥F(gt(s(s(x84)), plus(s(0), 0)), s(s(x84)), s(0), s(0)))
- (F(true, s(x85), s(x86), 0)≥F(gt(s(x85), plus(s(x86), 0)), s(x85), s(x86), s(0)) ⇒ F(true, s(s(x85)), s(s(x86)), 0)≥F(gt(s(s(x85)), plus(s(s(x86)), 0)), s(s(x85)), s(s(x86)), s(0)))
- (F(true, x69, x77, x78)≥F(gt(x69, plus(x77, x78)), x69, x77, s(x78)) ⇒ F(true, s(x69), x77, s(x78))≥F(gt(s(x69), plus(x77, s(x78))), s(x69), x77, s(s(x78))))
- (F(true, s(x89), 0, 0)≥F(gt(s(x89), plus(0, 0)), s(x89), 0, s(0)))
- (F(true, s(s(x105)), s(0), 0)≥F(gt(s(s(x105)), plus(s(0), 0)), s(s(x105)), s(0), s(0)))
- (F(true, s(x106), s(x107), 0)≥F(gt(s(x106), plus(s(x107), 0)), s(x106), s(x107), s(0)) ⇒ F(true, s(s(x106)), s(s(x107)), 0)≥F(gt(s(s(x106)), plus(s(s(x107)), 0)), s(s(x106)), s(s(x107)), s(0)))
- (F(true, x90, x98, x99)≥F(gt(x90, plus(x98, x99)), x90, x98, s(x99)) ⇒ F(true, s(x90), x98, s(x99))≥F(gt(s(x90), plus(x98, s(x99))), s(x90), x98, s(s(x99))))
The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved.
Polynomial interpretation [21]:
POL(0) = 0
POL(F(x1, x2, x3, x4)) = -1 + x2 - x3 - x4
POL(c) = -1
POL(false) = 1
POL(gt(x1, x2)) = x2
POL(plus(x1, x2)) = 1
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in P>:
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
The following pairs are in Pbound:
F(true, x, y, z) → F(gt(x, plus(y, z)), x, s(y), z)
F(true, x, y, z) → F(gt(x, plus(y, z)), x, y, s(z))
There are no usable rules
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
The set Q consists of the following terms:
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
gt(s(x0), 0)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.