YES Problem: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Proof: DP Processor: DPs: rec[x_0][1]#(f(x10),x7) -> rec[rpm_0][3]#(x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x5,f_0(rec[x_0](f(x7))),bot[4]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x6,f_0(rec[x_0](f(x7))),bot[2]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x2,f_0(rec[x_0](f(x4))),bot[8]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x3,f_0(rec[x_0](f(x4))),bot[6]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main#(x3) -> rec[x_0][1]#(f(x3),bot[12]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) TDG Processor: DPs: rec[x_0][1]#(f(x10),x7) -> rec[rpm_0][3]#(x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x5,f_0(rec[x_0](f(x7))),bot[4]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x6,f_0(rec[x_0](f(x7))),bot[2]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x2,f_0(rec[x_0](f(x4))),bot[8]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x3,f_0(rec[x_0](f(x4))),bot[6]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main#(x3) -> rec[x_0][1]#(f(x3),bot[12]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) graph: main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x6,f_0(rec[x_0](f(x7))),bot[2]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x5,f_0(rec[x_0](f(x7))),bot[4]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) main#(x3) -> fst_cond[1]#(rec[x_0][1](f(x3),bot[12]()),bot[13]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) main#(x3) -> rec[x_0][1]#(f(x3),bot[12]()) -> rec[x_0][1]#(f(x10),x7) -> rec[rpm_0][3]#(x10,f_0(rec[x_0](f(x10))),bot[0]()) rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) -> rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) -> rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x3,f_0(rec[x_0](f(x4))),bot[6]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x2,f_0(rec[x_0](f(x4))),bot[8]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x3,f_0(rec[x_0](f(x4))),bot[6]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x2,f_0(rec[x_0](f(x4))),bot[8]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x6,f_0(rec[x_0](f(x7))),bot[2]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x5,f_0(rec[x_0](f(x7))),bot[4]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x6,f_0(rec[x_0](f(x7))),bot[2]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x5,f_0(rec[x_0](f(x7))),bot[4]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) -> fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2]#(snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x3,f_0(rec[x_0](f(x4))),bot[6]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> snd_cond[1]#(rec[x_0][1](f(x3),bot[10]()),bot[11]()) -> snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[rpm_0][3]#(x2,f_0(rec[x_0](f(x4))),bot[8]()) fst_cond[1]#(P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> rec[x_0][1]#(f(x3),bot[10]()) -> rec[x_0][1]#(f(x10),x7) -> rec[rpm_0][3]#(x10,f_0(rec[x_0](f(x10))),bot[0]()) SCC Processor: #sccs: 3 #rules: 5 #arcs: 37/225 DPs: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Usable Rule Processor: DPs: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Arctic Interpretation Processor: dimension: 1 usable rules: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) interpretation: [fst_cond[1]#](x0, x1) = x0, [Node](x0, x1) = 5x0 + x1 + 0, [bot[5]] = 5, [bot[4]] = 0, [bot[3]] = 3, [bot[2]] = 4, [rpm_9](x0, x1, x2) = 2x0 + 2x1 + 1x2 + 0, [rpm_8](x0, x1, x2) = 5x1 + x2, [Leaf](x0) = 4x0 + 4, [P](x0, x1) = x0, [rpm_4](x0) = x0 + 4, [rpm_3](x0) = 4x0 + 0, [rec[rpm_0][3]](x0, x1, x2) = x0, [f_0](x0) = 0, [rec[x_0]](x0) = x0 + 0, [f](x0) = x0 + 0 orientation: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))), x3,x2)),x1) = x5 + 5x6 >= x5 = fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))), x3,x2)),x1) = x5 + 5x6 >= x6 = fst_cond[1]#(rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) = 4x3 + 4 >= 4 = P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) = x3 + 5x4 + 0 >= x3 + 5x4 = P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) problem: DPs: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Restore Modifier: DPs: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Usable Rule Processor: DPs: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Arctic Interpretation Processor: dimension: 1 usable rules: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) interpretation: [fst_cond[1]#](x0, x1) = 2x0 + 1x1 + 0, [Node](x0, x1) = 3x0 + 5x1 + 4, [bot[5]] = 0, [bot[4]] = 1, [rpm_9](x0, x1, x2) = 4x0 + 3x1 + 5x2 + 0, [rpm_8](x0, x1, x2) = x1 + 4x2 + 0, [Leaf](x0) = 2x0 + 6, [P](x0, x1) = x0 + x1 + 0, [rpm_4](x0) = x0 + 5, [rpm_3](x0) = x0 + 0, [rec[rpm_0][3]](x0, x1, x2) = x0 + 1x2, [f_0](x0) = x0 + 0, [rec[x_0]](x0) = x0 + 0, [f](x0) = 0 orientation: fst_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))), x3,x2)),x1) = 1x1 + 7x2 + 5x3 + 6x5 + 2x6 + 6 >= 2x5 + 4 = fst_cond[1]#(rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]()) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) = 1x1 + 2x3 + 6 >= x3 + 5 = P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) = 1x1 + 5x3 + 3x4 + 4 >= 5x3 + 3x4 + 4 = P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) problem: DPs: TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Qed DPs: snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Usable Rule Processor: DPs: snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Arctic Interpretation Processor: dimension: 1 usable rules: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) interpretation: [snd_cond[1]#](x0, x1) = x0, [bot[9]] = 4, [bot[8]] = 5, [bot[7]] = 5, [bot[6]] = 1, [Node](x0, x1) = 5x0 + 4x1 + 0, [rpm_9](x0, x1, x2) = 2x1 + 2x2, [rpm_8](x0, x1, x2) = 4x1 + 1x2, [Leaf](x0) = 4x0 + 7, [P](x0, x1) = 1x0 + 2x1, [rpm_4](x0) = x0 + 4, [rpm_3](x0) = x0 + 0, [rec[rpm_0][3]](x0, x1, x2) = x0, [f_0](x0) = 0, [rec[x_0]](x0) = 4x0 + 5, [f](x0) = x0 + 0 orientation: snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))), x3,x2)),x1) = 4x2 + 4x3 + 2x5 + 5x6 >= x2 = snd_cond[1]#(rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]()) snd_cond[1]#(P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))), x3,x2)),x1) = 4x2 + 4x3 + 2x5 + 5x6 >= x3 = snd_cond[1]#(rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) = 4x3 + 7 >= 2x3 + 6 = P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) = 4x3 + 5x4 + 0 >= 4x3 + 5x4 = P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) problem: DPs: TRS: rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) Qed DPs: rec[min_0][2]#(S(x10),S(x6)) -> rec[min_0][2]#(x10,x6) TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Subterm Criterion Processor: simple projection: pi(rec[min_0][2]#) = 0 problem: DPs: TRS: rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]()) fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]())) fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> Node(fst_cond[1](rec[rpm_0][3](x6,f_0(rec[x_0](f(x7))),bot[2]()),bot[3]()), fst_cond[1](rec[rpm_0][3](x5,f_0(rec[x_0](f(x7))),bot[4]()),bot[5]())) rec[min_0][2](0(),x82) -> 0() rec[min_0][2](S(x90),0()) -> 0() rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6)) rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3)) rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) -> P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3)) snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2 snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5),rpm_9(f_0(rec[x_0](f(x4))),x3,x2)),x1) -> rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]()),bot[7]()), snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]()),bot[9]())) main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()) Qed