* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            cond_fst_p#1(P(rpm_t_m_2(x2),x1),x3) -> rpm_t_m_2#1(x2,x3)
            cond_fst_p#1(P(rpm_t_m_9(x2,x3,x4),x1),x5) -> rpm_t_m_9#1(x2,x3,x4,x5)
            fst#2(P(rpm_t_m_2(x2),x1),x3) -> rpm_t_m_2#1(x2,x3)
            fst#2(P(rpm_t_m_9(x2,x3,x4),x1),x5) -> rpm_t_m_9#1(x2,x3,x4,x5)
            main(x1) -> cond_fst_p#1(x#1(f(x1),bot[0]()),bot[1]())
            min#2(0(),x12) -> 0()
            min#2(S(x16),0()) -> 0()
            min#2(S(x4),S(x2)) -> S(min#2(x4,x2))
            rpm#3(Leaf(x8),f_p(x12,x16),x4) -> P(rpm_t_m_2(f_p(x12,x16)),rpm_t_m_3(x8))
            rpm#3(Node(x8,x6),f_p(x2,x4),x10) -> rpm_t_m_8#1(rpm#3(x8,f_p(x2,x4),bot[9]())
                                                            ,rpm#3(x6,f_p(x2,x4),bot[10]())
                                                            ,x10)
            rpm_t_m_2#1(f_p(snd(),x(x2)),x3) -> Leaf(snd#2(x#1(x2,bot[2]()),bot[3]()))
            rpm_t_m_8#1(x3,x2,x1) -> P(rpm_t_m_9(fst(),x3,x2),rpm_t_m_10(x3,x2))
            rpm_t_m_9#1(fst(),P(rpm_t_m_2(x4),x2),x5,x3) -> Node(rpm_t_m_2#1(x4,bot[5]()),fst#2(x5,bot[6]()))
            rpm_t_m_9#1(fst(),P(rpm_t_m_9(x4,x6,x8),x2),x5,x3) -> Node(rpm_t_m_9#1(x4,x6,x8,bot[5]())
                                                                      ,fst#2(x5,bot[6]()))
            snd#2(P(x18,rpm_t_m_3(x14)),x18) -> x14
            snd#2(P(x2,rpm_t_m_10(x6,x4)),x2) -> min#2(snd#2(x6,bot[7]()),snd#2(x4,bot[8]()))
            x#1(f(x4),x3) -> rpm#3(x4,f_p(snd(),x(f(x4))),bot[11]())
        - Signature:
            {cond_fst_p#1/2,fst#2/2,main/1,min#2/2,rpm#3/3,rpm_t_m_2#1/2,rpm_t_m_8#1/3,rpm_t_m_9#1/4,snd#2/2
            ,x#1/2} / {0/0,Leaf/1,Node/2,P/2,S/1,bot[0]/0,bot[10]/0,bot[11]/0,bot[1]/0,bot[2]/0,bot[3]/0,bot[5]/0
            ,bot[6]/0,bot[7]/0,bot[8]/0,bot[9]/0,f/1,f_p/2,fst/0,rpm_t_m_10/2,rpm_t_m_2/1,rpm_t_m_3/1,rpm_t_m_9/3,snd/0
            ,x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {cond_fst_p#1,fst#2,main,min#2,rpm#3,rpm_t_m_2#1
            ,rpm_t_m_8#1,rpm_t_m_9#1,snd#2,x#1} and constructors {0,Leaf,Node,P,S,bot[0],bot[10],bot[11],bot[1],bot[2]
            ,bot[3],bot[5],bot[6],bot[7],bot[8],bot[9],f,f_p,fst,rpm_t_m_10,rpm_t_m_2,rpm_t_m_3,rpm_t_m_9,snd,x}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            cond_fst_p#1(P(rpm_t_m_2(x2),x1),x3) -> rpm_t_m_2#1(x2,x3)
            cond_fst_p#1(P(rpm_t_m_9(x2,x3,x4),x1),x5) -> rpm_t_m_9#1(x2,x3,x4,x5)
            fst#2(P(rpm_t_m_2(x2),x1),x3) -> rpm_t_m_2#1(x2,x3)
            fst#2(P(rpm_t_m_9(x2,x3,x4),x1),x5) -> rpm_t_m_9#1(x2,x3,x4,x5)
            main(x1) -> cond_fst_p#1(x#1(f(x1),bot[0]()),bot[1]())
            min#2(0(),x12) -> 0()
            min#2(S(x16),0()) -> 0()
            min#2(S(x4),S(x2)) -> S(min#2(x4,x2))
            rpm#3(Leaf(x8),f_p(x12,x16),x4) -> P(rpm_t_m_2(f_p(x12,x16)),rpm_t_m_3(x8))
            rpm#3(Node(x8,x6),f_p(x2,x4),x10) -> rpm_t_m_8#1(rpm#3(x8,f_p(x2,x4),bot[9]())
                                                            ,rpm#3(x6,f_p(x2,x4),bot[10]())
                                                            ,x10)
            rpm_t_m_2#1(f_p(snd(),x(x2)),x3) -> Leaf(snd#2(x#1(x2,bot[2]()),bot[3]()))
            rpm_t_m_8#1(x3,x2,x1) -> P(rpm_t_m_9(fst(),x3,x2),rpm_t_m_10(x3,x2))
            rpm_t_m_9#1(fst(),P(rpm_t_m_2(x4),x2),x5,x3) -> Node(rpm_t_m_2#1(x4,bot[5]()),fst#2(x5,bot[6]()))
            rpm_t_m_9#1(fst(),P(rpm_t_m_9(x4,x6,x8),x2),x5,x3) -> Node(rpm_t_m_9#1(x4,x6,x8,bot[5]())
                                                                      ,fst#2(x5,bot[6]()))
            snd#2(P(x18,rpm_t_m_3(x14)),x18) -> x14
            snd#2(P(x2,rpm_t_m_10(x6,x4)),x2) -> min#2(snd#2(x6,bot[7]()),snd#2(x4,bot[8]()))
            x#1(f(x4),x3) -> rpm#3(x4,f_p(snd(),x(f(x4))),bot[11]())
        - Signature:
            {cond_fst_p#1/2,fst#2/2,main/1,min#2/2,rpm#3/3,rpm_t_m_2#1/2,rpm_t_m_8#1/3,rpm_t_m_9#1/4,snd#2/2
            ,x#1/2} / {0/0,Leaf/1,Node/2,P/2,S/1,bot[0]/0,bot[10]/0,bot[11]/0,bot[1]/0,bot[2]/0,bot[3]/0,bot[5]/0
            ,bot[6]/0,bot[7]/0,bot[8]/0,bot[9]/0,f/1,f_p/2,fst/0,rpm_t_m_10/2,rpm_t_m_2/1,rpm_t_m_3/1,rpm_t_m_9/3,snd/0
            ,x/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {cond_fst_p#1,fst#2,main,min#2,rpm#3,rpm_t_m_2#1
            ,rpm_t_m_8#1,rpm_t_m_9#1,snd#2,x#1} and constructors {0,Leaf,Node,P,S,bot[0],bot[10],bot[11],bot[1],bot[2]
            ,bot[3],bot[5],bot[6],bot[7],bot[8],bot[9],f,f_p,fst,rpm_t_m_10,rpm_t_m_2,rpm_t_m_3,rpm_t_m_9,snd,x}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          min#2(x,y){x -> S(x),y -> S(y)} =
            min#2(S(x),S(y)) ->^+ S(min#2(x,y))
              = C[min#2(x,y) = min#2(x,y){}]

WORST_CASE(Omega(n^1),?)