MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
cond_take_l_n_xs(ConsL(x16,x18),0()) -> Nil()
cond_take_l_n_xs(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4
,x8
,x12
,bot[0]())
,x16))
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main(x12) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4} / {0/0,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0
,fibs_2/3,plus/0,tail_l/0,zipwith_l/0,zipwith_l_f_xs_ys/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs,cond_zipwith_l_f_xs_ys
,cond_zipwith_l_f_xs_ys_1,fibs_2#1,main,plus#2,zipwith_l#3,zipwith_l_f_xs_ys#1} and constructors {0,Cons
,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(0(),x12) -> c_9()
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l#3#(x8,x4) -> c_11()
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(0(),x12) -> c_9()
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l#3#(x8,x4) -> c_11()
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak TRS:
cond_take_l_n_xs(ConsL(x16,x18),0()) -> Nil()
cond_take_l_n_xs(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4
,x8
,x12
,bot[0]())
,x16))
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main(x12) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l(),plus(),tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(0(),x12) -> c_9()
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l#3#(x8,x4) -> c_11()
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(0(),x12) -> c_9()
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l#3#(x8,x4) -> c_11()
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,9,11}
by application of
Pre({1,9,11}) = {2,3,6,7,8,10}.
Here rules are labelled as follows:
1: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
2: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
3: cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
4: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
5: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
6: cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
7: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l(),plus(),tail_l())))
8: main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
9: plus#2#(0(),x12) -> c_9()
10: plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
11: zipwith_l#3#(x8,x4) -> c_11()
12: zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
13: zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
14: zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak DPs:
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
plus#2#(0(),x12) -> c_9()
zipwith_l#3#(x8,x4) -> c_11()
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{6}
by application of
Pre({6}) = {1,3,10}.
Here rules are labelled as follows:
1: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
2: cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
3: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
4: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
5: cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
6: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l(),plus(),tail_l())))
7: main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
8: plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
9: zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
10: zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
11: zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
12: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
13: plus#2#(0(),x12) -> c_9()
14: zipwith_l#3#(x8,x4) -> c_11()
* Step 5: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak DPs:
cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2#(0(),x12) -> c_9()
zipwith_l#3#(x8,x4) -> c_11()
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
-->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l()
,plus()
,tail_l()))):12
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
-->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l()
,plus()
,tail_l()))):12
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5
4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5
5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
-->_2 zipwith_l#3#(x8,x4) -> c_11():14
-->_1 plus#2#(0(),x12) -> c_9():13
6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
-->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
-->_1 plus#2#(0(),x12) -> c_9():13
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
-->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l()
,plus()
,tail_l()))):12
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
11:W:cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
12:W:fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l(),plus(),tail_l())))
-->_1 zipwith_l#3#(x8,x4) -> c_11():14
13:W:plus#2#(0(),x12) -> c_9()
14:W:zipwith_l#3#(x8,x4) -> c_11()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
11: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1()
13: plus#2#(0(),x12) -> c_9()
12: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs()
,fibs_2(zipwith_l(),plus(),tail_l())))
14: zipwith_l#3#(x8,x4) -> c_11()
* Step 6: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]()))
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]()))
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5
4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5
5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3))
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)
,fibs_2#1#(x4,x8,x12,bot[0]())):1
7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]()))
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)
,fibs_2#1#(x3,x4,x5,bot[7]())):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
,fibs_2#1#(x1,x2,x3,bot[6]())):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2))
* Step 7: RemoveHeads MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4))
main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16))
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)):1
2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16)
,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)):1
3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4))
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)):5
4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)):5
5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4))
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12))
-->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4
,x8
,x12
,bot[0]())
,x16)):1
7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
-->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7
8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)):3
9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2))
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)):3
10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
-->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2)):9
-->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)):8
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4
-->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)):3
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,main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)))]
* Step 8: Failure MAYBE
+ Considered Problem:
- Strict DPs:
cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) ->
c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]()))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4))
cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]()))
cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4))
plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2))
zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5))
zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3
,x4
,x5
,bot[7]())
,x2))
zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]()))
- Weak TRS:
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l(),plus(),tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4,cond_take_l_n_xs#/2,cond_zipwith_l_f_xs_ys#/2
,cond_zipwith_l_f_xs_ys_1#/3,fibs_2#1#/4,main#/1,plus#2#/2,zipwith_l#3#/2,zipwith_l_f_xs_ys#1#/4} / {0/0
,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0,fibs_2/3,plus/0,tail_l/0,zipwith_l/0
,zipwith_l_f_xs_ys/3,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1
,c_14/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs#,cond_zipwith_l_f_xs_ys#
,cond_zipwith_l_f_xs_ys_1#,fibs_2#1#,main#,plus#2#,zipwith_l#3#,zipwith_l_f_xs_ys#1#} and constructors {0
,Cons,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE