YES Problem: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Proof: DP Processor: DPs: rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[drop_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[length_0][1]#(x1) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[halve_0][1]#(rec[length_0][1](x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[take_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> const_f[2]#(Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) const_f[2]#(Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2]#(x3,x2) merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main#(x43) -> rec[dc_0][1]#(x43) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) TDG Processor: DPs: rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[drop_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[length_0][1]#(x1) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[halve_0][1]#(rec[length_0][1](x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[take_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> const_f[2]#(Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) const_f[2]#(Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2]#(x3,x2) merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main#(x43) -> rec[dc_0][1]#(x43) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) graph: main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> const_f[2]#(Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[take_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[halve_0][1]#(rec[length_0][1](x1)) main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[length_0][1]#(x1) main#(x43) -> rec[dc_0][1]#(x43) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[drop_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) -> rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) -> rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) -> merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) -> merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) const_f[2]#(Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2]#(x3,x2) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) const_f[2]#(Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2]#(x3,x2) -> rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> rec[leq_0][2]#(x18,x10) rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) -> rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) -> rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) -> rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) -> rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> const_f[2]#(Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) -> const_f[2]#(Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2]#(x3,x2) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[take_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) -> rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[halve_0][1]#(rec[length_0][1](x1)) -> rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[length_0][1]#(x1) -> rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[drop_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) -> rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) -> rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) -> rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> const_f[2]#(Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[take_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[halve_0][1]#(rec[length_0][1](x1)) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[length_0][1]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) -> rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[drop_0][2]#(rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) -> rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) -> rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) SCC Processor: #sccs: 7 #rules: 11 #arcs: 35/361 DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),Cons(x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Usable Rule Processor: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))),ConsL (rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) TRS: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) Arctic Interpretation Processor: dimension: 1 usable rules: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) interpretation: [rec[dc_0][1]#](x0) = x0 + 5, [rec[mapL_0][2]#](x0) = x0 + 0, [Tail_error_empty_list] = 0, [Head_error_empty_list] = 6, [S](x0) = 1x0 + 4, [0] = 0, [rec[drop_0][2]](x0, x1) = x1 + 0, [rec[take_0][2]](x0, x1) = 1x0, [rec[halve_0][1]](x0) = x0, [rec[length_0][1]](x0) = x0, [Cons](x0, x1) = 1x1 + 5, [Nil] = 0, [ConsL](x0, x1) = x0 + 1x1 + 5, [NilL] = 3 orientation: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) = 2x1 + 6 >= 2x1 + 6 = rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1] (x1)),Cons (x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1] (x1)),Cons(x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) = 1x1 + x2 + 5 >= x1 + 0 = rec[mapL_0][2]#(x1) rec[mapL_0][2]#(ConsL(x2,x1)) = 1x1 + x2 + 5 >= x2 + 5 = rec[dc_0][1]#(x2) rec[drop_0][2](0(),x26) = x26 + 0 >= x26 = x26 rec[drop_0][2](S(x14),Cons(x10,x6)) = 1x6 + 5 >= x6 + 0 = rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) = 0 >= 0 = 0() rec[length_0][1](Cons(x13,x17)) = 1x17 + 5 >= 1x17 + 4 = S(rec[length_0][1](x17)) rec[halve_0][1](0()) = 0 >= 0 = 0() rec[halve_0][1](S(0())) = 4 >= 4 = S(0()) rec[halve_0][1](S(S(x17))) = 2x17 + 5 >= 1x17 + 4 = S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) = 0 >= 0 = Tail_error_empty_list() rec[take_0][2](0(),x26) = 1 >= 0 = Nil() rec[take_0][2](S(x14),Cons(x10,x6)) = 2x14 + 5 >= 2x14 + 5 = Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) = 5 >= 5 = Cons(Head_error_empty_list(),Nil()) problem: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))),ConsL (rec[drop_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) TRS: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) Restore Modifier: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))),ConsL (rec[drop_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3, rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Usable Rule Processor: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))),ConsL ( rec[drop_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) -> rec[dc_0][1]#(x2) TRS: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) Arctic Interpretation Processor: dimension: 1 usable rules: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) interpretation: [rec[dc_0][1]#](x0) = 3x0 + 0, [rec[mapL_0][2]#](x0) = 4x0 + 0, [Tail_error_empty_list] = 0, [Head_error_empty_list] = 4, [S](x0) = 1x0 + 0, [0] = 0, [rec[drop_0][2]](x0, x1) = x1 + 0, [rec[take_0][2]](x0, x1) = x0, [rec[halve_0][1]](x0) = x0, [rec[length_0][1]](x0) = x0, [Cons](x0, x1) = 1x1 + 0, [Nil] = 0, [ConsL](x0, x1) = x0 + x1 + 0, [NilL] = 0 orientation: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) = 5x1 + 4 >= 5x1 + 4 = rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1] (x1)),Cons (x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1] (x1)),Cons(x2,x1)), NilL()))) rec[mapL_0][2]#(ConsL(x2,x1)) = 4x1 + 4x2 + 4 >= 3x2 + 0 = rec[dc_0][1]#(x2) rec[drop_0][2](0(),x26) = x26 + 0 >= x26 = x26 rec[drop_0][2](S(x14),Cons(x10,x6)) = 1x6 + 0 >= x6 + 0 = rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) = 0 >= 0 = 0() rec[length_0][1](Cons(x13,x17)) = 1x17 + 0 >= 1x17 + 0 = S(rec[length_0][1](x17)) rec[halve_0][1](0()) = 0 >= 0 = 0() rec[halve_0][1](S(0())) = 1 >= 1 = S(0()) rec[halve_0][1](S(S(x17))) = 2x17 + 1 >= 1x17 + 0 = S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) = 0 >= 0 = Tail_error_empty_list() rec[take_0][2](0(),x26) = 0 >= 0 = Nil() rec[take_0][2](S(x14),Cons(x10,x6)) = 1x14 + 0 >= 1x14 + 0 = Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) = 1 >= 1 = Cons(Head_error_empty_list(),Nil()) problem: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1)),NilL()))) TRS: rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) Restore Modifier: DPs: rec[dc_0][1]#(Cons(x3,Cons(x2,x1))) -> rec[mapL_0][2]#(ConsL(Cons(x3,rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1))), ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)), Cons(x2,x1)),NilL()))) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons( x3, rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL (rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/1 DPs: rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Size-Change Termination Processor: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) The DP: rec[merge_0][2]#(Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2#(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) has the edges: 0 > 4 0 > 3 0 >= 1 1 > 6 1 > 5 1 >= 2 The DP: merge_cond_2#(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(x7,Cons(x11,x13)) has the edges: 2 >= 1 4 >= 0 The DP: merge_cond_2#(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> rec[merge_0][2]#(Cons(x15,x17),x3) has the edges: 1 >= 0 6 >= 1 Qed DPs: rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Subterm Criterion Processor: simple projection: pi(rec[leq_0][2]#) = 0 problem: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Qed DPs: rec[take_0][2]#(S(x14),Cons(x10,x6)) -> rec[take_0][2]#(x14,x6) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Subterm Criterion Processor: simple projection: pi(rec[take_0][2]#) = 0 problem: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Qed DPs: rec[halve_0][1]#(S(S(x17))) -> rec[halve_0][1]#(x17) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Subterm Criterion Processor: simple projection: pi(rec[halve_0][1]#) = 0 problem: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Qed DPs: rec[length_0][1]#(Cons(x13,x17)) -> rec[length_0][1]#(x17) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Subterm Criterion Processor: simple projection: pi(rec[length_0][1]#) = 0 problem: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Qed DPs: rec[drop_0][2]#(S(x14),Cons(x10,x6)) -> rec[drop_0][2]#(x14,x6) TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons(x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Subterm Criterion Processor: simple projection: pi(rec[drop_0][2]#) = 0 problem: DPs: TRS: rec[mapL_0][2](NilL()) -> NilL() rec[mapL_0][2](ConsL(x2,x1)) -> ConsL(rec[dc_0][1](x2),rec[mapL_0][2](x1)) rec[dc_0][1](Nil()) -> Nil() rec[dc_0][1](Cons(x77,Nil())) -> Cons(x77,Nil()) rec[dc_0][1](Cons(x3,Cons(x2,x1))) -> const_f[2](Cons(x3,Cons(x2,x1)),rec[mapL_0][2](ConsL(Cons(x3,rec[take_0][2] ( rec[halve_0][1] ( rec[length_0][1](x1)), Cons (x2,x1))), ConsL(rec[drop_0][2] (rec[halve_0][1] (rec[length_0][1](x1)), Cons (x2,x1)), NilL())))) rec[take_0][2](0(),x26) -> Nil() rec[take_0][2](S(0()),Nil()) -> Cons(Head_error_empty_list(),Nil()) rec[take_0][2](S(x14),Cons(x10,x6)) -> Cons(x10,rec[take_0][2](x14,x6)) rec[halve_0][1](0()) -> 0() rec[halve_0][1](S(0())) -> S(0()) rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17)) rec[length_0][1](Nil()) -> 0() rec[length_0][1](Cons(x13,x17)) -> S(rec[length_0][1](x17)) rec[drop_0][2](0(),x26) -> x26 rec[drop_0][2](S(0()),Nil()) -> Tail_error_empty_list() rec[drop_0][2](S(x14),Cons(x10,x6)) -> rec[drop_0][2](x14,x6) const_f[2](Cons(x4,Cons(x5,x6)),ConsL(x3,ConsL(x2,x1))) -> rec[merge_0][2](x3,x2) merge_cond_2(True(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x9,rec[merge_0][2](x7,Cons(x11,x13))) merge_cond_2(False(),Cons(x15,x17),Cons(x11,x13),x9,x7,x5,x3) -> Cons(x5,rec[merge_0][2](Cons(x15,x17),x3)) rec[leq_0][2](0(),x106) -> True() rec[leq_0][2](S(x114),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) rec[merge_0][2](Nil(),x58) -> x58 rec[merge_0][2](Cons(x66,x74),Nil()) -> Cons(x66,x74) rec[merge_0][2](Cons(x18,x14),Cons(x10,x6)) -> merge_cond_2(rec[leq_0][2](x18,x10),Cons(x18,x14),Cons(x10,x6),x18,x14,x10,x6) main(x43) -> rec[dc_0][1](x43) Qed