MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
facIter(x,y) -> if(isZero(x),minus(x,s(0())),y,times(y,x))
factorial(x) -> facIter(x,s(0()))
if(false(),x,y,z) -> facIter(x,z)
if(true(),x,y,z) -> y
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2} / {0/0,false/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter,factorial,if,isZero,minus,p,plus
,times} and constructors {0,false,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
if#(true(),x,y,z) -> c_4()
isZero#(0()) -> c_5()
isZero#(s(x)) -> c_6()
minus#(x,0()) -> c_7()
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
minus#(0(),x) -> c_9()
p#(0()) -> c_10()
p#(s(x)) -> c_11()
plus#(0(),x) -> c_12()
plus#(s(x),y) -> c_13(plus#(x,y))
times#(0(),y) -> c_14()
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
if#(true(),x,y,z) -> c_4()
isZero#(0()) -> c_5()
isZero#(s(x)) -> c_6()
minus#(x,0()) -> c_7()
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
minus#(0(),x) -> c_9()
p#(0()) -> c_10()
p#(s(x)) -> c_11()
plus#(0(),x) -> c_12()
plus#(s(x),y) -> c_13(plus#(x,y))
times#(0(),y) -> c_14()
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak TRS:
facIter(x,y) -> if(isZero(x),minus(x,s(0())),y,times(y,x))
factorial(x) -> facIter(x,s(0()))
if(false(),x,y,z) -> facIter(x,z)
if(true(),x,y,z) -> y
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/4,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
if#(true(),x,y,z) -> c_4()
isZero#(0()) -> c_5()
isZero#(s(x)) -> c_6()
minus#(x,0()) -> c_7()
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
minus#(0(),x) -> c_9()
p#(0()) -> c_10()
p#(s(x)) -> c_11()
plus#(0(),x) -> c_12()
plus#(s(x),y) -> c_13(plus#(x,y))
times#(0(),y) -> c_14()
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
if#(true(),x,y,z) -> c_4()
isZero#(0()) -> c_5()
isZero#(s(x)) -> c_6()
minus#(x,0()) -> c_7()
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
minus#(0(),x) -> c_9()
p#(0()) -> c_10()
p#(s(x)) -> c_11()
plus#(0(),x) -> c_12()
plus#(s(x),y) -> c_13(plus#(x,y))
times#(0(),y) -> c_14()
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak TRS:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/4,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{4,5,6,7,9,10,11,12,14}
by application of
Pre({4,5,6,7,9,10,11,12,14}) = {1,8,13,15}.
Here rules are labelled as follows:
1: facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x))
2: factorial#(x) -> c_2(facIter#(x,s(0())))
3: if#(false(),x,y,z) -> c_3(facIter#(x,z))
4: if#(true(),x,y,z) -> c_4()
5: isZero#(0()) -> c_5()
6: isZero#(s(x)) -> c_6()
7: minus#(x,0()) -> c_7()
8: minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
9: minus#(0(),x) -> c_9()
10: p#(0()) -> c_10()
11: p#(s(x)) -> c_11()
12: plus#(0(),x) -> c_12()
13: plus#(s(x),y) -> c_13(plus#(x,y))
14: times#(0(),y) -> c_14()
15: times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
plus#(s(x),y) -> c_13(plus#(x,y))
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak DPs:
if#(true(),x,y,z) -> c_4()
isZero#(0()) -> c_5()
isZero#(s(x)) -> c_6()
minus#(x,0()) -> c_7()
minus#(0(),x) -> c_9()
p#(0()) -> c_10()
p#(s(x)) -> c_11()
plus#(0(),x) -> c_12()
times#(0(),y) -> c_14()
- Weak TRS:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/4,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x))
-->_4 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_3 minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y)):4
-->_1 if#(false(),x,y,z) -> c_3(facIter#(x,z)):3
-->_4 times#(0(),y) -> c_14():15
-->_3 minus#(0(),x) -> c_9():11
-->_2 isZero#(s(x)) -> c_6():9
-->_2 isZero#(0()) -> c_5():8
-->_1 if#(true(),x,y,z) -> c_4():7
2:S:factorial#(x) -> c_2(facIter#(x,s(0())))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x)):1
3:S:if#(false(),x,y,z) -> c_3(facIter#(x,z))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x)):1
4:S:minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
-->_1 p#(s(x)) -> c_11():13
-->_1 p#(0()) -> c_10():12
-->_2 minus#(0(),x) -> c_9():11
-->_2 minus#(x,0()) -> c_7():10
-->_2 minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y)):4
5:S:plus#(s(x),y) -> c_13(plus#(x,y))
-->_1 plus#(0(),x) -> c_12():14
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
6:S:times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
-->_2 times#(0(),y) -> c_14():15
-->_1 plus#(0(),x) -> c_12():14
-->_2 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
7:W:if#(true(),x,y,z) -> c_4()
8:W:isZero#(0()) -> c_5()
9:W:isZero#(s(x)) -> c_6()
10:W:minus#(x,0()) -> c_7()
11:W:minus#(0(),x) -> c_9()
12:W:p#(0()) -> c_10()
13:W:p#(s(x)) -> c_11()
14:W:plus#(0(),x) -> c_12()
15:W:times#(0(),y) -> c_14()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: if#(true(),x,y,z) -> c_4()
8: isZero#(0()) -> c_5()
9: isZero#(s(x)) -> c_6()
10: minus#(x,0()) -> c_7()
11: minus#(0(),x) -> c_9()
12: p#(0()) -> c_10()
13: p#(s(x)) -> c_11()
14: plus#(0(),x) -> c_12()
15: times#(0(),y) -> c_14()
* Step 5: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),isZero#(x),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
plus#(s(x),y) -> c_13(plus#(x,y))
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak TRS:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/4,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/2
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x))
-->_4 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_3 minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y)):4
-->_1 if#(false(),x,y,z) -> c_3(facIter#(x,z)):3
2:S:factorial#(x) -> c_2(facIter#(x,s(0())))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x)):1
3:S:if#(false(),x,y,z) -> c_3(facIter#(x,z))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x))
,isZero#(x)
,minus#(x,s(0()))
,times#(y,x)):1
4:S:minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y))
-->_2 minus#(x,s(y)) -> c_8(p#(minus(x,y)),minus#(x,y)):4
5:S:plus#(s(x),y) -> c_13(plus#(x,y))
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
6:S:times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
-->_2 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x))
minus#(x,s(y)) -> c_8(minus#(x,y))
* Step 6: RemoveHeads MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x))
factorial#(x) -> c_2(facIter#(x,s(0())))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
minus#(x,s(y)) -> c_8(minus#(x,y))
plus#(s(x),y) -> c_13(plus#(x,y))
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak TRS:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/3,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x))
-->_3 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_2 minus#(x,s(y)) -> c_8(minus#(x,y)):4
-->_1 if#(false(),x,y,z) -> c_3(facIter#(x,z)):3
2:S:factorial#(x) -> c_2(facIter#(x,s(0())))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x)):1
3:S:if#(false(),x,y,z) -> c_3(facIter#(x,z))
-->_1 facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x)):1
4:S:minus#(x,s(y)) -> c_8(minus#(x,y))
-->_1 minus#(x,s(y)) -> c_8(minus#(x,y)):4
5:S:plus#(s(x),y) -> c_13(plus#(x,y))
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
6:S:times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
-->_2 times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y)):6
-->_1 plus#(s(x),y) -> c_13(plus#(x,y)):5
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(2,factorial#(x) -> c_2(facIter#(x,s(0()))))]
* Step 7: Failure MAYBE
+ Considered Problem:
- Strict DPs:
facIter#(x,y) -> c_1(if#(isZero(x),minus(x,s(0())),y,times(y,x)),minus#(x,s(0())),times#(y,x))
if#(false(),x,y,z) -> c_3(facIter#(x,z))
minus#(x,s(y)) -> c_8(minus#(x,y))
plus#(s(x),y) -> c_13(plus#(x,y))
times#(s(x),y) -> c_15(plus#(y,times(x,y)),times#(x,y))
- Weak TRS:
isZero(0()) -> true()
isZero(s(x)) -> false()
minus(x,0()) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(0(),x) -> 0()
p(0()) -> 0()
p(s(x)) -> x
plus(0(),x) -> x
plus(s(x),y) -> s(plus(x,y))
times(0(),y) -> 0()
times(s(x),y) -> plus(y,times(x,y))
- Signature:
{facIter/2,factorial/1,if/4,isZero/1,minus/2,p/1,plus/2,times/2,facIter#/2,factorial#/1,if#/4,isZero#/1
,minus#/2,p#/1,plus#/2,times#/2} / {0/0,false/0,s/1,true/0,c_1/3,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1
,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {facIter#,factorial#,if#,isZero#,minus#,p#,plus#
,times#} and constructors {0,false,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE