MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
gcd(0(),N) -> 0()
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
lt(N,M) -> gt(M,N)
p(s(N)) -> N
quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
quot(NzM,NzM) -> u_01(is_NzNat(NzM))
u_01(True()) -> s(0())
u_02(True(),NzM) -> NzM
u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
u_2(True()) -> 0()
u_21(True(),NzM,N) -> u_2(gt(NzM,N))
u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1} / {0/0,False/0,True/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,d,gcd,gt,is_NzNat,lt,p,quot,u_01,u_02,u_1,u_11,u_2
,u_21,u_3,u_31,u_4} and constructors {0,False,True,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
*#(N,0()) -> c_1()
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(N,0()) -> c_3()
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(0(),N) -> c_5()
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gcd#(0(),N) -> c_9()
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(0(),M) -> c_11()
gt#(s(N),s(M)) -> c_12(gt#(N,M))
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
lt#(N,M) -> c_15(gt#(M,N))
p#(s(N)) -> c_16()
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_2#(True()) -> c_24()
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
u_4#(True()) -> c_28()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
*#(N,0()) -> c_1()
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(N,0()) -> c_3()
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(0(),N) -> c_5()
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gcd#(0(),N) -> c_9()
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(0(),M) -> c_11()
gt#(s(N),s(M)) -> c_12(gt#(N,M))
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
lt#(N,M) -> c_15(gt#(M,N))
p#(s(N)) -> c_16()
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_2#(True()) -> c_24()
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
u_4#(True()) -> c_28()
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
gcd(0(),N) -> 0()
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
lt(N,M) -> gt(M,N)
p(s(N)) -> N
quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
quot(NzM,NzM) -> u_01(is_NzNat(NzM))
u_01(True()) -> s(0())
u_02(True(),NzM) -> NzM
u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
u_2(True()) -> 0()
u_21(True(),NzM,N) -> u_2(gt(NzM,N))
u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
*#(N,0()) -> c_1()
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(N,0()) -> c_3()
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(0(),N) -> c_5()
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gcd#(0(),N) -> c_9()
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(0(),M) -> c_11()
gt#(s(N),s(M)) -> c_12(gt#(N,M))
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
lt#(N,M) -> c_15(gt#(M,N))
p#(s(N)) -> c_16()
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_2#(True()) -> c_24()
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
u_4#(True()) -> c_28()
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(N,0()) -> c_1()
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(N,0()) -> c_3()
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(0(),N) -> c_5()
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gcd#(0(),N) -> c_9()
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(0(),M) -> c_11()
gt#(s(N),s(M)) -> c_12(gt#(N,M))
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
lt#(N,M) -> c_15(gt#(M,N))
p#(s(N)) -> c_16()
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_2#(True()) -> c_24()
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
u_4#(True()) -> c_28()
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,3,5,9,11,13,14,16,20,21,24,28}
by application of
Pre({1,3,5,9,11,13,14,16,20,21,24,28}) = {2,4,6,7,8,10,12,15,17,18,19,22,23,25,26,27}.
Here rules are labelled as follows:
1: *#(N,0()) -> c_1()
2: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
3: +#(N,0()) -> c_3()
4: +#(s(N),s(M)) -> c_4(+#(N,M))
5: d#(0(),N) -> c_5()
6: d#(s(N),s(M)) -> c_6(d#(N,M))
7: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
8: gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
9: gcd#(0(),N) -> c_9()
10: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
11: gt#(0(),M) -> c_11()
12: gt#(s(N),s(M)) -> c_12(gt#(N,M))
13: is_NzNat#(0()) -> c_13()
14: is_NzNat#(s(N)) -> c_14()
15: lt#(N,M) -> c_15(gt#(M,N))
16: p#(s(N)) -> c_16()
17: quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
18: quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
19: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
20: u_01#(True()) -> c_20()
21: u_02#(True(),NzM) -> c_21()
22: u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
23: u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
24: u_2#(True()) -> c_24()
25: u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
26: u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
27: u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
28: u_4#(True()) -> c_28()
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
lt#(N,M) -> c_15(gt#(M,N))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak DPs:
*#(N,0()) -> c_1()
+#(N,0()) -> c_3()
d#(0(),N) -> c_5()
gcd#(0(),N) -> c_9()
gt#(0(),M) -> c_11()
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
p#(s(N)) -> c_16()
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_2#(True()) -> c_24()
u_4#(True()) -> c_28()
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{4,6,11}
by application of
Pre({4,6,11}) = {7,8,12,13,14,15,16}.
Here rules are labelled as follows:
1: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
2: +#(s(N),s(M)) -> c_4(+#(N,M))
3: d#(s(N),s(M)) -> c_6(d#(N,M))
4: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
5: gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
6: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
7: gt#(s(N),s(M)) -> c_12(gt#(N,M))
8: lt#(N,M) -> c_15(gt#(M,N))
9: quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
10: quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
11: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
12: u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
13: u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
14: u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
15: u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
16: u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
17: *#(N,0()) -> c_1()
18: +#(N,0()) -> c_3()
19: d#(0(),N) -> c_5()
20: gcd#(0(),N) -> c_9()
21: gt#(0(),M) -> c_11()
22: is_NzNat#(0()) -> c_13()
23: is_NzNat#(s(N)) -> c_14()
24: p#(s(N)) -> c_16()
25: u_01#(True()) -> c_20()
26: u_02#(True(),NzM) -> c_21()
27: u_2#(True()) -> c_24()
28: u_4#(True()) -> c_28()
* Step 5: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
lt#(N,M) -> c_15(gt#(M,N))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak DPs:
*#(N,0()) -> c_1()
+#(N,0()) -> c_3()
d#(0(),N) -> c_5()
gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
gcd#(0(),N) -> c_9()
gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
gt#(0(),M) -> c_11()
is_NzNat#(0()) -> c_13()
is_NzNat#(s(N)) -> c_14()
p#(s(N)) -> c_16()
quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
u_01#(True()) -> c_20()
u_02#(True(),NzM) -> c_21()
u_2#(True()) -> c_24()
u_4#(True()) -> c_28()
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
-->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_2 +#(N,0()) -> c_3():15
-->_1 +#(N,0()) -> c_3():15
-->_3 *#(N,0()) -> c_1():14
-->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1
2:S:+#(s(N),s(M)) -> c_4(+#(N,M))
-->_1 +#(N,0()) -> c_3():15
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
3:S:d#(s(N),s(M)) -> c_6(d#(N,M))
-->_1 d#(0(),N) -> c_5():16
-->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3
4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
-->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13
-->_3 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_3 is_NzNat#(0()) -> c_13():21
-->_2 is_NzNat#(0()) -> c_13():21
5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M))
-->_1 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19
-->_1 gt#(0(),M) -> c_11():20
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
6:S:lt#(N,M) -> c_15(gt#(M,N))
-->_1 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19
-->_1 gt#(0(),M) -> c_11():20
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
-->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(0()) -> c_13():21
8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
-->_1 u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)):11
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(0()) -> c_13():21
9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
-->_1 quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)):24
-->_2 d#(0(),N) -> c_5():16
-->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)):8
-->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)):7
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
-->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19
-->_2 gt#(0(),M) -> c_11():20
-->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
11:S:u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
-->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19
-->_1 u_2#(True()) -> c_24():27
-->_2 gt#(0(),M) -> c_11():20
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
-->_1 gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)):17
-->_1 gcd#(0(),N) -> c_9():18
-->_2 d#(0(),N) -> c_5():16
-->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)):4
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
-->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19
-->_2 gt#(0(),M) -> c_11():20
-->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
14:W:*#(N,0()) -> c_1()
15:W:+#(N,0()) -> c_3()
16:W:d#(0(),N) -> c_5()
17:W:gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
-->_1 u_02#(True(),NzM) -> c_21():26
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(0()) -> c_13():21
18:W:gcd#(0(),N) -> c_9()
19:W:gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
-->_1 u_4#(True()) -> c_28():28
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(0()) -> c_13():21
20:W:gt#(0(),M) -> c_11()
21:W:is_NzNat#(0()) -> c_13()
22:W:is_NzNat#(s(N)) -> c_14()
23:W:p#(s(N)) -> c_16()
24:W:quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
-->_1 u_01#(True()) -> c_20():25
-->_2 is_NzNat#(s(N)) -> c_14():22
-->_2 is_NzNat#(0()) -> c_13():21
25:W:u_01#(True()) -> c_20()
26:W:u_02#(True(),NzM) -> c_21()
27:W:u_2#(True()) -> c_24()
28:W:u_4#(True()) -> c_28()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
23: p#(s(N)) -> c_16()
27: u_2#(True()) -> c_24()
24: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM))
25: u_01#(True()) -> c_20()
18: gcd#(0(),N) -> c_9()
17: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM))
26: u_02#(True(),NzM) -> c_21()
20: gt#(0(),M) -> c_11()
19: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN))
21: is_NzNat#(0()) -> c_13()
22: is_NzNat#(s(N)) -> c_14()
28: u_4#(True()) -> c_28()
16: d#(0(),N) -> c_5()
14: *#(N,0()) -> c_1()
15: +#(N,0()) -> c_3()
* Step 6: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
lt#(N,M) -> c_15(gt#(M,N))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
-->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1
2:S:+#(s(N),s(M)) -> c_4(+#(N,M))
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
3:S:d#(s(N),s(M)) -> c_6(d#(N,M))
-->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3
4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM))
-->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13
5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M))
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
6:S:lt#(N,M) -> c_15(gt#(M,N))
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM))
-->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10
8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM))
-->_1 u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)):11
9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
-->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)):8
-->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)):7
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
-->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
11:S:u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N))
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
-->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)):4
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
-->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
* Step 7: RemoveHeads MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
lt#(N,M) -> c_15(gt#(M,N))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
-->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
-->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1
2:S:+#(s(N),s(M)) -> c_4(+#(N,M))
-->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2
3:S:d#(s(N),s(M)) -> c_6(d#(N,M))
-->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3
4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
-->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13
5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M))
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
6:S:lt#(N,M) -> c_15(gt#(M,N))
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
-->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10
8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
-->_1 u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)):11
9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
-->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)):8
-->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)):7
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
-->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
11:S:u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
-->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5
12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
-->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)):4
-->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3
13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
-->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12
-->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):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).
[(6,lt#(N,M) -> c_15(gt#(M,N)))]
* Step 8: NaturalMI MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_2) = {1,2,3},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_12) = {1},
uargs(c_17) = {1},
uargs(c_18) = {1},
uargs(c_22) = {1,2},
uargs(c_23) = {1,2},
uargs(c_25) = {1},
uargs(c_26) = {1,2},
uargs(c_27) = {1,2}
Following symbols are considered usable:
{is_NzNat,*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#}
TcT has computed the following interpretation:
p(*) = [4] x2 + [6]
p(+) = [2] x1 + [1] x2 + [0]
p(0) = [1]
p(False) = [0]
p(True) = [1]
p(d) = [0]
p(gcd) = [1] x1 + [0]
p(gt) = [0]
p(is_NzNat) = [1]
p(lt) = [4] x2 + [0]
p(p) = [0]
p(quot) = [1]
p(s) = [0]
p(u_01) = [4] x1 + [4]
p(u_02) = [4] x1 + [1] x2 + [0]
p(u_1) = [1] x2 + [1] x3 + [2]
p(u_11) = [4] x3 + [2]
p(u_2) = [2] x1 + [1]
p(u_21) = [2] x2 + [0]
p(u_3) = [1] x1 + [1] x2 + [1] x3 + [2]
p(u_31) = [2] x1 + [1] x4 + [0]
p(u_4) = [6] x1 + [6]
p(*#) = [0]
p(+#) = [0]
p(d#) = [0]
p(gcd#) = [0]
p(gt#) = [0]
p(is_NzNat#) = [0]
p(lt#) = [1] x1 + [2]
p(p#) = [0]
p(quot#) = [4] x2 + [4]
p(u_01#) = [1]
p(u_02#) = [4] x1 + [4]
p(u_1#) = [4] x3 + [4]
p(u_11#) = [3] x1 + [4] x3 + [1]
p(u_2#) = [0]
p(u_21#) = [4] x1 + [0]
p(u_3#) = [0]
p(u_31#) = [0]
p(u_4#) = [4]
p(c_1) = [1]
p(c_2) = [2] x1 + [4] x2 + [4] x3 + [0]
p(c_3) = [4]
p(c_4) = [4] x1 + [0]
p(c_5) = [0]
p(c_6) = [4] x1 + [0]
p(c_7) = [1] x1 + [1]
p(c_8) = [2] x1 + [0]
p(c_9) = [2]
p(c_10) = [4] x2 + [1]
p(c_11) = [1]
p(c_12) = [4] x1 + [0]
p(c_13) = [0]
p(c_14) = [1]
p(c_15) = [0]
p(c_16) = [4]
p(c_17) = [1] x1 + [0]
p(c_18) = [1] x1 + [0]
p(c_19) = [2]
p(c_20) = [1]
p(c_21) = [0]
p(c_22) = [1] x1 + [2] x2 + [0]
p(c_23) = [1] x1 + [2] x2 + [0]
p(c_24) = [4]
p(c_25) = [2] x1 + [0]
p(c_26) = [2] x1 + [2] x2 + [0]
p(c_27) = [4] x1 + [4] x2 + [0]
p(c_28) = [0]
Following rules are strictly oriented:
u_21#(True(),NzM,N) = [4]
> [0]
= c_25(gt#(NzM,N))
Following rules are (at-least) weakly oriented:
*#(s(N),s(M)) = [0]
>= [0]
= c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) = [0]
>= [0]
= c_4(+#(N,M))
d#(s(N),s(M)) = [0]
>= [0]
= c_6(d#(N,M))
gcd#(NzN,NzM) = [0]
>= [0]
= c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) = [0]
>= [0]
= c_12(gt#(N,M))
quot#(N,NzM) = [4] NzM + [4]
>= [4] NzM + [4]
= c_17(u_11#(is_NzNat(NzM),N,NzM))
quot#(N,NzM) = [4] NzM + [4]
>= [4]
= c_18(u_21#(is_NzNat(NzM),NzM,N))
u_1#(True(),N,NzM) = [4] NzM + [4]
>= [4] NzM + [4]
= c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) = [4] NzM + [4]
>= [4] NzM + [4]
= c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_3#(True(),NzN,NzM) = [0]
>= [0]
= c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) = [0]
>= [0]
= c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
is_NzNat(0()) = [1]
>= [0]
= False()
is_NzNat(s(N)) = [1]
>= [1]
= True()
* Step 9: NaturalMI MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak DPs:
u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_2) = {1,2,3},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1},
uargs(c_12) = {1},
uargs(c_17) = {1},
uargs(c_18) = {1},
uargs(c_22) = {1,2},
uargs(c_23) = {1,2},
uargs(c_25) = {1},
uargs(c_26) = {1,2},
uargs(c_27) = {1,2}
Following symbols are considered usable:
{gt,u_4,*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#}
TcT has computed the following interpretation:
p(*) = [1] x1 + [1] x2 + [0]
p(+) = [0]
p(0) = [0]
p(False) = [0]
p(True) = [1]
p(d) = [4] x1 + [0]
p(gcd) = [4] x1 + [1]
p(gt) = [1]
p(is_NzNat) = [0]
p(lt) = [2] x1 + [1]
p(p) = [1]
p(quot) = [4] x1 + [1]
p(s) = [0]
p(u_01) = [0]
p(u_02) = [2]
p(u_1) = [1] x1 + [1]
p(u_11) = [1] x1 + [1]
p(u_2) = [1] x1 + [1]
p(u_21) = [1]
p(u_3) = [4] x2 + [2] x3 + [0]
p(u_31) = [2] x1 + [1] x3 + [2]
p(u_4) = [1]
p(*#) = [0]
p(+#) = [0]
p(d#) = [0]
p(gcd#) = [0]
p(gt#) = [0]
p(is_NzNat#) = [1]
p(lt#) = [1] x1 + [1] x2 + [2]
p(p#) = [4]
p(quot#) = [4]
p(u_01#) = [1]
p(u_02#) = [0]
p(u_1#) = [4] x1 + [0]
p(u_11#) = [4]
p(u_2#) = [1]
p(u_21#) = [0]
p(u_3#) = [0]
p(u_31#) = [0]
p(u_4#) = [1]
p(c_1) = [0]
p(c_2) = [2] x1 + [1] x2 + [1] x3 + [0]
p(c_3) = [1]
p(c_4) = [4] x1 + [0]
p(c_5) = [4]
p(c_6) = [4] x1 + [0]
p(c_7) = [0]
p(c_8) = [2] x1 + [0]
p(c_9) = [4]
p(c_10) = [4] x1 + [0]
p(c_11) = [1]
p(c_12) = [4] x1 + [0]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [4] x1 + [4]
p(c_16) = [0]
p(c_17) = [1] x1 + [0]
p(c_18) = [4] x1 + [2]
p(c_19) = [1] x1 + [1] x2 + [0]
p(c_20) = [1]
p(c_21) = [0]
p(c_22) = [1] x1 + [4] x2 + [0]
p(c_23) = [1] x1 + [4] x2 + [0]
p(c_24) = [1]
p(c_25) = [4] x1 + [0]
p(c_26) = [2] x1 + [1] x2 + [0]
p(c_27) = [2] x1 + [4] x2 + [0]
p(c_28) = [0]
Following rules are strictly oriented:
quot#(N,NzM) = [4]
> [2]
= c_18(u_21#(is_NzNat(NzM),NzM,N))
Following rules are (at-least) weakly oriented:
*#(s(N),s(M)) = [0]
>= [0]
= c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) = [0]
>= [0]
= c_4(+#(N,M))
d#(s(N),s(M)) = [0]
>= [0]
= c_6(d#(N,M))
gcd#(NzN,NzM) = [0]
>= [0]
= c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) = [0]
>= [0]
= c_12(gt#(N,M))
quot#(N,NzM) = [4]
>= [4]
= c_17(u_11#(is_NzNat(NzM),N,NzM))
u_1#(True(),N,NzM) = [4]
>= [4]
= c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) = [4]
>= [4]
= c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_21#(True(),NzM,N) = [0]
>= [0]
= c_25(gt#(NzM,N))
u_3#(True(),NzN,NzM) = [0]
>= [0]
= c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) = [0]
>= [0]
= c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
gt(NzN,0()) = [1]
>= [1]
= u_4(is_NzNat(NzN))
gt(0(),M) = [1]
>= [0]
= False()
gt(s(N),s(M)) = [1]
>= [1]
= gt(N,M)
u_4(True()) = [1]
>= [1]
= True()
* Step 10: Failure MAYBE
+ Considered Problem:
- Strict DPs:
*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M))
+#(s(N),s(M)) -> c_4(+#(N,M))
d#(s(N),s(M)) -> c_6(d#(N,M))
gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM))
gt#(s(N),s(M)) -> c_12(gt#(N,M))
quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM))
u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM))
u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM))
u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM))
u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM))
- Weak DPs:
quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N))
u_21#(True(),NzM,N) -> c_25(gt#(NzM,N))
- Weak TRS:
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
gt(NzN,0()) -> u_4(is_NzNat(NzN))
gt(0(),M) -> False()
gt(s(N),s(M)) -> gt(N,M)
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
u_4(True()) -> True()
- Signature:
{*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4
,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1
,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1
,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2
,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#
,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE