YES Problem: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Proof: DP Processor: DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) rec[sum_0][1]#(Cons(x5,x3)) -> rec[plus_0][2]#(x5,rec[sum_0][1](x3)) rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) rec[mult_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) main#(S(x1)) -> rec[unfoldr_0][2]#(S(x1)) main#(S(x1)) -> rec[map_0][2]#(Cons(S(x1),rec[unfoldr_0][2](S(x1)))) main#(S(x1)) -> rec[sum_0][1]#(rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) TDG Processor: DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) rec[sum_0][1]#(Cons(x5,x3)) -> rec[plus_0][2]#(x5,rec[sum_0][1](x3)) rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) rec[mult_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) main#(S(x1)) -> rec[unfoldr_0][2]#(S(x1)) main#(S(x1)) -> rec[map_0][2]#(Cons(S(x1),rec[unfoldr_0][2](S(x1)))) main#(S(x1)) -> rec[sum_0][1]#(rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) graph: main#(S(x1)) -> rec[unfoldr_0][2]#(S(x1)) -> rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) main#(S(x1)) -> rec[map_0][2]#(Cons(S(x1),rec[unfoldr_0][2](S(x1)))) -> rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) main#(S(x1)) -> rec[map_0][2]#(Cons(S(x1),rec[unfoldr_0][2](S(x1)))) -> rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) main#(S(x1)) -> rec[sum_0][1]#(rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) -> rec[sum_0][1]#(Cons(x5,x3)) -> rec[plus_0][2]#(x5,rec[sum_0][1](x3)) main#(S(x1)) -> rec[sum_0][1]#(rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) -> rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) -> rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) -> rec[mult_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x6,rec[mult_0][2](x10,x6)) rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) -> rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) rec[mult_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x6,rec[mult_0][2](x10,x6)) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) -> rec[mult_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x6,rec[mult_0][2](x10,x6)) rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) -> rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) -> rec[map_0][2]#(Cons(x6,x13)) -> rec[mult_0][2]#(x6,x6) rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) -> rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) -> rec[sum_0][1]#(Cons(x5,x3)) -> rec[plus_0][2]#(x5,rec[sum_0][1](x3)) rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) -> rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) rec[sum_0][1]#(Cons(x5,x3)) -> rec[plus_0][2]#(x5,rec[sum_0][1](x3)) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) SCC Processor: #sccs: 5 #rules: 5 #arcs: 17/121 DPs: rec[sum_0][1]#(Cons(x5,x3)) -> rec[sum_0][1]#(x3) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Subterm Criterion Processor: simple projection: pi(rec[sum_0][1]#) = 0 problem: DPs: TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Qed DPs: rec[map_0][2]#(Cons(x6,x13)) -> rec[map_0][2]#(x13) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Subterm Criterion Processor: simple projection: pi(rec[map_0][2]#) = 0 problem: DPs: TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Qed DPs: rec[mult_0][2]#(S(x10),x6) -> rec[mult_0][2]#(x10,x6) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Subterm Criterion Processor: simple projection: pi(rec[mult_0][2]#) = 0 problem: DPs: TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Qed DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Subterm Criterion Processor: simple projection: pi(rec[plus_0][2]#) = 0 problem: DPs: TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Qed DPs: rec[unfoldr_0][2]#(S(x6)) -> rec[unfoldr_0][2]#(x6) TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Subterm Criterion Processor: simple projection: pi(rec[unfoldr_0][2]#) = 0 problem: DPs: TRS: rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) rec[sum_0][1](Nil()) -> 0() rec[sum_0][1](Cons(x5,x3)) -> rec[plus_0][2](x5,rec[sum_0][1](x3)) rec[map_0][2](Nil()) -> Nil() rec[map_0][2](Cons(x6,x13)) -> Cons(rec[mult_0][2](x6,x6),rec[map_0][2](x13)) rec[mult_0][2](0(),x34) -> 0() rec[mult_0][2](S(x10),x6) -> rec[plus_0][2](x6,rec[mult_0][2](x10,x6)) rec[unfoldr_0][2](0()) -> Nil() rec[unfoldr_0][2](S(x6)) -> Cons(x6,rec[unfoldr_0][2](x6)) main(0()) -> 0() main(S(x1)) -> rec[sum_0][1](rec[map_0][2](Cons(S(x1),rec[unfoldr_0][2](S(x1))))) Qed