YES Problem: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Proof: DP Processor: DPs: rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) insert_ord[2]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) main#(x7) -> rec[fold_0][3]#(x7) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) TDG Processor: DPs: rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) insert_ord[2]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) main#(x7) -> rec[fold_0][3]#(x7) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) graph: main#(x7) -> rec[fold_0][3]#(x7) -> rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) main#(x7) -> rec[fold_0][3]#(x7) -> rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(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) insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) -> insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) -> insert_ord[2]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) insert_ord[2]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) -> rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) -> insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) -> insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) -> insert_ord[2]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) -> rec[fold_0][3]#(Cons(x2,x1)) -> insert_ord[2]#(x2,rec[fold_0][3](x1)) rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) -> rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) SCC Processor: #sccs: 3 #rules: 4 #arcs: 11/49 DPs: rec[fold_0][3]#(Cons(x2,x1)) -> rec[fold_0][3]#(x1) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Subterm Criterion Processor: simple projection: pi(rec[fold_0][3]#) = 0 problem: DPs: TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Qed DPs: insert_ord[2]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Subterm Criterion Processor: simple projection: pi(insert_ord[2]#) = 1 pi(insert_cond_1#) = 3 problem: DPs: insert_cond_1#(False(),x4,x11,x8) -> insert_ord[2]#(x4,x8) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1 DPs: rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Subterm Criterion Processor: simple projection: pi(rec[leq_0][2]#) = 0 problem: DPs: TRS: rec[fold_0][3](Nil()) -> Nil() rec[fold_0][3](Cons(x2,x1)) -> insert_ord[2](x2,rec[fold_0][3](x1)) insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3)) insert_cond_1(False(),x4,x11,x8) -> Cons(x11,insert_ord[2](x4,x8)) insert_ord[2](x6,Nil()) -> Cons(x6,Nil()) insert_ord[2](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6) rec[leq_0][2](0(),x18) -> True() rec[leq_0][2](S(x26),0()) -> False() rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6) main(x7) -> rec[fold_0][3](x7) Qed