YES Problem: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Proof: DP Processor: DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0(bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) main#(S(S(x1))) -> evalState_cond#(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) TDG Processor: DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) main#(S(S(x1))) -> evalState_cond#(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) graph: main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) main#(S(S(x1))) -> bind_cond#(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))),liftM2_0( bind_m_f ( bind_m_f ( get(),liftM_0(find_key(x1))), memoM_0 (x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) main#(S(S(x1))) -> bind_cond#(Pair(Nil(),None()),memoM_0(S(x1))) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> find_key[1]#(S(x1),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> find_key[1]#(x8,x2) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) bind_cond#(Pair(x3,x2),liftM2_1(x1)) -> rec[plus_0][2]#(x1,x2) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) -> bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) -> bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) -> rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) -> rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) -> find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) -> find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> rec[equal_0][2]#(x7,x9) 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: 4 #rules: 12 #arcs: 93/361 DPs: bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) EDG Processor: DPs: bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) graph: bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) -> bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) -> bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) -> bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) -> bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) SCC Processor: #sccs: 1 #rules: 6 #arcs: 15/64 DPs: bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Usable Rule Processor: DPs: bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1]#(memoM_1(0()),x9) TRS: find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) Matrix Interpretation Processor: dim=1 usable rules: interpretation: [bind_m_f[1]#](x0, x1) = 4x0 + 1, [bind_cond#](x0, x1) = 2x1 + 1, [liftM2_1](x0) = 0, [liftM2_0](x0) = x0, [bind_m_f](x0, x1) = x1, [liftM_0](x0) = 4x0, [find_key](x0) = 6x0 + 4, [get] = 0, [bind_m_f[1]](x0, x1) = 2, [memoM_0](x0) = x0, [bind_cond](x0, x1) = 4, [memoM_1](x0) = 0, [Cons](x0, x1) = 2x0 + 2x1 + 4, [None] = 1, [Nil] = 2, [rec[equal_0][2]](x0, x1) = 2x1 + 1, [find_key[1]](x0, x1) = 3x0 + x1 + 2, [False] = 0, [Some](x0) = 2, [find_cond_2](x0, x1, x2, x3) = 4, [True] = 0, [S](x0) = 2x0 + 4, [rec[plus_0][2]](x0, x1) = 4, [0] = 5, [Pair](x0, x1) = x0 + 2x1 + 2 orientation: bind_m_f[1]#(x2,x1) = 4x2 + 1 >= 2x2 + 1 = bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))), memoM_0(x6)))) = 2x6 + 1 >= 2x6 + 1 = bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) = 8x1 + 25 >= 2x1 + 1 = bind_cond#(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))),liftM2_0 ( bind_m_f ( bind_m_f ( get(), liftM_0 ( find_key ( x1))), memoM_0 ( x1)))) bind_cond#(Pair(x2,None()),memoM_0(S(S(x1)))) = 8x1 + 25 >= 4x1 + 9 = bind_cond#(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))) bind_cond#(Pair(x9,None()),memoM_0(S(0()))) = 29 >= 1 = bind_m_f[1]#(memoM_1(S(0())),x9) bind_cond#(Pair(x9,None()),memoM_0(0())) = 11 >= 1 = bind_m_f[1]#(memoM_1(0()),x9) find_key[1](x29,Nil()) = 3x29 + 4 >= 1 = None() find_key[1](x9,Cons(Pair(x7,x5),x3)) = 2x3 + 4x5 + 2x7 + 3x9 + 10 >= 4 = find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) find_cond_2(True(),x15,x21,x25) = 4 >= 2 = Some(x25) find_cond_2(False(),x58,x4,x7) = 4 >= x4 + 3x58 + 2 = find_key[1](x58,x4) rec[equal_0][2](0(),0()) = 11 >= 0 = True() rec[equal_0][2](0(),S(x122)) = 4x122 + 9 >= 0 = False() rec[equal_0][2](S(x122),0()) = 11 >= 0 = False() rec[equal_0][2](S(x10),S(x6)) = 4x6 + 9 >= 2x6 + 1 = rec[equal_0][2](x10,x6) bind_cond(Pair(x9,None()),memoM_0(S(0()))) = 4 >= 2 = bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) = 4 >= 4 = bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))), memoM_0(x1)))),memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) = 4 >= 2x76 + x84 + 2 = Pair(x84,x76) bind_m_f[1](x2,x1) = 2 >= 4 = bind_cond(Pair(x1,S(0())),x2) bind_cond(Pair(x337,x152),memoM_1(x209)) = 4 >= 6x152 + 2x209 + 2x337 + 10 = Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x3,x2),liftM2_1(x1)) = 4 >= x3 + 10 = Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))), memoM_0(x6)))) = 4 >= 4 = bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) rec[plus_0][2](0(),x50) = 4 >= x50 = x50 rec[plus_0][2](S(x10),x6) = 4 >= 12 = S(rec[plus_0][2](x10,x6)) bind_cond(Pair(x9,None()),memoM_0(0())) = 4 >= 2 = bind_m_f[1](memoM_1(0()),x9) problem: DPs: bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))), memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) TRS: find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) Restore Modifier: DPs: bind_m_f[1]#(x2,x1) -> bind_cond#(Pair(x1,S(0())),x2) bind_cond#(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))), memoM_0(x6)))) -> bind_cond#(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))), memoM_0(x1))))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 11/4 DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Subterm Criterion Processor: simple projection: pi(rec[plus_0][2]#) = 0 problem: DPs: TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Qed DPs: find_key[1]#(x9,Cons(Pair(x7,x5),x3)) -> find_cond_2#(rec[equal_0][2](x7,x9),x9,x3,x5) find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Subterm Criterion Processor: simple projection: pi(find_cond_2#) = 2 pi(find_key[1]#) = 1 problem: DPs: find_cond_2#(False(),x58,x4,x7) -> find_key[1]#(x58,x4) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1 DPs: rec[equal_0][2]#(S(x10),S(x6)) -> rec[equal_0][2]#(x10,x6) TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Subterm Criterion Processor: simple projection: pi(rec[equal_0][2]#) = 0 problem: DPs: TRS: evalState_cond(Pair(x9,x11)) -> x11 rec[plus_0][2](0(),x50) -> x50 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) find_cond_2(True(),x15,x21,x25) -> Some(x25) find_cond_2(False(),x58,x4,x7) -> find_key[1](x58,x4) rec[equal_0][2](0(),0()) -> True() rec[equal_0][2](0(),S(x122)) -> False() rec[equal_0][2](S(x122),0()) -> False() rec[equal_0][2](S(x10),S(x6)) -> rec[equal_0][2](x10,x6) find_key[1](x29,Nil()) -> None() find_key[1](x9,Cons(Pair(x7,x5),x3)) -> find_cond_2(rec[equal_0][2](x7,x9),x9,x3,x5) bind_cond(Pair(x337,x152),memoM_1(x209)) -> Pair(Cons(Pair(x209,x152),x337),x152) bind_cond(Pair(x9,None()),memoM_0(0())) -> bind_m_f[1](memoM_1(0()),x9) bind_cond(Pair(x9,None()),memoM_0(S(0()))) -> bind_m_f[1](memoM_1(S(0())),x9) bind_cond(Pair(x2,None()),memoM_0(S(S(x1)))) -> bind_cond(bind_cond(bind_cond(Pair(x2,find_key[1](S(x1),x2)),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1)))), memoM_1(S(S(x1)))) bind_cond(Pair(x84,Some(x76)),memoM_0(x22)) -> Pair(x84,x76) bind_cond(Pair(x3,x2),liftM2_1(x1)) -> Pair(x3,rec[plus_0][2](x1,x2)) bind_cond(Pair(x2,x4),liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x8))),memoM_0(x6)))) -> bind_cond(bind_cond(Pair(x2,find_key[1](x8,x2)),memoM_0(x6)),liftM2_1(x4)) bind_m_f[1](x2,x1) -> bind_cond(Pair(x1,S(0())),x2) main(0()) -> S(0()) main(S(0())) -> S(0()) main(S(S(x1))) -> evalState_cond(bind_cond(bind_cond(Pair(Nil(),None()),memoM_0(S(x1))), liftM2_0(bind_m_f(bind_m_f(get(),liftM_0(find_key(x1))),memoM_0(x1))))) Qed