WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            #abs(#0()) -> #0()
            #abs(#neg(x)) -> #pos(x)
            #abs(#pos(x)) -> #pos(x)
            #abs(#s(x)) -> #pos(#s(x))
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0
            ,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs,#cklt,#compare,#less,insert,insert#1,insert#2
            ,insertD,insertD#1,insertD#2,insertionsort,insertionsort#1,insertionsortD
            ,insertionsortD#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          #abs#(#0()) -> c_1()
          #abs#(#neg(x)) -> c_2()
          #abs#(#pos(x)) -> c_3()
          #abs#(#s(x)) -> c_4()
          #cklt#(#EQ()) -> c_5()
          #cklt#(#GT()) -> c_6()
          #cklt#(#LT()) -> c_7()
          #compare#(#0(),#0()) -> c_8()
          #compare#(#0(),#neg(y)) -> c_9()
          #compare#(#0(),#pos(y)) -> c_10()
          #compare#(#0(),#s(y)) -> c_11()
          #compare#(#neg(x),#0()) -> c_12()
          #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
          #compare#(#neg(x),#pos(y)) -> c_14()
          #compare#(#pos(x),#0()) -> c_15()
          #compare#(#pos(x),#neg(y)) -> c_16()
          #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
          #compare#(#s(x),#0()) -> c_18()
          #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
          #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
          insert#(x,l) -> c_21(insert#1#(l,x))
          insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
          insert#1#(nil(),x) -> c_23()
          insert#2#(#false(),x,y,ys) -> c_24()
          insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
          insertD#(x,l) -> c_26(insertD#1#(l,x))
          insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
          insertD#1#(nil(),x) -> c_28()
          insertD#2#(#false(),x,y,ys) -> c_29()
          insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
          insertionsort#(l) -> c_31(insertionsort#1#(l))
          insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
          insertionsort#1#(nil()) -> c_33()
          insertionsortD#(l) -> c_34(insertionsortD#1#(l))
          insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
          insertionsortD#1#(nil()) -> c_36()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #abs#(#0()) -> c_1()
            #abs#(#neg(x)) -> c_2()
            #abs#(#pos(x)) -> c_3()
            #abs#(#s(x)) -> c_4()
            #cklt#(#EQ()) -> c_5()
            #cklt#(#GT()) -> c_6()
            #cklt#(#LT()) -> c_7()
            #compare#(#0(),#0()) -> c_8()
            #compare#(#0(),#neg(y)) -> c_9()
            #compare#(#0(),#pos(y)) -> c_10()
            #compare#(#0(),#s(y)) -> c_11()
            #compare#(#neg(x),#0()) -> c_12()
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#neg(x),#pos(y)) -> c_14()
            #compare#(#pos(x),#0()) -> c_15()
            #compare#(#pos(x),#neg(y)) -> c_16()
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#0()) -> c_18()
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#1#(nil(),x) -> c_23()
            insert#2#(#false(),x,y,ys) -> c_24()
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#1#(nil(),x) -> c_28()
            insertD#2#(#false(),x,y,ys) -> c_29()
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsort#1#(nil()) -> c_33()
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
            insertionsortD#1#(nil()) -> c_36()
        - Weak TRS:
            #abs(#0()) -> #0()
            #abs(#neg(x)) -> #pos(x)
            #abs(#pos(x)) -> #pos(x)
            #abs(#s(x)) -> #pos(#s(x))
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,18,23,24,28,29,33,36}
        by application of
          Pre({1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,18,23,24,28,29,33,36}) = {13,17,19,20,21,22,26,27,31,34}.
        Here rules are labelled as follows:
          1: #abs#(#0()) -> c_1()
          2: #abs#(#neg(x)) -> c_2()
          3: #abs#(#pos(x)) -> c_3()
          4: #abs#(#s(x)) -> c_4()
          5: #cklt#(#EQ()) -> c_5()
          6: #cklt#(#GT()) -> c_6()
          7: #cklt#(#LT()) -> c_7()
          8: #compare#(#0(),#0()) -> c_8()
          9: #compare#(#0(),#neg(y)) -> c_9()
          10: #compare#(#0(),#pos(y)) -> c_10()
          11: #compare#(#0(),#s(y)) -> c_11()
          12: #compare#(#neg(x),#0()) -> c_12()
          13: #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
          14: #compare#(#neg(x),#pos(y)) -> c_14()
          15: #compare#(#pos(x),#0()) -> c_15()
          16: #compare#(#pos(x),#neg(y)) -> c_16()
          17: #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
          18: #compare#(#s(x),#0()) -> c_18()
          19: #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
          20: #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
          21: insert#(x,l) -> c_21(insert#1#(l,x))
          22: insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
          23: insert#1#(nil(),x) -> c_23()
          24: insert#2#(#false(),x,y,ys) -> c_24()
          25: insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
          26: insertD#(x,l) -> c_26(insertD#1#(l,x))
          27: insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
          28: insertD#1#(nil(),x) -> c_28()
          29: insertD#2#(#false(),x,y,ys) -> c_29()
          30: insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
          31: insertionsort#(l) -> c_31(insertionsort#1#(l))
          32: insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
          33: insertionsort#1#(nil()) -> c_33()
          34: insertionsortD#(l) -> c_34(insertionsortD#1#(l))
          35: insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
          36: insertionsortD#1#(nil()) -> c_36()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        - Weak DPs:
            #abs#(#0()) -> c_1()
            #abs#(#neg(x)) -> c_2()
            #abs#(#pos(x)) -> c_3()
            #abs#(#s(x)) -> c_4()
            #cklt#(#EQ()) -> c_5()
            #cklt#(#GT()) -> c_6()
            #cklt#(#LT()) -> c_7()
            #compare#(#0(),#0()) -> c_8()
            #compare#(#0(),#neg(y)) -> c_9()
            #compare#(#0(),#pos(y)) -> c_10()
            #compare#(#0(),#s(y)) -> c_11()
            #compare#(#neg(x),#0()) -> c_12()
            #compare#(#neg(x),#pos(y)) -> c_14()
            #compare#(#pos(x),#0()) -> c_15()
            #compare#(#pos(x),#neg(y)) -> c_16()
            #compare#(#s(x),#0()) -> c_18()
            insert#1#(nil(),x) -> c_23()
            insert#2#(#false(),x,y,ys) -> c_24()
            insertD#1#(nil(),x) -> c_28()
            insertD#2#(#false(),x,y,ys) -> c_29()
            insertionsort#1#(nil()) -> c_33()
            insertionsortD#1#(nil()) -> c_36()
        - Weak TRS:
            #abs(#0()) -> #0()
            #abs(#neg(x)) -> #pos(x)
            #abs(#pos(x)) -> #pos(x)
            #abs(#s(x)) -> #pos(#s(x))
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:#compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#s(x),#0()) -> c_18():30
             -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29
             -->_1 #compare#(#pos(x),#0()) -> c_15():28
             -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27
             -->_1 #compare#(#neg(x),#0()) -> c_12():26
             -->_1 #compare#(#0(),#s(y)) -> c_11():25
             -->_1 #compare#(#0(),#pos(y)) -> c_10():24
             -->_1 #compare#(#0(),#neg(y)) -> c_9():23
             -->_1 #compare#(#0(),#0()) -> c_8():22
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          2:S:#compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#s(x),#0()) -> c_18():30
             -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29
             -->_1 #compare#(#pos(x),#0()) -> c_15():28
             -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27
             -->_1 #compare#(#neg(x),#0()) -> c_12():26
             -->_1 #compare#(#0(),#s(y)) -> c_11():25
             -->_1 #compare#(#0(),#pos(y)) -> c_10():24
             -->_1 #compare#(#0(),#neg(y)) -> c_9():23
             -->_1 #compare#(#0(),#0()) -> c_8():22
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          3:S:#compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
             -->_1 #compare#(#s(x),#0()) -> c_18():30
             -->_1 #compare#(#pos(x),#neg(y)) -> c_16():29
             -->_1 #compare#(#pos(x),#0()) -> c_15():28
             -->_1 #compare#(#neg(x),#pos(y)) -> c_14():27
             -->_1 #compare#(#neg(x),#0()) -> c_12():26
             -->_1 #compare#(#0(),#s(y)) -> c_11():25
             -->_1 #compare#(#0(),#pos(y)) -> c_10():24
             -->_1 #compare#(#0(),#neg(y)) -> c_9():23
             -->_1 #compare#(#0(),#0()) -> c_8():22
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          4:S:#less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
             -->_2 #compare#(#s(x),#0()) -> c_18():30
             -->_2 #compare#(#pos(x),#neg(y)) -> c_16():29
             -->_2 #compare#(#pos(x),#0()) -> c_15():28
             -->_2 #compare#(#neg(x),#pos(y)) -> c_14():27
             -->_2 #compare#(#neg(x),#0()) -> c_12():26
             -->_2 #compare#(#0(),#s(y)) -> c_11():25
             -->_2 #compare#(#0(),#pos(y)) -> c_10():24
             -->_2 #compare#(#0(),#neg(y)) -> c_9():23
             -->_2 #compare#(#0(),#0()) -> c_8():22
             -->_1 #cklt#(#LT()) -> c_7():21
             -->_1 #cklt#(#GT()) -> c_6():20
             -->_1 #cklt#(#EQ()) -> c_5():19
             -->_2 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_2 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_2 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          5:S:insert#(x,l) -> c_21(insert#1#(l,x))
             -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):6
             -->_1 insert#1#(nil(),x) -> c_23():31
          
          6:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):7
             -->_1 insert#2#(#false(),x,y,ys) -> c_24():32
             -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4
          
          7:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5
          
          8:S:insertD#(x,l) -> c_26(insertD#1#(l,x))
             -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):9
             -->_1 insertD#1#(nil(),x) -> c_28():33
          
          9:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):10
             -->_1 insertD#2#(#false(),x,y,ys) -> c_29():34
             -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4
          
          10:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8
          
          11:S:insertionsort#(l) -> c_31(insertionsort#1#(l))
             -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):12
             -->_1 insertionsort#1#(nil()) -> c_33():35
          
          12:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):11
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5
          
          13:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l))
             -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):14
             -->_1 insertionsortD#1#(nil()) -> c_36():36
          
          14:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
             -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):13
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8
          
          15:W:#abs#(#0()) -> c_1()
             
          
          16:W:#abs#(#neg(x)) -> c_2()
             
          
          17:W:#abs#(#pos(x)) -> c_3()
             
          
          18:W:#abs#(#s(x)) -> c_4()
             
          
          19:W:#cklt#(#EQ()) -> c_5()
             
          
          20:W:#cklt#(#GT()) -> c_6()
             
          
          21:W:#cklt#(#LT()) -> c_7()
             
          
          22:W:#compare#(#0(),#0()) -> c_8()
             
          
          23:W:#compare#(#0(),#neg(y)) -> c_9()
             
          
          24:W:#compare#(#0(),#pos(y)) -> c_10()
             
          
          25:W:#compare#(#0(),#s(y)) -> c_11()
             
          
          26:W:#compare#(#neg(x),#0()) -> c_12()
             
          
          27:W:#compare#(#neg(x),#pos(y)) -> c_14()
             
          
          28:W:#compare#(#pos(x),#0()) -> c_15()
             
          
          29:W:#compare#(#pos(x),#neg(y)) -> c_16()
             
          
          30:W:#compare#(#s(x),#0()) -> c_18()
             
          
          31:W:insert#1#(nil(),x) -> c_23()
             
          
          32:W:insert#2#(#false(),x,y,ys) -> c_24()
             
          
          33:W:insertD#1#(nil(),x) -> c_28()
             
          
          34:W:insertD#2#(#false(),x,y,ys) -> c_29()
             
          
          35:W:insertionsort#1#(nil()) -> c_33()
             
          
          36:W:insertionsortD#1#(nil()) -> c_36()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          18: #abs#(#s(x)) -> c_4()
          17: #abs#(#pos(x)) -> c_3()
          16: #abs#(#neg(x)) -> c_2()
          15: #abs#(#0()) -> c_1()
          36: insertionsortD#1#(nil()) -> c_36()
          35: insertionsort#1#(nil()) -> c_33()
          33: insertD#1#(nil(),x) -> c_28()
          34: insertD#2#(#false(),x,y,ys) -> c_29()
          31: insert#1#(nil(),x) -> c_23()
          32: insert#2#(#false(),x,y,ys) -> c_24()
          19: #cklt#(#EQ()) -> c_5()
          20: #cklt#(#GT()) -> c_6()
          21: #cklt#(#LT()) -> c_7()
          22: #compare#(#0(),#0()) -> c_8()
          23: #compare#(#0(),#neg(y)) -> c_9()
          24: #compare#(#0(),#pos(y)) -> c_10()
          25: #compare#(#0(),#s(y)) -> c_11()
          26: #compare#(#neg(x),#0()) -> c_12()
          27: #compare#(#neg(x),#pos(y)) -> c_14()
          28: #compare#(#pos(x),#0()) -> c_15()
          29: #compare#(#pos(x),#neg(y)) -> c_16()
          30: #compare#(#s(x),#0()) -> c_18()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        - Weak TRS:
            #abs(#0()) -> #0()
            #abs(#neg(x)) -> #pos(x)
            #abs(#pos(x)) -> #pos(x)
            #abs(#s(x)) -> #pos(#s(x))
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/2,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:#compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          2:S:#compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          3:S:#compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
             -->_1 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_1 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_1 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          4:S:#less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y))
             -->_2 #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y)):3
             -->_2 #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y)):2
             -->_2 #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x)):1
          
          5:S:insert#(x,l) -> c_21(insert#1#(l,x))
             -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):6
          
          6:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):7
             -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4
          
          7:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5
          
          8:S:insertD#(x,l) -> c_26(insertD#1#(l,x))
             -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):9
          
          9:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):10
             -->_2 #less#(x,y) -> c_20(#cklt#(#compare(x,y)),#compare#(x,y)):4
          
          10:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8
          
          11:S:insertionsort#(l) -> c_31(insertionsort#1#(l))
             -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):12
          
          12:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):11
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):5
          
          13:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l))
             -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):14
          
          14:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
             -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):13
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):8
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          #less#(x,y) -> c_20(#compare#(x,y))
* Step 5: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        - Weak TRS:
            #abs(#0()) -> #0()
            #abs(#neg(x)) -> #pos(x)
            #abs(#pos(x)) -> #pos(x)
            #abs(#s(x)) -> #pos(#s(x))
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          #cklt(#EQ()) -> #false()
          #cklt(#GT()) -> #false()
          #cklt(#LT()) -> #true()
          #compare(#0(),#0()) -> #EQ()
          #compare(#0(),#neg(y)) -> #GT()
          #compare(#0(),#pos(y)) -> #LT()
          #compare(#0(),#s(y)) -> #LT()
          #compare(#neg(x),#0()) -> #LT()
          #compare(#neg(x),#neg(y)) -> #compare(y,x)
          #compare(#neg(x),#pos(y)) -> #LT()
          #compare(#pos(x),#0()) -> #GT()
          #compare(#pos(x),#neg(y)) -> #GT()
          #compare(#pos(x),#pos(y)) -> #compare(x,y)
          #compare(#s(x),#0()) -> #GT()
          #compare(#s(x),#s(y)) -> #compare(x,y)
          #less(x,y) -> #cklt(#compare(x,y))
          insert(x,l) -> insert#1(l,x)
          insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
          insert#1(nil(),x) -> dd(x,nil())
          insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
          insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
          insertD(x,l) -> insertD#1(l,x)
          insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
          insertD#1(nil(),x) -> dd(x,nil())
          insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
          insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
          insertionsort(l) -> insertionsort#1(l)
          insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
          insertionsort#1(nil()) -> nil()
          insertionsortD(l) -> insertionsortD#1(l)
          insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
          insertionsortD#1(nil()) -> nil()
          #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
          #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
          #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
          #less#(x,y) -> c_20(#compare#(x,y))
          insert#(x,l) -> c_21(insert#1#(l,x))
          insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
          insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
          insertD#(x,l) -> c_26(insertD#1#(l,x))
          insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
          insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
          insertionsort#(l) -> c_31(insertionsort#1#(l))
          insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
          insertionsortD#(l) -> c_34(insertionsortD#1#(l))
          insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
* Step 6: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          insertionsort#(l) -> c_31(insertionsort#1#(l))
          insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
          insertionsortD#(l) -> c_34(insertionsortD#1#(l))
          insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        and a lower component
          #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
          #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
          #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
          #less#(x,y) -> c_20(#compare#(x,y))
          insert#(x,l) -> c_21(insert#1#(l,x))
          insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
          insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
          insertD#(x,l) -> c_26(insertD#1#(l,x))
          insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
          insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
        Further, following extension rules are added to the lower component.
          insertionsort#(l) -> insertionsort#1#(l)
          insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
          insertionsortD#(l) -> insertionsortD#1#(l)
          insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
          insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:insertionsort#(l) -> c_31(insertionsort#1#(l))
             -->_1 insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs)):2
          
          2:S:insertionsort#1#(dd(x,xs)) -> c_32(insert#(x,insertionsort(xs)),insertionsort#(xs))
             -->_2 insertionsort#(l) -> c_31(insertionsort#1#(l)):1
          
          3:S:insertionsortD#(l) -> c_34(insertionsortD#1#(l))
             -->_1 insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs)):4
          
          4:S:insertionsortD#1#(dd(x,xs)) -> c_35(insertD#(x,insertionsortD(xs)),insertionsortD#(xs))
             -->_2 insertionsortD#(l) -> c_34(insertionsortD#1#(l)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
          insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          insertionsort#(l) -> c_31(insertionsort#1#(l))
          insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
          insertionsortD#(l) -> c_34(insertionsortD#1#(l))
          insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_31) = {1},
            uargs(c_32) = {1},
            uargs(c_34) = {1},
            uargs(c_35) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                  
                          p(#EQ) = [0]                  
                          p(#GT) = [0]                  
                          p(#LT) = [0]                  
                         p(#abs) = [0]                  
                        p(#cklt) = [0]                  
                     p(#compare) = [0]                  
                       p(#false) = [0]                  
                        p(#less) = [0]                  
                         p(#neg) = [1] x1 + [0]         
                         p(#pos) = [1] x1 + [0]         
                           p(#s) = [1] x1 + [0]         
                        p(#true) = [0]                  
                           p(dd) = [1] x1 + [1] x2 + [0]
                       p(insert) = [0]                  
                     p(insert#1) = [0]                  
                     p(insert#2) = [0]                  
                      p(insertD) = [0]                  
                    p(insertD#1) = [0]                  
                    p(insertD#2) = [0]                  
                p(insertionsort) = [0]                  
              p(insertionsort#1) = [0]                  
               p(insertionsortD) = [0]                  
             p(insertionsortD#1) = [0]                  
                          p(nil) = [0]                  
                        p(#abs#) = [0]                  
                       p(#cklt#) = [0]                  
                    p(#compare#) = [0]                  
                       p(#less#) = [0]                  
                      p(insert#) = [0]                  
                    p(insert#1#) = [0]                  
                    p(insert#2#) = [0]                  
                     p(insertD#) = [0]                  
                   p(insertD#1#) = [0]                  
                   p(insertD#2#) = [0]                  
               p(insertionsort#) = [0]                  
             p(insertionsort#1#) = [0]                  
              p(insertionsortD#) = [0]                  
            p(insertionsortD#1#) = [5]                  
                          p(c_1) = [0]                  
                          p(c_2) = [0]                  
                          p(c_3) = [0]                  
                          p(c_4) = [0]                  
                          p(c_5) = [0]                  
                          p(c_6) = [0]                  
                          p(c_7) = [0]                  
                          p(c_8) = [0]                  
                          p(c_9) = [0]                  
                         p(c_10) = [0]                  
                         p(c_11) = [0]                  
                         p(c_12) = [0]                  
                         p(c_13) = [0]                  
                         p(c_14) = [0]                  
                         p(c_15) = [0]                  
                         p(c_16) = [0]                  
                         p(c_17) = [0]                  
                         p(c_18) = [0]                  
                         p(c_19) = [0]                  
                         p(c_20) = [0]                  
                         p(c_21) = [0]                  
                         p(c_22) = [0]                  
                         p(c_23) = [0]                  
                         p(c_24) = [0]                  
                         p(c_25) = [0]                  
                         p(c_26) = [0]                  
                         p(c_27) = [0]                  
                         p(c_28) = [0]                  
                         p(c_29) = [0]                  
                         p(c_30) = [0]                  
                         p(c_31) = [1] x1 + [0]         
                         p(c_32) = [1] x1 + [0]         
                         p(c_33) = [0]                  
                         p(c_34) = [1] x1 + [0]         
                         p(c_35) = [1] x1 + [0]         
                         p(c_36) = [0]                  
          
          Following rules are strictly oriented:
          insertionsortD#1#(dd(x,xs)) = [5]                      
                                      > [0]                      
                                      = c_35(insertionsortD#(xs))
          
          
          Following rules are (at-least) weakly oriented:
                   insertionsort#(l) =  [0]                       
                                     >= [0]                       
                                     =  c_31(insertionsort#1#(l)) 
          
          insertionsort#1#(dd(x,xs)) =  [0]                       
                                     >= [0]                       
                                     =  c_32(insertionsort#(xs))  
          
                  insertionsortD#(l) =  [0]                       
                                     >= [5]                       
                                     =  c_34(insertionsortD#1#(l))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 6.a:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
        - Weak DPs:
            insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_31) = {1},
            uargs(c_32) = {1},
            uargs(c_34) = {1},
            uargs(c_35) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                           
                          p(#EQ) = [2]                           
                          p(#GT) = [0]                           
                          p(#LT) = [0]                           
                         p(#abs) = [0]                           
                        p(#cklt) = [0]                           
                     p(#compare) = [0]                           
                       p(#false) = [0]                           
                        p(#less) = [2] x2 + [0]                  
                         p(#neg) = [1] x1 + [0]                  
                         p(#pos) = [1] x1 + [0]                  
                           p(#s) = [1] x1 + [0]                  
                        p(#true) = [0]                           
                           p(dd) = [1] x1 + [1] x2 + [1]         
                       p(insert) = [0]                           
                     p(insert#1) = [0]                           
                     p(insert#2) = [0]                           
                      p(insertD) = [0]                           
                    p(insertD#1) = [0]                           
                    p(insertD#2) = [0]                           
                p(insertionsort) = [0]                           
              p(insertionsort#1) = [0]                           
               p(insertionsortD) = [0]                           
             p(insertionsortD#1) = [0]                           
                          p(nil) = [0]                           
                        p(#abs#) = [0]                           
                       p(#cklt#) = [0]                           
                    p(#compare#) = [0]                           
                       p(#less#) = [0]                           
                      p(insert#) = [0]                           
                    p(insert#1#) = [0]                           
                    p(insert#2#) = [0]                           
                     p(insertD#) = [0]                           
                   p(insertD#1#) = [0]                           
                   p(insertD#2#) = [2] x1 + [2] x2 + [2] x3 + [0]
               p(insertionsort#) = [4]                           
             p(insertionsort#1#) = [0]                           
              p(insertionsortD#) = [2] x1 + [7]                  
            p(insertionsortD#1#) = [2] x1 + [5]                  
                          p(c_1) = [0]                           
                          p(c_2) = [0]                           
                          p(c_3) = [0]                           
                          p(c_4) = [0]                           
                          p(c_5) = [0]                           
                          p(c_6) = [0]                           
                          p(c_7) = [0]                           
                          p(c_8) = [0]                           
                          p(c_9) = [0]                           
                         p(c_10) = [0]                           
                         p(c_11) = [0]                           
                         p(c_12) = [0]                           
                         p(c_13) = [0]                           
                         p(c_14) = [0]                           
                         p(c_15) = [0]                           
                         p(c_16) = [0]                           
                         p(c_17) = [0]                           
                         p(c_18) = [0]                           
                         p(c_19) = [0]                           
                         p(c_20) = [0]                           
                         p(c_21) = [0]                           
                         p(c_22) = [0]                           
                         p(c_23) = [0]                           
                         p(c_24) = [0]                           
                         p(c_25) = [1]                           
                         p(c_26) = [1] x1 + [1]                  
                         p(c_27) = [1] x1 + [8] x2 + [1]         
                         p(c_28) = [1]                           
                         p(c_29) = [0]                           
                         p(c_30) = [2] x1 + [1]                  
                         p(c_31) = [1] x1 + [2]                  
                         p(c_32) = [1] x1 + [12]                 
                         p(c_33) = [0]                           
                         p(c_34) = [1] x1 + [1]                  
                         p(c_35) = [1] x1 + [0]                  
                         p(c_36) = [0]                           
          
          Following rules are strictly oriented:
           insertionsort#(l) = [4]                       
                             > [2]                       
                             = c_31(insertionsort#1#(l)) 
          
          insertionsortD#(l) = [2] l + [7]               
                             > [2] l + [6]               
                             = c_34(insertionsortD#1#(l))
          
          
          Following rules are (at-least) weakly oriented:
           insertionsort#1#(dd(x,xs)) =  [0]                      
                                      >= [16]                     
                                      =  c_32(insertionsort#(xs)) 
          
          insertionsortD#1#(dd(x,xs)) =  [2] x + [2] xs + [7]     
                                      >= [2] xs + [7]             
                                      =  c_35(insertionsortD#(xs))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 6.a:5: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
        - Weak DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_31) = {1},
            uargs(c_32) = {1},
            uargs(c_34) = {1},
            uargs(c_35) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                  
                          p(#EQ) = [0]                  
                          p(#GT) = [0]                  
                          p(#LT) = [0]                  
                         p(#abs) = [0]                  
                        p(#cklt) = [0]                  
                     p(#compare) = [0]                  
                       p(#false) = [0]                  
                        p(#less) = [0]                  
                         p(#neg) = [1] x1 + [0]         
                         p(#pos) = [1] x1 + [0]         
                           p(#s) = [1] x1 + [0]         
                        p(#true) = [0]                  
                           p(dd) = [1] x1 + [1] x2 + [1]
                       p(insert) = [0]                  
                     p(insert#1) = [0]                  
                     p(insert#2) = [0]                  
                      p(insertD) = [0]                  
                    p(insertD#1) = [0]                  
                    p(insertD#2) = [0]                  
                p(insertionsort) = [1]                  
              p(insertionsort#1) = [0]                  
               p(insertionsortD) = [0]                  
             p(insertionsortD#1) = [0]                  
                          p(nil) = [0]                  
                        p(#abs#) = [0]                  
                       p(#cklt#) = [0]                  
                    p(#compare#) = [0]                  
                       p(#less#) = [0]                  
                      p(insert#) = [0]                  
                    p(insert#1#) = [1] x1 + [0]         
                    p(insert#2#) = [0]                  
                     p(insertD#) = [0]                  
                   p(insertD#1#) = [0]                  
                   p(insertD#2#) = [0]                  
               p(insertionsort#) = [1] x1 + [0]         
             p(insertionsort#1#) = [1] x1 + [0]         
              p(insertionsortD#) = [0]                  
            p(insertionsortD#1#) = [0]                  
                          p(c_1) = [0]                  
                          p(c_2) = [0]                  
                          p(c_3) = [0]                  
                          p(c_4) = [0]                  
                          p(c_5) = [0]                  
                          p(c_6) = [0]                  
                          p(c_7) = [0]                  
                          p(c_8) = [0]                  
                          p(c_9) = [0]                  
                         p(c_10) = [0]                  
                         p(c_11) = [0]                  
                         p(c_12) = [0]                  
                         p(c_13) = [0]                  
                         p(c_14) = [0]                  
                         p(c_15) = [0]                  
                         p(c_16) = [0]                  
                         p(c_17) = [0]                  
                         p(c_18) = [0]                  
                         p(c_19) = [0]                  
                         p(c_20) = [0]                  
                         p(c_21) = [0]                  
                         p(c_22) = [0]                  
                         p(c_23) = [0]                  
                         p(c_24) = [0]                  
                         p(c_25) = [0]                  
                         p(c_26) = [0]                  
                         p(c_27) = [0]                  
                         p(c_28) = [0]                  
                         p(c_29) = [0]                  
                         p(c_30) = [0]                  
                         p(c_31) = [1] x1 + [0]         
                         p(c_32) = [1] x1 + [0]         
                         p(c_33) = [0]                  
                         p(c_34) = [1] x1 + [0]         
                         p(c_35) = [1] x1 + [0]         
                         p(c_36) = [0]                  
          
          Following rules are strictly oriented:
          insertionsort#1#(dd(x,xs)) = [1] x + [1] xs + [1]    
                                     > [1] xs + [0]            
                                     = c_32(insertionsort#(xs))
          
          
          Following rules are (at-least) weakly oriented:
                    insertionsort#(l) =  [1] l + [0]               
                                      >= [1] l + [0]               
                                      =  c_31(insertionsort#1#(l)) 
          
                   insertionsortD#(l) =  [0]                       
                                      >= [0]                       
                                      =  c_34(insertionsortD#1#(l))
          
          insertionsortD#1#(dd(x,xs)) =  [0]                       
                                      >= [0]                       
                                      =  c_35(insertionsortD#(xs)) 
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 6.a:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            insertionsort#(l) -> c_31(insertionsort#1#(l))
            insertionsort#1#(dd(x,xs)) -> c_32(insertionsort#(xs))
            insertionsortD#(l) -> c_34(insertionsortD#1#(l))
            insertionsortD#1#(dd(x,xs)) -> c_35(insertionsortD#(xs))
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/1,c_33/0,c_34/1,c_35/1,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
        - Weak DPs:
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          insert#(x,l) -> c_21(insert#1#(l,x))
          insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
          insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
          insertD#(x,l) -> c_26(insertD#1#(l,x))
          insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
          insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
          insertionsort#(l) -> insertionsort#1#(l)
          insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
          insertionsortD#(l) -> insertionsortD#1#(l)
          insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
          insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        and a lower component
          #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
          #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
          #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
          #less#(x,y) -> c_20(#compare#(x,y))
        Further, following extension rules are added to the lower component.
          insert#(x,l) -> insert#1#(l,x)
          insert#1#(dd(y,ys),x) -> #less#(y,x)
          insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
          insert#2#(#true(),x,y,ys) -> insert#(x,ys)
          insertD#(x,l) -> insertD#1#(l,x)
          insertD#1#(dd(y,ys),x) -> #less#(y,x)
          insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
          insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
          insertionsort#(l) -> insertionsort#1#(l)
          insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
          insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
          insertionsortD#(l) -> insertionsortD#1#(l)
          insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
          insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
*** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
        - Weak DPs:
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:insert#(x,l) -> c_21(insert#1#(l,x))
             -->_1 insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x)):2
          
          2:S:insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys)):3
          
          3:S:insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):1
          
          4:S:insertD#(x,l) -> c_26(insertD#1#(l,x))
             -->_1 insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x)):5
          
          5:S:insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys),#less#(y,x))
             -->_1 insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys)):6
          
          6:S:insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):4
          
          7:W:insertionsort#(l) -> insertionsort#1#(l)
             -->_1 insertionsort#1#(dd(x,xs)) -> insertionsort#(xs):9
             -->_1 insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs)):8
          
          8:W:insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
             -->_1 insert#(x,l) -> c_21(insert#1#(l,x)):1
          
          9:W:insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
             -->_1 insertionsort#(l) -> insertionsort#1#(l):7
          
          10:W:insertionsortD#(l) -> insertionsortD#1#(l)
             -->_1 insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs):12
             -->_1 insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs)):11
          
          11:W:insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
             -->_1 insertD#(x,l) -> c_26(insertD#1#(l,x)):4
          
          12:W:insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
             -->_1 insertionsortD#(l) -> insertionsortD#1#(l):10
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys))
          insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys))
*** Step 6.b:1.a:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
        - Weak DPs:
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_21) = {1},
            uargs(c_22) = {1},
            uargs(c_25) = {1},
            uargs(c_26) = {1},
            uargs(c_27) = {1},
            uargs(c_30) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                  
                          p(#EQ) = [0]                  
                          p(#GT) = [0]                  
                          p(#LT) = [0]                  
                         p(#abs) = [0]                  
                        p(#cklt) = [1] x1 + [0]         
                     p(#compare) = [0]                  
                       p(#false) = [0]                  
                        p(#less) = [0]                  
                         p(#neg) = [1] x1 + [0]         
                         p(#pos) = [1] x1 + [0]         
                           p(#s) = [0]                  
                        p(#true) = [0]                  
                           p(dd) = [1] x2 + [0]         
                       p(insert) = [1] x2 + [0]         
                     p(insert#1) = [1] x1 + [0]         
                     p(insert#2) = [1] x1 + [1] x4 + [0]
                      p(insertD) = [1] x2 + [0]         
                    p(insertD#1) = [1] x1 + [0]         
                    p(insertD#2) = [1] x1 + [1] x4 + [0]
                p(insertionsort) = [1]                  
              p(insertionsort#1) = [1]                  
               p(insertionsortD) = [2]                  
             p(insertionsortD#1) = [2]                  
                          p(nil) = [1]                  
                        p(#abs#) = [0]                  
                       p(#cklt#) = [0]                  
                    p(#compare#) = [0]                  
                       p(#less#) = [0]                  
                      p(insert#) = [1] x2 + [1]         
                    p(insert#1#) = [1] x1 + [0]         
                    p(insert#2#) = [1] x1 + [1] x4 + [0]
                     p(insertD#) = [1] x2 + [0]         
                   p(insertD#1#) = [1] x1 + [2]         
                   p(insertD#2#) = [1] x1 + [1] x4 + [2]
               p(insertionsort#) = [4]                  
             p(insertionsort#1#) = [4]                  
              p(insertionsortD#) = [1] x1 + [2]         
            p(insertionsortD#1#) = [1] x1 + [2]         
                          p(c_1) = [0]                  
                          p(c_2) = [0]                  
                          p(c_3) = [0]                  
                          p(c_4) = [0]                  
                          p(c_5) = [0]                  
                          p(c_6) = [0]                  
                          p(c_7) = [0]                  
                          p(c_8) = [0]                  
                          p(c_9) = [0]                  
                         p(c_10) = [0]                  
                         p(c_11) = [0]                  
                         p(c_12) = [0]                  
                         p(c_13) = [0]                  
                         p(c_14) = [0]                  
                         p(c_15) = [0]                  
                         p(c_16) = [0]                  
                         p(c_17) = [0]                  
                         p(c_18) = [0]                  
                         p(c_19) = [0]                  
                         p(c_20) = [0]                  
                         p(c_21) = [1] x1 + [0]         
                         p(c_22) = [1] x1 + [0]         
                         p(c_23) = [0]                  
                         p(c_24) = [0]                  
                         p(c_25) = [1] x1 + [3]         
                         p(c_26) = [1] x1 + [0]         
                         p(c_27) = [1] x1 + [6]         
                         p(c_28) = [0]                  
                         p(c_29) = [4]                  
                         p(c_30) = [1] x1 + [0]         
                         p(c_31) = [1]                  
                         p(c_32) = [1] x1 + [1] x2 + [0]
                         p(c_33) = [0]                  
                         p(c_34) = [1] x1 + [0]         
                         p(c_35) = [2] x1 + [4] x2 + [2]
                         p(c_36) = [0]                  
          
          Following rules are strictly oriented:
                        insert#(x,l) = [1] l + [1]         
                                     > [1] l + [0]         
                                     = c_21(insert#1#(l,x))
          
          insertD#2#(#true(),x,y,ys) = [1] ys + [2]        
                                     > [1] ys + [0]        
                                     = c_30(insertD#(x,ys))
          
          
          Following rules are (at-least) weakly oriented:
                insert#1#(dd(y,ys),x) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  c_22(insert#2#(#less(y,x),x,y,ys)) 
          
            insert#2#(#true(),x,y,ys) =  [1] ys + [0]                       
                                      >= [1] ys + [4]                       
                                      =  c_25(insert#(x,ys))                
          
                        insertD#(x,l) =  [1] l + [0]                        
                                      >= [1] l + [2]                        
                                      =  c_26(insertD#1#(l,x))              
          
               insertD#1#(dd(y,ys),x) =  [1] ys + [2]                       
                                      >= [1] ys + [8]                       
                                      =  c_27(insertD#2#(#less(y,x),x,y,ys))
          
                    insertionsort#(l) =  [4]                                
                                      >= [4]                                
                                      =  insertionsort#1#(l)                
          
           insertionsort#1#(dd(x,xs)) =  [4]                                
                                      >= [2]                                
                                      =  insert#(x,insertionsort(xs))       
          
           insertionsort#1#(dd(x,xs)) =  [4]                                
                                      >= [4]                                
                                      =  insertionsort#(xs)                 
          
                   insertionsortD#(l) =  [1] l + [2]                        
                                      >= [1] l + [2]                        
                                      =  insertionsortD#1#(l)               
          
          insertionsortD#1#(dd(x,xs)) =  [1] xs + [2]                       
                                      >= [2]                                
                                      =  insertD#(x,insertionsortD(xs))     
          
          insertionsortD#1#(dd(x,xs)) =  [1] xs + [2]                       
                                      >= [1] xs + [2]                       
                                      =  insertionsortD#(xs)                
          
                         #cklt(#EQ()) =  [0]                                
                                      >= [0]                                
                                      =  #false()                           
          
                         #cklt(#GT()) =  [0]                                
                                      >= [0]                                
                                      =  #false()                           
          
                         #cklt(#LT()) =  [0]                                
                                      >= [0]                                
                                      =  #true()                            
          
                  #compare(#0(),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #EQ()                              
          
               #compare(#0(),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
               #compare(#0(),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
                 #compare(#0(),#s(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
               #compare(#neg(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
            #compare(#neg(x),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(y,x)                      
          
            #compare(#neg(x),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
               #compare(#pos(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
            #compare(#pos(x),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
            #compare(#pos(x),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(x,y)                      
          
                 #compare(#s(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
                #compare(#s(x),#s(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(x,y)                      
          
                           #less(x,y) =  [0]                                
                                      >= [0]                                
                                      =  #cklt(#compare(x,y))               
          
                          insert(x,l) =  [1] l + [0]                        
                                      >= [1] l + [0]                        
                                      =  insert#1(l,x)                      
          
                 insert#1(dd(y,ys),x) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  insert#2(#less(y,x),x,y,ys)        
          
                    insert#1(nil(),x) =  [1]                                
                                      >= [1]                                
                                      =  dd(x,nil())                        
          
            insert#2(#false(),x,y,ys) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  dd(x,dd(y,ys))                     
          
             insert#2(#true(),x,y,ys) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  dd(y,insert(x,ys))                 
          
                         insertD(x,l) =  [1] l + [0]                        
                                      >= [1] l + [0]                        
                                      =  insertD#1(l,x)                     
          
                insertD#1(dd(y,ys),x) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  insertD#2(#less(y,x),x,y,ys)       
          
                   insertD#1(nil(),x) =  [1]                                
                                      >= [1]                                
                                      =  dd(x,nil())                        
          
           insertD#2(#false(),x,y,ys) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  dd(x,dd(y,ys))                     
          
            insertD#2(#true(),x,y,ys) =  [1] ys + [0]                       
                                      >= [1] ys + [0]                       
                                      =  dd(y,insertD(x,ys))                
          
                     insertionsort(l) =  [1]                                
                                      >= [1]                                
                                      =  insertionsort#1(l)                 
          
            insertionsort#1(dd(x,xs)) =  [1]                                
                                      >= [1]                                
                                      =  insert(x,insertionsort(xs))        
          
               insertionsort#1(nil()) =  [1]                                
                                      >= [1]                                
                                      =  nil()                              
          
                    insertionsortD(l) =  [2]                                
                                      >= [2]                                
                                      =  insertionsortD#1(l)                
          
           insertionsortD#1(dd(x,xs)) =  [2]                                
                                      >= [2]                                
                                      =  insertD(x,insertionsortD(xs))      
          
              insertionsortD#1(nil()) =  [2]                                
                                      >= [1]                                
                                      =  nil()                              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys))
        - Weak DPs:
            insert#(x,l) -> c_21(insert#1#(l,x))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_21) = {1},
            uargs(c_22) = {1},
            uargs(c_25) = {1},
            uargs(c_26) = {1},
            uargs(c_27) = {1},
            uargs(c_30) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [1]                  
                          p(#EQ) = [5]                  
                          p(#GT) = [5]                  
                          p(#LT) = [5]                  
                         p(#abs) = [2]                  
                        p(#cklt) = [1] x1 + [1]         
                     p(#compare) = [5]                  
                       p(#false) = [6]                  
                        p(#less) = [6]                  
                         p(#neg) = [1] x1 + [0]         
                         p(#pos) = [2]                  
                           p(#s) = [0]                  
                        p(#true) = [6]                  
                           p(dd) = [1] x2 + [4]         
                       p(insert) = [1] x2 + [4]         
                     p(insert#1) = [1] x1 + [4]         
                     p(insert#2) = [1] x1 + [1] x4 + [2]
                      p(insertD) = [1] x2 + [4]         
                    p(insertD#1) = [1] x1 + [4]         
                    p(insertD#2) = [1] x1 + [1] x4 + [2]
                p(insertionsort) = [1] x1 + [0]         
              p(insertionsort#1) = [1] x1 + [0]         
               p(insertionsortD) = [1] x1 + [0]         
             p(insertionsortD#1) = [1] x1 + [0]         
                          p(nil) = [0]                  
                        p(#abs#) = [1] x1 + [1]         
                       p(#cklt#) = [0]                  
                    p(#compare#) = [1] x1 + [1]         
                       p(#less#) = [1] x1 + [2]         
                      p(insert#) = [1] x2 + [4]         
                    p(insert#1#) = [1] x1 + [3]         
                    p(insert#2#) = [1] x1 + [1] x4 + [0]
                     p(insertD#) = [1] x2 + [3]         
                   p(insertD#1#) = [1] x1 + [5]         
                   p(insertD#2#) = [1] x1 + [1] x4 + [1]
               p(insertionsort#) = [1] x1 + [0]         
             p(insertionsort#1#) = [1] x1 + [0]         
              p(insertionsortD#) = [2] x1 + [1]         
            p(insertionsortD#1#) = [2] x1 + [1]         
                          p(c_1) = [1]                  
                          p(c_2) = [0]                  
                          p(c_3) = [1]                  
                          p(c_4) = [1]                  
                          p(c_5) = [1]                  
                          p(c_6) = [0]                  
                          p(c_7) = [0]                  
                          p(c_8) = [0]                  
                          p(c_9) = [0]                  
                         p(c_10) = [2]                  
                         p(c_11) = [0]                  
                         p(c_12) = [0]                  
                         p(c_13) = [4] x1 + [0]         
                         p(c_14) = [1]                  
                         p(c_15) = [4]                  
                         p(c_16) = [0]                  
                         p(c_17) = [2] x1 + [0]         
                         p(c_18) = [4]                  
                         p(c_19) = [1] x1 + [0]         
                         p(c_20) = [4] x1 + [1]         
                         p(c_21) = [1] x1 + [1]         
                         p(c_22) = [1] x1 + [0]         
                         p(c_23) = [1]                  
                         p(c_24) = [4]                  
                         p(c_25) = [1] x1 + [0]         
                         p(c_26) = [1] x1 + [3]         
                         p(c_27) = [1] x1 + [1]         
                         p(c_28) = [1]                  
                         p(c_29) = [0]                  
                         p(c_30) = [1] x1 + [4]         
                         p(c_31) = [1] x1 + [1]         
                         p(c_32) = [1] x1 + [1] x2 + [0]
                         p(c_33) = [0]                  
                         p(c_34) = [2] x1 + [1]         
                         p(c_35) = [1] x1 + [1] x2 + [1]
                         p(c_36) = [0]                  
          
          Following rules are strictly oriented:
              insert#1#(dd(y,ys),x) = [1] ys + [7]                       
                                    > [1] ys + [6]                       
                                    = c_22(insert#2#(#less(y,x),x,y,ys)) 
          
          insert#2#(#true(),x,y,ys) = [1] ys + [6]                       
                                    > [1] ys + [4]                       
                                    = c_25(insert#(x,ys))                
          
             insertD#1#(dd(y,ys),x) = [1] ys + [9]                       
                                    > [1] ys + [8]                       
                                    = c_27(insertD#2#(#less(y,x),x,y,ys))
          
          
          Following rules are (at-least) weakly oriented:
                         insert#(x,l) =  [1] l + [4]                   
                                      >= [1] l + [4]                   
                                      =  c_21(insert#1#(l,x))          
          
                        insertD#(x,l) =  [1] l + [3]                   
                                      >= [1] l + [8]                   
                                      =  c_26(insertD#1#(l,x))         
          
           insertD#2#(#true(),x,y,ys) =  [1] ys + [7]                  
                                      >= [1] ys + [7]                  
                                      =  c_30(insertD#(x,ys))          
          
                    insertionsort#(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1#(l)           
          
           insertionsort#1#(dd(x,xs)) =  [1] xs + [4]                  
                                      >= [1] xs + [4]                  
                                      =  insert#(x,insertionsort(xs))  
          
           insertionsort#1#(dd(x,xs)) =  [1] xs + [4]                  
                                      >= [1] xs + [0]                  
                                      =  insertionsort#(xs)            
          
                   insertionsortD#(l) =  [2] l + [1]                   
                                      >= [2] l + [1]                   
                                      =  insertionsortD#1#(l)          
          
          insertionsortD#1#(dd(x,xs)) =  [2] xs + [9]                  
                                      >= [1] xs + [3]                  
                                      =  insertD#(x,insertionsortD(xs))
          
          insertionsortD#1#(dd(x,xs)) =  [2] xs + [9]                  
                                      >= [2] xs + [1]                  
                                      =  insertionsortD#(xs)           
          
                         #cklt(#EQ()) =  [6]                           
                                      >= [6]                           
                                      =  #false()                      
          
                         #cklt(#GT()) =  [6]                           
                                      >= [6]                           
                                      =  #false()                      
          
                         #cklt(#LT()) =  [6]                           
                                      >= [6]                           
                                      =  #true()                       
          
                  #compare(#0(),#0()) =  [5]                           
                                      >= [5]                           
                                      =  #EQ()                         
          
               #compare(#0(),#neg(y)) =  [5]                           
                                      >= [5]                           
                                      =  #GT()                         
          
               #compare(#0(),#pos(y)) =  [5]                           
                                      >= [5]                           
                                      =  #LT()                         
          
                 #compare(#0(),#s(y)) =  [5]                           
                                      >= [5]                           
                                      =  #LT()                         
          
               #compare(#neg(x),#0()) =  [5]                           
                                      >= [5]                           
                                      =  #LT()                         
          
            #compare(#neg(x),#neg(y)) =  [5]                           
                                      >= [5]                           
                                      =  #compare(y,x)                 
          
            #compare(#neg(x),#pos(y)) =  [5]                           
                                      >= [5]                           
                                      =  #LT()                         
          
               #compare(#pos(x),#0()) =  [5]                           
                                      >= [5]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#neg(y)) =  [5]                           
                                      >= [5]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#pos(y)) =  [5]                           
                                      >= [5]                           
                                      =  #compare(x,y)                 
          
                 #compare(#s(x),#0()) =  [5]                           
                                      >= [5]                           
                                      =  #GT()                         
          
                #compare(#s(x),#s(y)) =  [5]                           
                                      >= [5]                           
                                      =  #compare(x,y)                 
          
                           #less(x,y) =  [6]                           
                                      >= [6]                           
                                      =  #cklt(#compare(x,y))          
          
                          insert(x,l) =  [1] l + [4]                   
                                      >= [1] l + [4]                   
                                      =  insert#1(l,x)                 
          
                 insert#1(dd(y,ys),x) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  insert#2(#less(y,x),x,y,ys)   
          
                    insert#1(nil(),x) =  [4]                           
                                      >= [4]                           
                                      =  dd(x,nil())                   
          
            insert#2(#false(),x,y,ys) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  dd(x,dd(y,ys))                
          
             insert#2(#true(),x,y,ys) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  dd(y,insert(x,ys))            
          
                         insertD(x,l) =  [1] l + [4]                   
                                      >= [1] l + [4]                   
                                      =  insertD#1(l,x)                
          
                insertD#1(dd(y,ys),x) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  insertD#2(#less(y,x),x,y,ys)  
          
                   insertD#1(nil(),x) =  [4]                           
                                      >= [4]                           
                                      =  dd(x,nil())                   
          
           insertD#2(#false(),x,y,ys) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  dd(x,dd(y,ys))                
          
            insertD#2(#true(),x,y,ys) =  [1] ys + [8]                  
                                      >= [1] ys + [8]                  
                                      =  dd(y,insertD(x,ys))           
          
                     insertionsort(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1(l)            
          
            insertionsort#1(dd(x,xs)) =  [1] xs + [4]                  
                                      >= [1] xs + [4]                  
                                      =  insert(x,insertionsort(xs))   
          
               insertionsort#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
                    insertionsortD(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsortD#1(l)           
          
           insertionsortD#1(dd(x,xs)) =  [1] xs + [4]                  
                                      >= [1] xs + [4]                  
                                      =  insertD(x,insertionsortD(xs)) 
          
              insertionsortD#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            insertD#(x,l) -> c_26(insertD#1#(l,x))
        - Weak DPs:
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_21) = {1},
            uargs(c_22) = {1},
            uargs(c_25) = {1},
            uargs(c_26) = {1},
            uargs(c_27) = {1},
            uargs(c_30) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [2]                  
                          p(#EQ) = [0]                  
                          p(#GT) = [0]                  
                          p(#LT) = [0]                  
                         p(#abs) = [1] x1 + [1]         
                        p(#cklt) = [1] x1 + [0]         
                     p(#compare) = [0]                  
                       p(#false) = [0]                  
                        p(#less) = [0]                  
                         p(#neg) = [0]                  
                         p(#pos) = [1] x1 + [0]         
                           p(#s) = [1] x1 + [0]         
                        p(#true) = [0]                  
                           p(dd) = [1] x2 + [2]         
                       p(insert) = [1] x2 + [2]         
                     p(insert#1) = [1] x1 + [2]         
                     p(insert#2) = [1] x1 + [1] x4 + [4]
                      p(insertD) = [1] x2 + [2]         
                    p(insertD#1) = [1] x1 + [2]         
                    p(insertD#2) = [1] x1 + [1] x4 + [4]
                p(insertionsort) = [4] x1 + [1]         
              p(insertionsort#1) = [4] x1 + [0]         
               p(insertionsortD) = [1] x1 + [0]         
             p(insertionsortD#1) = [1] x1 + [0]         
                          p(nil) = [0]                  
                        p(#abs#) = [0]                  
                       p(#cklt#) = [1] x1 + [4]         
                    p(#compare#) = [1] x2 + [1]         
                       p(#less#) = [4] x2 + [4]         
                      p(insert#) = [1] x2 + [0]         
                    p(insert#1#) = [1] x1 + [0]         
                    p(insert#2#) = [1] x1 + [1] x4 + [1]
                     p(insertD#) = [1] x2 + [3]         
                   p(insertD#1#) = [1] x1 + [2]         
                   p(insertD#2#) = [1] x1 + [1] x4 + [4]
               p(insertionsort#) = [4] x1 + [4]         
             p(insertionsort#1#) = [4] x1 + [3]         
              p(insertionsortD#) = [1] x1 + [1]         
            p(insertionsortD#1#) = [1] x1 + [1]         
                          p(c_1) = [1]                  
                          p(c_2) = [1]                  
                          p(c_3) = [1]                  
                          p(c_4) = [2]                  
                          p(c_5) = [0]                  
                          p(c_6) = [1]                  
                          p(c_7) = [0]                  
                          p(c_8) = [2]                  
                          p(c_9) = [0]                  
                         p(c_10) = [0]                  
                         p(c_11) = [1]                  
                         p(c_12) = [2]                  
                         p(c_13) = [4] x1 + [2]         
                         p(c_14) = [1]                  
                         p(c_15) = [0]                  
                         p(c_16) = [1]                  
                         p(c_17) = [0]                  
                         p(c_18) = [0]                  
                         p(c_19) = [1] x1 + [0]         
                         p(c_20) = [0]                  
                         p(c_21) = [1] x1 + [0]         
                         p(c_22) = [1] x1 + [1]         
                         p(c_23) = [2]                  
                         p(c_24) = [0]                  
                         p(c_25) = [1] x1 + [1]         
                         p(c_26) = [1] x1 + [0]         
                         p(c_27) = [1] x1 + [0]         
                         p(c_28) = [1]                  
                         p(c_29) = [0]                  
                         p(c_30) = [1] x1 + [1]         
                         p(c_31) = [1] x1 + [0]         
                         p(c_32) = [2] x2 + [2]         
                         p(c_33) = [1]                  
                         p(c_34) = [1] x1 + [4]         
                         p(c_35) = [4] x1 + [2] x2 + [0]
                         p(c_36) = [0]                  
          
          Following rules are strictly oriented:
          insertD#(x,l) = [1] l + [3]          
                        > [1] l + [2]          
                        = c_26(insertD#1#(l,x))
          
          
          Following rules are (at-least) weakly oriented:
                         insert#(x,l) =  [1] l + [0]                        
                                      >= [1] l + [0]                        
                                      =  c_21(insert#1#(l,x))               
          
                insert#1#(dd(y,ys),x) =  [1] ys + [2]                       
                                      >= [1] ys + [2]                       
                                      =  c_22(insert#2#(#less(y,x),x,y,ys)) 
          
            insert#2#(#true(),x,y,ys) =  [1] ys + [1]                       
                                      >= [1] ys + [1]                       
                                      =  c_25(insert#(x,ys))                
          
               insertD#1#(dd(y,ys),x) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  c_27(insertD#2#(#less(y,x),x,y,ys))
          
           insertD#2#(#true(),x,y,ys) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  c_30(insertD#(x,ys))               
          
                    insertionsort#(l) =  [4] l + [4]                        
                                      >= [4] l + [3]                        
                                      =  insertionsort#1#(l)                
          
           insertionsort#1#(dd(x,xs)) =  [4] xs + [11]                      
                                      >= [4] xs + [1]                       
                                      =  insert#(x,insertionsort(xs))       
          
           insertionsort#1#(dd(x,xs)) =  [4] xs + [11]                      
                                      >= [4] xs + [4]                       
                                      =  insertionsort#(xs)                 
          
                   insertionsortD#(l) =  [1] l + [1]                        
                                      >= [1] l + [1]                        
                                      =  insertionsortD#1#(l)               
          
          insertionsortD#1#(dd(x,xs)) =  [1] xs + [3]                       
                                      >= [1] xs + [3]                       
                                      =  insertD#(x,insertionsortD(xs))     
          
          insertionsortD#1#(dd(x,xs)) =  [1] xs + [3]                       
                                      >= [1] xs + [1]                       
                                      =  insertionsortD#(xs)                
          
                         #cklt(#EQ()) =  [0]                                
                                      >= [0]                                
                                      =  #false()                           
          
                         #cklt(#GT()) =  [0]                                
                                      >= [0]                                
                                      =  #false()                           
          
                         #cklt(#LT()) =  [0]                                
                                      >= [0]                                
                                      =  #true()                            
          
                  #compare(#0(),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #EQ()                              
          
               #compare(#0(),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
               #compare(#0(),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
                 #compare(#0(),#s(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
               #compare(#neg(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
            #compare(#neg(x),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(y,x)                      
          
            #compare(#neg(x),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #LT()                              
          
               #compare(#pos(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
            #compare(#pos(x),#neg(y)) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
            #compare(#pos(x),#pos(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(x,y)                      
          
                 #compare(#s(x),#0()) =  [0]                                
                                      >= [0]                                
                                      =  #GT()                              
          
                #compare(#s(x),#s(y)) =  [0]                                
                                      >= [0]                                
                                      =  #compare(x,y)                      
          
                           #less(x,y) =  [0]                                
                                      >= [0]                                
                                      =  #cklt(#compare(x,y))               
          
                          insert(x,l) =  [1] l + [2]                        
                                      >= [1] l + [2]                        
                                      =  insert#1(l,x)                      
          
                 insert#1(dd(y,ys),x) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  insert#2(#less(y,x),x,y,ys)        
          
                    insert#1(nil(),x) =  [2]                                
                                      >= [2]                                
                                      =  dd(x,nil())                        
          
            insert#2(#false(),x,y,ys) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  dd(x,dd(y,ys))                     
          
             insert#2(#true(),x,y,ys) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  dd(y,insert(x,ys))                 
          
                         insertD(x,l) =  [1] l + [2]                        
                                      >= [1] l + [2]                        
                                      =  insertD#1(l,x)                     
          
                insertD#1(dd(y,ys),x) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  insertD#2(#less(y,x),x,y,ys)       
          
                   insertD#1(nil(),x) =  [2]                                
                                      >= [2]                                
                                      =  dd(x,nil())                        
          
           insertD#2(#false(),x,y,ys) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  dd(x,dd(y,ys))                     
          
            insertD#2(#true(),x,y,ys) =  [1] ys + [4]                       
                                      >= [1] ys + [4]                       
                                      =  dd(y,insertD(x,ys))                
          
                     insertionsort(l) =  [4] l + [1]                        
                                      >= [4] l + [0]                        
                                      =  insertionsort#1(l)                 
          
            insertionsort#1(dd(x,xs)) =  [4] xs + [8]                       
                                      >= [4] xs + [3]                       
                                      =  insert(x,insertionsort(xs))        
          
               insertionsort#1(nil()) =  [0]                                
                                      >= [0]                                
                                      =  nil()                              
          
                    insertionsortD(l) =  [1] l + [0]                        
                                      >= [1] l + [0]                        
                                      =  insertionsortD#1(l)                
          
           insertionsortD#1(dd(x,xs)) =  [1] xs + [2]                       
                                      >= [1] xs + [2]                       
                                      =  insertD(x,insertionsortD(xs))      
          
              insertionsortD#1(nil()) =  [0]                                
                                      >= [0]                                
                                      =  nil()                              
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            insert#(x,l) -> c_21(insert#1#(l,x))
            insert#1#(dd(y,ys),x) -> c_22(insert#2#(#less(y,x),x,y,ys))
            insert#2#(#true(),x,y,ys) -> c_25(insert#(x,ys))
            insertD#(x,l) -> c_26(insertD#1#(l,x))
            insertD#1#(dd(y,ys),x) -> c_27(insertD#2#(#less(y,x),x,y,ys))
            insertD#2#(#true(),x,y,ys) -> c_30(insertD#(x,ys))
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/1,c_27/1,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

*** Step 6.b:1.b:1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
        - Weak DPs:
            insert#(x,l) -> insert#1#(l,x)
            insert#1#(dd(y,ys),x) -> #less#(y,x)
            insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
            insert#2#(#true(),x,y,ys) -> insert#(x,ys)
            insertD#(x,l) -> insertD#1#(l,x)
            insertD#1#(dd(y,ys),x) -> #less#(y,x)
            insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
            insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_17) = {1},
            uargs(c_19) = {1},
            uargs(c_20) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                  
                          p(#EQ) = [0]                  
                          p(#GT) = [0]                  
                          p(#LT) = [0]                  
                         p(#abs) = [1] x1 + [2]         
                        p(#cklt) = [1] x1 + [0]         
                     p(#compare) = [0]                  
                       p(#false) = [0]                  
                        p(#less) = [0]                  
                         p(#neg) = [2]                  
                         p(#pos) = [1] x1 + [0]         
                           p(#s) = [0]                  
                        p(#true) = [0]                  
                           p(dd) = [1] x2 + [0]         
                       p(insert) = [1] x2 + [0]         
                     p(insert#1) = [1] x1 + [0]         
                     p(insert#2) = [1] x1 + [1] x4 + [0]
                      p(insertD) = [1] x2 + [0]         
                    p(insertD#1) = [1] x1 + [0]         
                    p(insertD#2) = [1] x1 + [1] x4 + [0]
                p(insertionsort) = [0]                  
              p(insertionsort#1) = [0]                  
               p(insertionsortD) = [6]                  
             p(insertionsortD#1) = [6]                  
                          p(nil) = [0]                  
                        p(#abs#) = [4]                  
                       p(#cklt#) = [2] x1 + [1]         
                    p(#compare#) = [0]                  
                       p(#less#) = [1]                  
                      p(insert#) = [1] x2 + [2]         
                    p(insert#1#) = [1] x1 + [2]         
                    p(insert#2#) = [1] x1 + [1] x4 + [2]
                     p(insertD#) = [1] x2 + [1]         
                   p(insertD#1#) = [1] x1 + [1]         
                   p(insertD#2#) = [1] x1 + [1] x4 + [1]
               p(insertionsort#) = [1] x1 + [2]         
             p(insertionsort#1#) = [1] x1 + [2]         
              p(insertionsortD#) = [7]                  
            p(insertionsortD#1#) = [7]                  
                          p(c_1) = [1]                  
                          p(c_2) = [0]                  
                          p(c_3) = [4]                  
                          p(c_4) = [0]                  
                          p(c_5) = [1]                  
                          p(c_6) = [2]                  
                          p(c_7) = [0]                  
                          p(c_8) = [0]                  
                          p(c_9) = [1]                  
                         p(c_10) = [1]                  
                         p(c_11) = [0]                  
                         p(c_12) = [1]                  
                         p(c_13) = [1] x1 + [2]         
                         p(c_14) = [0]                  
                         p(c_15) = [0]                  
                         p(c_16) = [1]                  
                         p(c_17) = [1] x1 + [0]         
                         p(c_18) = [1]                  
                         p(c_19) = [1] x1 + [0]         
                         p(c_20) = [1] x1 + [0]         
                         p(c_21) = [2] x1 + [4]         
                         p(c_22) = [2] x1 + [1]         
                         p(c_23) = [1]                  
                         p(c_24) = [0]                  
                         p(c_25) = [0]                  
                         p(c_26) = [1] x1 + [0]         
                         p(c_27) = [4] x1 + [2]         
                         p(c_28) = [4]                  
                         p(c_29) = [0]                  
                         p(c_30) = [1] x1 + [0]         
                         p(c_31) = [1]                  
                         p(c_32) = [1]                  
                         p(c_33) = [0]                  
                         p(c_34) = [1] x1 + [1]         
                         p(c_35) = [1] x1 + [0]         
                         p(c_36) = [1]                  
          
          Following rules are strictly oriented:
          #less#(x,y) = [1]                 
                      > [0]                 
                      = c_20(#compare#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
           #compare#(#neg(x),#neg(y)) =  [0]                           
                                      >= [2]                           
                                      =  c_13(#compare#(y,x))          
          
           #compare#(#pos(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  c_17(#compare#(x,y))          
          
               #compare#(#s(x),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  c_19(#compare#(x,y))          
          
                         insert#(x,l) =  [1] l + [2]                   
                                      >= [1] l + [2]                   
                                      =  insert#1#(l,x)                
          
                insert#1#(dd(y,ys),x) =  [1] ys + [2]                  
                                      >= [1]                           
                                      =  #less#(y,x)                   
          
                insert#1#(dd(y,ys),x) =  [1] ys + [2]                  
                                      >= [1] ys + [2]                  
                                      =  insert#2#(#less(y,x),x,y,ys)  
          
            insert#2#(#true(),x,y,ys) =  [1] ys + [2]                  
                                      >= [1] ys + [2]                  
                                      =  insert#(x,ys)                 
          
                        insertD#(x,l) =  [1] l + [1]                   
                                      >= [1] l + [1]                   
                                      =  insertD#1#(l,x)               
          
               insertD#1#(dd(y,ys),x) =  [1] ys + [1]                  
                                      >= [1]                           
                                      =  #less#(y,x)                   
          
               insertD#1#(dd(y,ys),x) =  [1] ys + [1]                  
                                      >= [1] ys + [1]                  
                                      =  insertD#2#(#less(y,x),x,y,ys) 
          
           insertD#2#(#true(),x,y,ys) =  [1] ys + [1]                  
                                      >= [1] ys + [1]                  
                                      =  insertD#(x,ys)                
          
                    insertionsort#(l) =  [1] l + [2]                   
                                      >= [1] l + [2]                   
                                      =  insertionsort#1#(l)           
          
           insertionsort#1#(dd(x,xs)) =  [1] xs + [2]                  
                                      >= [2]                           
                                      =  insert#(x,insertionsort(xs))  
          
           insertionsort#1#(dd(x,xs)) =  [1] xs + [2]                  
                                      >= [1] xs + [2]                  
                                      =  insertionsort#(xs)            
          
                   insertionsortD#(l) =  [7]                           
                                      >= [7]                           
                                      =  insertionsortD#1#(l)          
          
          insertionsortD#1#(dd(x,xs)) =  [7]                           
                                      >= [7]                           
                                      =  insertD#(x,insertionsortD(xs))
          
          insertionsortD#1#(dd(x,xs)) =  [7]                           
                                      >= [7]                           
                                      =  insertionsortD#(xs)           
          
                         #cklt(#EQ()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#GT()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#LT()) =  [0]                           
                                      >= [0]                           
                                      =  #true()                       
          
                  #compare(#0(),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #EQ()                         
          
               #compare(#0(),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
               #compare(#0(),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
                 #compare(#0(),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#neg(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
            #compare(#neg(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(y,x)                 
          
            #compare(#neg(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#pos(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                 #compare(#s(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
                #compare(#s(x),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                           #less(x,y) =  [0]                           
                                      >= [0]                           
                                      =  #cklt(#compare(x,y))          
          
                          insert(x,l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insert#1(l,x)                 
          
                 insert#1(dd(y,ys),x) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  insert#2(#less(y,x),x,y,ys)   
          
                    insert#1(nil(),x) =  [0]                           
                                      >= [0]                           
                                      =  dd(x,nil())                   
          
            insert#2(#false(),x,y,ys) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  dd(x,dd(y,ys))                
          
             insert#2(#true(),x,y,ys) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  dd(y,insert(x,ys))            
          
                         insertD(x,l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertD#1(l,x)                
          
                insertD#1(dd(y,ys),x) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  insertD#2(#less(y,x),x,y,ys)  
          
                   insertD#1(nil(),x) =  [0]                           
                                      >= [0]                           
                                      =  dd(x,nil())                   
          
           insertD#2(#false(),x,y,ys) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  dd(x,dd(y,ys))                
          
            insertD#2(#true(),x,y,ys) =  [1] ys + [0]                  
                                      >= [1] ys + [0]                  
                                      =  dd(y,insertD(x,ys))           
          
                     insertionsort(l) =  [0]                           
                                      >= [0]                           
                                      =  insertionsort#1(l)            
          
            insertionsort#1(dd(x,xs)) =  [0]                           
                                      >= [0]                           
                                      =  insert(x,insertionsort(xs))   
          
               insertionsort#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
                    insertionsortD(l) =  [6]                           
                                      >= [6]                           
                                      =  insertionsortD#1(l)           
          
           insertionsortD#1(dd(x,xs)) =  [6]                           
                                      >= [6]                           
                                      =  insertD(x,insertionsortD(xs)) 
          
              insertionsortD#1(nil()) =  [6]                           
                                      >= [0]                           
                                      =  nil()                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.b:2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
        - Weak DPs:
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> insert#1#(l,x)
            insert#1#(dd(y,ys),x) -> #less#(y,x)
            insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
            insert#2#(#true(),x,y,ys) -> insert#(x,ys)
            insertD#(x,l) -> insertD#1#(l,x)
            insertD#1#(dd(y,ys),x) -> #less#(y,x)
            insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
            insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_17) = {1},
            uargs(c_19) = {1},
            uargs(c_20) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [2]                                    
                          p(#EQ) = [0]                                    
                          p(#GT) = [0]                                    
                          p(#LT) = [0]                                    
                         p(#abs) = [1] x1 + [1]                           
                        p(#cklt) = [1] x1 + [0]                           
                     p(#compare) = [0]                                    
                       p(#false) = [0]                                    
                        p(#less) = [0]                                    
                         p(#neg) = [1] x1 + [0]                           
                         p(#pos) = [1] x1 + [0]                           
                           p(#s) = [1] x1 + [1]                           
                        p(#true) = [0]                                    
                           p(dd) = [1] x1 + [1] x2 + [0]                  
                       p(insert) = [1] x1 + [1] x2 + [0]                  
                     p(insert#1) = [1] x1 + [1] x2 + [0]                  
                     p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                      p(insertD) = [1] x1 + [1] x2 + [0]                  
                    p(insertD#1) = [1] x1 + [1] x2 + [0]                  
                    p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                p(insertionsort) = [1] x1 + [0]                           
              p(insertionsort#1) = [1] x1 + [0]                           
               p(insertionsortD) = [2] x1 + [0]                           
             p(insertionsortD#1) = [2] x1 + [0]                           
                          p(nil) = [3]                                    
                        p(#abs#) = [4] x1 + [1]                           
                       p(#cklt#) = [4]                                    
                    p(#compare#) = [1] x1 + [1] x2 + [0]                  
                       p(#less#) = [1] x1 + [1] x2 + [0]                  
                      p(insert#) = [1] x1 + [1] x2 + [0]                  
                    p(insert#1#) = [1] x1 + [1] x2 + [0]                  
                    p(insert#2#) = [1] x1 + [1] x2 + [1] x4 + [0]         
                     p(insertD#) = [1] x1 + [1] x2 + [0]                  
                   p(insertD#1#) = [1] x1 + [1] x2 + [0]                  
                   p(insertD#2#) = [1] x1 + [1] x2 + [1] x4 + [0]         
               p(insertionsort#) = [2] x1 + [0]                           
             p(insertionsort#1#) = [2] x1 + [0]                           
              p(insertionsortD#) = [3] x1 + [3]                           
            p(insertionsortD#1#) = [3] x1 + [3]                           
                          p(c_1) = [0]                                    
                          p(c_2) = [4]                                    
                          p(c_3) = [1]                                    
                          p(c_4) = [2]                                    
                          p(c_5) = [0]                                    
                          p(c_6) = [0]                                    
                          p(c_7) = [0]                                    
                          p(c_8) = [1]                                    
                          p(c_9) = [0]                                    
                         p(c_10) = [0]                                    
                         p(c_11) = [2]                                    
                         p(c_12) = [4]                                    
                         p(c_13) = [1] x1 + [0]                           
                         p(c_14) = [1]                                    
                         p(c_15) = [1]                                    
                         p(c_16) = [0]                                    
                         p(c_17) = [1] x1 + [3]                           
                         p(c_18) = [0]                                    
                         p(c_19) = [1] x1 + [0]                           
                         p(c_20) = [1] x1 + [0]                           
                         p(c_21) = [1] x1 + [0]                           
                         p(c_22) = [1] x1 + [2] x2 + [0]                  
                         p(c_23) = [2]                                    
                         p(c_24) = [0]                                    
                         p(c_25) = [2] x1 + [1]                           
                         p(c_26) = [2] x1 + [0]                           
                         p(c_27) = [2] x1 + [1] x2 + [1]                  
                         p(c_28) = [2]                                    
                         p(c_29) = [1]                                    
                         p(c_30) = [2] x1 + [4]                           
                         p(c_31) = [4] x1 + [0]                           
                         p(c_32) = [1] x1 + [4] x2 + [0]                  
                         p(c_33) = [4]                                    
                         p(c_34) = [4] x1 + [1]                           
                         p(c_35) = [4] x1 + [1] x2 + [1]                  
                         p(c_36) = [0]                                    
          
          Following rules are strictly oriented:
          #compare#(#s(x),#s(y)) = [1] x + [1] y + [2] 
                                 > [1] x + [1] y + [0] 
                                 = c_19(#compare#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
           #compare#(#neg(x),#neg(y)) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_13(#compare#(y,x))          
          
           #compare#(#pos(x),#pos(y)) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [3]           
                                      =  c_17(#compare#(x,y))          
          
                          #less#(x,y) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_20(#compare#(x,y))          
          
                         insert#(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insert#1#(l,x)                
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] ys + [0]          
                                      =  insert#2#(#less(y,x),x,y,ys)  
          
            insert#2#(#true(),x,y,ys) =  [1] x + [1] ys + [0]          
                                      >= [1] x + [1] ys + [0]          
                                      =  insert#(x,ys)                 
          
                        insertD#(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insertD#1#(l,x)               
          
               insertD#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
               insertD#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] ys + [0]          
                                      =  insertD#2#(#less(y,x),x,y,ys) 
          
           insertD#2#(#true(),x,y,ys) =  [1] x + [1] ys + [0]          
                                      >= [1] x + [1] ys + [0]          
                                      =  insertD#(x,ys)                
          
                    insertionsort#(l) =  [2] l + [0]                   
                                      >= [2] l + [0]                   
                                      =  insertionsort#1#(l)           
          
           insertionsort#1#(dd(x,xs)) =  [2] x + [2] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insert#(x,insertionsort(xs))  
          
           insertionsort#1#(dd(x,xs)) =  [2] x + [2] xs + [0]          
                                      >= [2] xs + [0]                  
                                      =  insertionsort#(xs)            
          
                   insertionsortD#(l) =  [3] l + [3]                   
                                      >= [3] l + [3]                   
                                      =  insertionsortD#1#(l)          
          
          insertionsortD#1#(dd(x,xs)) =  [3] x + [3] xs + [3]          
                                      >= [1] x + [2] xs + [0]          
                                      =  insertD#(x,insertionsortD(xs))
          
          insertionsortD#1#(dd(x,xs)) =  [3] x + [3] xs + [3]          
                                      >= [3] xs + [3]                  
                                      =  insertionsortD#(xs)           
          
                         #cklt(#EQ()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#GT()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#LT()) =  [0]                           
                                      >= [0]                           
                                      =  #true()                       
          
                  #compare(#0(),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #EQ()                         
          
               #compare(#0(),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
               #compare(#0(),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
                 #compare(#0(),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#neg(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
            #compare(#neg(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(y,x)                 
          
            #compare(#neg(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#pos(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                 #compare(#s(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
                #compare(#s(x),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                           #less(x,y) =  [0]                           
                                      >= [0]                           
                                      =  #cklt(#compare(x,y))          
          
                          insert(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insert#1(l,x)                 
          
                 insert#1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  insert#2(#less(y,x),x,y,ys)   
          
                    insert#1(nil(),x) =  [1] x + [3]                   
                                      >= [1] x + [3]                   
                                      =  dd(x,nil())                   
          
            insert#2(#false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
             insert#2(#true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insert(x,ys))            
          
                         insertD(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insertD#1(l,x)                
          
                insertD#1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  insertD#2(#less(y,x),x,y,ys)  
          
                   insertD#1(nil(),x) =  [1] x + [3]                   
                                      >= [1] x + [3]                   
                                      =  dd(x,nil())                   
          
           insertD#2(#false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
            insertD#2(#true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insertD(x,ys))           
          
                     insertionsort(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1(l)            
          
            insertionsort#1(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insert(x,insertionsort(xs))   
          
               insertionsort#1(nil()) =  [3]                           
                                      >= [3]                           
                                      =  nil()                         
          
                    insertionsortD(l) =  [2] l + [0]                   
                                      >= [2] l + [0]                   
                                      =  insertionsortD#1(l)           
          
           insertionsortD#1(dd(x,xs)) =  [2] x + [2] xs + [0]          
                                      >= [1] x + [2] xs + [0]          
                                      =  insertD(x,insertionsortD(xs)) 
          
              insertionsortD#1(nil()) =  [6]                           
                                      >= [3]                           
                                      =  nil()                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.b:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
        - Weak DPs:
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> insert#1#(l,x)
            insert#1#(dd(y,ys),x) -> #less#(y,x)
            insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
            insert#2#(#true(),x,y,ys) -> insert#(x,ys)
            insertD#(x,l) -> insertD#1#(l,x)
            insertD#1#(dd(y,ys),x) -> #less#(y,x)
            insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
            insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_17) = {1},
            uargs(c_19) = {1},
            uargs(c_20) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [2]                                    
                          p(#EQ) = [0]                                    
                          p(#GT) = [0]                                    
                          p(#LT) = [0]                                    
                         p(#abs) = [2] x1 + [1]                           
                        p(#cklt) = [1] x1 + [0]                           
                     p(#compare) = [0]                                    
                       p(#false) = [0]                                    
                        p(#less) = [0]                                    
                         p(#neg) = [1] x1 + [1]                           
                         p(#pos) = [1] x1 + [0]                           
                           p(#s) = [1] x1 + [4]                           
                        p(#true) = [0]                                    
                           p(dd) = [1] x1 + [1] x2 + [0]                  
                       p(insert) = [1] x1 + [1] x2 + [0]                  
                     p(insert#1) = [1] x1 + [1] x2 + [0]                  
                     p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                      p(insertD) = [1] x1 + [1] x2 + [0]                  
                    p(insertD#1) = [1] x1 + [1] x2 + [0]                  
                    p(insertD#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                p(insertionsort) = [1] x1 + [0]                           
              p(insertionsort#1) = [1] x1 + [0]                           
               p(insertionsortD) = [1] x1 + [0]                           
             p(insertionsortD#1) = [1] x1 + [0]                           
                          p(nil) = [0]                                    
                        p(#abs#) = [1]                                    
                       p(#cklt#) = [0]                                    
                    p(#compare#) = [1] x1 + [1] x2 + [0]                  
                       p(#less#) = [1] x1 + [1] x2 + [0]                  
                      p(insert#) = [1] x1 + [1] x2 + [0]                  
                    p(insert#1#) = [1] x1 + [1] x2 + [0]                  
                    p(insert#2#) = [1] x1 + [1] x2 + [1] x4 + [0]         
                     p(insertD#) = [2] x1 + [1] x2 + [0]                  
                   p(insertD#1#) = [1] x1 + [2] x2 + [0]                  
                   p(insertD#2#) = [1] x1 + [2] x2 + [1] x3 + [1] x4 + [0]
               p(insertionsort#) = [1] x1 + [0]                           
             p(insertionsort#1#) = [1] x1 + [0]                           
              p(insertionsortD#) = [4] x1 + [0]                           
            p(insertionsortD#1#) = [4] x1 + [0]                           
                          p(c_1) = [0]                                    
                          p(c_2) = [0]                                    
                          p(c_3) = [0]                                    
                          p(c_4) = [1]                                    
                          p(c_5) = [1]                                    
                          p(c_6) = [1]                                    
                          p(c_7) = [1]                                    
                          p(c_8) = [0]                                    
                          p(c_9) = [2]                                    
                         p(c_10) = [1]                                    
                         p(c_11) = [0]                                    
                         p(c_12) = [1]                                    
                         p(c_13) = [1] x1 + [0]                           
                         p(c_14) = [0]                                    
                         p(c_15) = [0]                                    
                         p(c_16) = [2]                                    
                         p(c_17) = [1] x1 + [1]                           
                         p(c_18) = [1]                                    
                         p(c_19) = [1] x1 + [2]                           
                         p(c_20) = [1] x1 + [0]                           
                         p(c_21) = [1]                                    
                         p(c_22) = [1] x1 + [2] x2 + [0]                  
                         p(c_23) = [0]                                    
                         p(c_24) = [1]                                    
                         p(c_25) = [0]                                    
                         p(c_26) = [1]                                    
                         p(c_27) = [2] x1 + [1] x2 + [0]                  
                         p(c_28) = [4]                                    
                         p(c_29) = [0]                                    
                         p(c_30) = [1] x1 + [0]                           
                         p(c_31) = [0]                                    
                         p(c_32) = [1]                                    
                         p(c_33) = [1]                                    
                         p(c_34) = [1]                                    
                         p(c_35) = [1] x2 + [1]                           
                         p(c_36) = [4]                                    
          
          Following rules are strictly oriented:
          #compare#(#neg(x),#neg(y)) = [1] x + [1] y + [2] 
                                     > [1] x + [1] y + [0] 
                                     = c_13(#compare#(y,x))
          
          
          Following rules are (at-least) weakly oriented:
           #compare#(#pos(x),#pos(y)) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [1]           
                                      =  c_17(#compare#(x,y))          
          
               #compare#(#s(x),#s(y)) =  [1] x + [1] y + [8]           
                                      >= [1] x + [1] y + [2]           
                                      =  c_19(#compare#(x,y))          
          
                          #less#(x,y) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_20(#compare#(x,y))          
          
                         insert#(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insert#1#(l,x)                
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] ys + [0]          
                                      =  insert#2#(#less(y,x),x,y,ys)  
          
            insert#2#(#true(),x,y,ys) =  [1] x + [1] ys + [0]          
                                      >= [1] x + [1] ys + [0]          
                                      =  insert#(x,ys)                 
          
                        insertD#(x,l) =  [1] l + [2] x + [0]           
                                      >= [1] l + [2] x + [0]           
                                      =  insertD#1#(l,x)               
          
               insertD#1#(dd(y,ys),x) =  [2] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
               insertD#1#(dd(y,ys),x) =  [2] x + [1] y + [1] ys + [0]  
                                      >= [2] x + [1] y + [1] ys + [0]  
                                      =  insertD#2#(#less(y,x),x,y,ys) 
          
           insertD#2#(#true(),x,y,ys) =  [2] x + [1] y + [1] ys + [0]  
                                      >= [2] x + [1] ys + [0]          
                                      =  insertD#(x,ys)                
          
                    insertionsort#(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1#(l)           
          
           insertionsort#1#(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insert#(x,insertionsort(xs))  
          
           insertionsort#1#(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] xs + [0]                  
                                      =  insertionsort#(xs)            
          
                   insertionsortD#(l) =  [4] l + [0]                   
                                      >= [4] l + [0]                   
                                      =  insertionsortD#1#(l)          
          
          insertionsortD#1#(dd(x,xs)) =  [4] x + [4] xs + [0]          
                                      >= [2] x + [1] xs + [0]          
                                      =  insertD#(x,insertionsortD(xs))
          
          insertionsortD#1#(dd(x,xs)) =  [4] x + [4] xs + [0]          
                                      >= [4] xs + [0]                  
                                      =  insertionsortD#(xs)           
          
                         #cklt(#EQ()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#GT()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#LT()) =  [0]                           
                                      >= [0]                           
                                      =  #true()                       
          
                  #compare(#0(),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #EQ()                         
          
               #compare(#0(),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
               #compare(#0(),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
                 #compare(#0(),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#neg(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
            #compare(#neg(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(y,x)                 
          
            #compare(#neg(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#pos(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                 #compare(#s(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
                #compare(#s(x),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                           #less(x,y) =  [0]                           
                                      >= [0]                           
                                      =  #cklt(#compare(x,y))          
          
                          insert(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insert#1(l,x)                 
          
                 insert#1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  insert#2(#less(y,x),x,y,ys)   
          
                    insert#1(nil(),x) =  [1] x + [0]                   
                                      >= [1] x + [0]                   
                                      =  dd(x,nil())                   
          
            insert#2(#false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
             insert#2(#true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insert(x,ys))            
          
                         insertD(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insertD#1(l,x)                
          
                insertD#1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  insertD#2(#less(y,x),x,y,ys)  
          
                   insertD#1(nil(),x) =  [1] x + [0]                   
                                      >= [1] x + [0]                   
                                      =  dd(x,nil())                   
          
           insertD#2(#false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
            insertD#2(#true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insertD(x,ys))           
          
                     insertionsort(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1(l)            
          
            insertionsort#1(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insert(x,insertionsort(xs))   
          
               insertionsort#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
                    insertionsortD(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsortD#1(l)           
          
           insertionsortD#1(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insertD(x,insertionsortD(xs)) 
          
              insertionsortD#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.b:4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
        - Weak DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> insert#1#(l,x)
            insert#1#(dd(y,ys),x) -> #less#(y,x)
            insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
            insert#2#(#true(),x,y,ys) -> insert#(x,ys)
            insertD#(x,l) -> insertD#1#(l,x)
            insertD#1#(dd(y,ys),x) -> #less#(y,x)
            insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
            insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(#cklt) = {1},
            uargs(dd) = {2},
            uargs(insert) = {2},
            uargs(insert#2) = {1},
            uargs(insertD) = {2},
            uargs(insertD#2) = {1},
            uargs(insert#) = {2},
            uargs(insert#2#) = {1},
            uargs(insertD#) = {2},
            uargs(insertD#2#) = {1},
            uargs(c_13) = {1},
            uargs(c_17) = {1},
            uargs(c_19) = {1},
            uargs(c_20) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                           p(#0) = [0]                                    
                          p(#EQ) = [0]                                    
                          p(#GT) = [0]                                    
                          p(#LT) = [0]                                    
                         p(#abs) = [1] x1 + [1]                           
                        p(#cklt) = [1] x1 + [0]                           
                     p(#compare) = [0]                                    
                       p(#false) = [0]                                    
                        p(#less) = [0]                                    
                         p(#neg) = [1] x1 + [0]                           
                         p(#pos) = [1] x1 + [1]                           
                           p(#s) = [1] x1 + [0]                           
                        p(#true) = [0]                                    
                           p(dd) = [1] x1 + [1] x2 + [0]                  
                       p(insert) = [1] x1 + [1] x2 + [0]                  
                     p(insert#1) = [1] x1 + [1] x2 + [0]                  
                     p(insert#2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                      p(insertD) = [4] x1 + [1] x2 + [0]                  
                    p(insertD#1) = [1] x1 + [4] x2 + [0]                  
                    p(insertD#2) = [1] x1 + [4] x2 + [1] x3 + [1] x4 + [0]
                p(insertionsort) = [1] x1 + [0]                           
              p(insertionsort#1) = [1] x1 + [0]                           
               p(insertionsortD) = [6] x1 + [0]                           
             p(insertionsortD#1) = [6] x1 + [0]                           
                          p(nil) = [0]                                    
                        p(#abs#) = [4]                                    
                       p(#cklt#) = [4] x1 + [0]                           
                    p(#compare#) = [1] x1 + [1] x2 + [0]                  
                       p(#less#) = [1] x1 + [1] x2 + [0]                  
                      p(insert#) = [1] x1 + [1] x2 + [2]                  
                    p(insert#1#) = [1] x1 + [1] x2 + [2]                  
                    p(insert#2#) = [1] x1 + [1] x2 + [1] x4 + [2]         
                     p(insertD#) = [1] x1 + [1] x2 + [0]                  
                   p(insertD#1#) = [1] x1 + [1] x2 + [0]                  
                   p(insertD#2#) = [1] x1 + [1] x2 + [1] x4 + [0]         
               p(insertionsort#) = [2] x1 + [2]                           
             p(insertionsort#1#) = [2] x1 + [2]                           
              p(insertionsortD#) = [6] x1 + [0]                           
            p(insertionsortD#1#) = [6] x1 + [0]                           
                          p(c_1) = [0]                                    
                          p(c_2) = [2]                                    
                          p(c_3) = [2]                                    
                          p(c_4) = [1]                                    
                          p(c_5) = [0]                                    
                          p(c_6) = [1]                                    
                          p(c_7) = [0]                                    
                          p(c_8) = [1]                                    
                          p(c_9) = [0]                                    
                         p(c_10) = [4]                                    
                         p(c_11) = [0]                                    
                         p(c_12) = [1]                                    
                         p(c_13) = [1] x1 + [0]                           
                         p(c_14) = [1]                                    
                         p(c_15) = [2]                                    
                         p(c_16) = [1]                                    
                         p(c_17) = [1] x1 + [0]                           
                         p(c_18) = [0]                                    
                         p(c_19) = [1] x1 + [0]                           
                         p(c_20) = [1] x1 + [0]                           
                         p(c_21) = [4] x1 + [0]                           
                         p(c_22) = [2] x1 + [2] x2 + [1]                  
                         p(c_23) = [2]                                    
                         p(c_24) = [0]                                    
                         p(c_25) = [1] x1 + [1]                           
                         p(c_26) = [1]                                    
                         p(c_27) = [1] x1 + [1] x2 + [2]                  
                         p(c_28) = [0]                                    
                         p(c_29) = [4]                                    
                         p(c_30) = [1] x1 + [1]                           
                         p(c_31) = [0]                                    
                         p(c_32) = [2] x1 + [4] x2 + [2]                  
                         p(c_33) = [0]                                    
                         p(c_34) = [1] x1 + [0]                           
                         p(c_35) = [1]                                    
                         p(c_36) = [0]                                    
          
          Following rules are strictly oriented:
          #compare#(#pos(x),#pos(y)) = [1] x + [1] y + [2] 
                                     > [1] x + [1] y + [0] 
                                     = c_17(#compare#(x,y))
          
          
          Following rules are (at-least) weakly oriented:
           #compare#(#neg(x),#neg(y)) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_13(#compare#(y,x))          
          
               #compare#(#s(x),#s(y)) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_19(#compare#(x,y))          
          
                          #less#(x,y) =  [1] x + [1] y + [0]           
                                      >= [1] x + [1] y + [0]           
                                      =  c_20(#compare#(x,y))          
          
                         insert#(x,l) =  [1] l + [1] x + [2]           
                                      >= [1] l + [1] x + [2]           
                                      =  insert#1#(l,x)                
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [2]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
                insert#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [2]  
                                      >= [1] x + [1] ys + [2]          
                                      =  insert#2#(#less(y,x),x,y,ys)  
          
            insert#2#(#true(),x,y,ys) =  [1] x + [1] ys + [2]          
                                      >= [1] x + [1] ys + [2]          
                                      =  insert#(x,ys)                 
          
                        insertD#(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insertD#1#(l,x)               
          
               insertD#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [0]           
                                      =  #less#(y,x)                   
          
               insertD#1#(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] ys + [0]          
                                      =  insertD#2#(#less(y,x),x,y,ys) 
          
           insertD#2#(#true(),x,y,ys) =  [1] x + [1] ys + [0]          
                                      >= [1] x + [1] ys + [0]          
                                      =  insertD#(x,ys)                
          
                    insertionsort#(l) =  [2] l + [2]                   
                                      >= [2] l + [2]                   
                                      =  insertionsort#1#(l)           
          
           insertionsort#1#(dd(x,xs)) =  [2] x + [2] xs + [2]          
                                      >= [1] x + [1] xs + [2]          
                                      =  insert#(x,insertionsort(xs))  
          
           insertionsort#1#(dd(x,xs)) =  [2] x + [2] xs + [2]          
                                      >= [2] xs + [2]                  
                                      =  insertionsort#(xs)            
          
                   insertionsortD#(l) =  [6] l + [0]                   
                                      >= [6] l + [0]                   
                                      =  insertionsortD#1#(l)          
          
          insertionsortD#1#(dd(x,xs)) =  [6] x + [6] xs + [0]          
                                      >= [1] x + [6] xs + [0]          
                                      =  insertD#(x,insertionsortD(xs))
          
          insertionsortD#1#(dd(x,xs)) =  [6] x + [6] xs + [0]          
                                      >= [6] xs + [0]                  
                                      =  insertionsortD#(xs)           
          
                         #cklt(#EQ()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#GT()) =  [0]                           
                                      >= [0]                           
                                      =  #false()                      
          
                         #cklt(#LT()) =  [0]                           
                                      >= [0]                           
                                      =  #true()                       
          
                  #compare(#0(),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #EQ()                         
          
               #compare(#0(),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
               #compare(#0(),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
                 #compare(#0(),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#neg(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
            #compare(#neg(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(y,x)                 
          
            #compare(#neg(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #LT()                         
          
               #compare(#pos(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#neg(y)) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
            #compare(#pos(x),#pos(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                 #compare(#s(x),#0()) =  [0]                           
                                      >= [0]                           
                                      =  #GT()                         
          
                #compare(#s(x),#s(y)) =  [0]                           
                                      >= [0]                           
                                      =  #compare(x,y)                 
          
                           #less(x,y) =  [0]                           
                                      >= [0]                           
                                      =  #cklt(#compare(x,y))          
          
                          insert(x,l) =  [1] l + [1] x + [0]           
                                      >= [1] l + [1] x + [0]           
                                      =  insert#1(l,x)                 
          
                 insert#1(dd(y,ys),x) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  insert#2(#less(y,x),x,y,ys)   
          
                    insert#1(nil(),x) =  [1] x + [0]                   
                                      >= [1] x + [0]                   
                                      =  dd(x,nil())                   
          
            insert#2(#false(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
             insert#2(#true(),x,y,ys) =  [1] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insert(x,ys))            
          
                         insertD(x,l) =  [1] l + [4] x + [0]           
                                      >= [1] l + [4] x + [0]           
                                      =  insertD#1(l,x)                
          
                insertD#1(dd(y,ys),x) =  [4] x + [1] y + [1] ys + [0]  
                                      >= [4] x + [1] y + [1] ys + [0]  
                                      =  insertD#2(#less(y,x),x,y,ys)  
          
                   insertD#1(nil(),x) =  [4] x + [0]                   
                                      >= [1] x + [0]                   
                                      =  dd(x,nil())                   
          
           insertD#2(#false(),x,y,ys) =  [4] x + [1] y + [1] ys + [0]  
                                      >= [1] x + [1] y + [1] ys + [0]  
                                      =  dd(x,dd(y,ys))                
          
            insertD#2(#true(),x,y,ys) =  [4] x + [1] y + [1] ys + [0]  
                                      >= [4] x + [1] y + [1] ys + [0]  
                                      =  dd(y,insertD(x,ys))           
          
                     insertionsort(l) =  [1] l + [0]                   
                                      >= [1] l + [0]                   
                                      =  insertionsort#1(l)            
          
            insertionsort#1(dd(x,xs)) =  [1] x + [1] xs + [0]          
                                      >= [1] x + [1] xs + [0]          
                                      =  insert(x,insertionsort(xs))   
          
               insertionsort#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
                    insertionsortD(l) =  [6] l + [0]                   
                                      >= [6] l + [0]                   
                                      =  insertionsortD#1(l)           
          
           insertionsortD#1(dd(x,xs)) =  [6] x + [6] xs + [0]          
                                      >= [4] x + [6] xs + [0]          
                                      =  insertD(x,insertionsortD(xs)) 
          
              insertionsortD#1(nil()) =  [0]                           
                                      >= [0]                           
                                      =  nil()                         
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 6.b:1.b:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            #compare#(#neg(x),#neg(y)) -> c_13(#compare#(y,x))
            #compare#(#pos(x),#pos(y)) -> c_17(#compare#(x,y))
            #compare#(#s(x),#s(y)) -> c_19(#compare#(x,y))
            #less#(x,y) -> c_20(#compare#(x,y))
            insert#(x,l) -> insert#1#(l,x)
            insert#1#(dd(y,ys),x) -> #less#(y,x)
            insert#1#(dd(y,ys),x) -> insert#2#(#less(y,x),x,y,ys)
            insert#2#(#true(),x,y,ys) -> insert#(x,ys)
            insertD#(x,l) -> insertD#1#(l,x)
            insertD#1#(dd(y,ys),x) -> #less#(y,x)
            insertD#1#(dd(y,ys),x) -> insertD#2#(#less(y,x),x,y,ys)
            insertD#2#(#true(),x,y,ys) -> insertD#(x,ys)
            insertionsort#(l) -> insertionsort#1#(l)
            insertionsort#1#(dd(x,xs)) -> insert#(x,insertionsort(xs))
            insertionsort#1#(dd(x,xs)) -> insertionsort#(xs)
            insertionsortD#(l) -> insertionsortD#1#(l)
            insertionsortD#1#(dd(x,xs)) -> insertD#(x,insertionsortD(xs))
            insertionsortD#1#(dd(x,xs)) -> insertionsortD#(xs)
        - Weak TRS:
            #cklt(#EQ()) -> #false()
            #cklt(#GT()) -> #false()
            #cklt(#LT()) -> #true()
            #compare(#0(),#0()) -> #EQ()
            #compare(#0(),#neg(y)) -> #GT()
            #compare(#0(),#pos(y)) -> #LT()
            #compare(#0(),#s(y)) -> #LT()
            #compare(#neg(x),#0()) -> #LT()
            #compare(#neg(x),#neg(y)) -> #compare(y,x)
            #compare(#neg(x),#pos(y)) -> #LT()
            #compare(#pos(x),#0()) -> #GT()
            #compare(#pos(x),#neg(y)) -> #GT()
            #compare(#pos(x),#pos(y)) -> #compare(x,y)
            #compare(#s(x),#0()) -> #GT()
            #compare(#s(x),#s(y)) -> #compare(x,y)
            #less(x,y) -> #cklt(#compare(x,y))
            insert(x,l) -> insert#1(l,x)
            insert#1(dd(y,ys),x) -> insert#2(#less(y,x),x,y,ys)
            insert#1(nil(),x) -> dd(x,nil())
            insert#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insert#2(#true(),x,y,ys) -> dd(y,insert(x,ys))
            insertD(x,l) -> insertD#1(l,x)
            insertD#1(dd(y,ys),x) -> insertD#2(#less(y,x),x,y,ys)
            insertD#1(nil(),x) -> dd(x,nil())
            insertD#2(#false(),x,y,ys) -> dd(x,dd(y,ys))
            insertD#2(#true(),x,y,ys) -> dd(y,insertD(x,ys))
            insertionsort(l) -> insertionsort#1(l)
            insertionsort#1(dd(x,xs)) -> insert(x,insertionsort(xs))
            insertionsort#1(nil()) -> nil()
            insertionsortD(l) -> insertionsortD#1(l)
            insertionsortD#1(dd(x,xs)) -> insertD(x,insertionsortD(xs))
            insertionsortD#1(nil()) -> nil()
        - Signature:
            {#abs/1,#cklt/1,#compare/2,#less/2,insert/2,insert#1/2,insert#2/4,insertD/2,insertD#1/2,insertD#2/4
            ,insertionsort/1,insertionsort#1/1,insertionsortD/1,insertionsortD#1/1,#abs#/1,#cklt#/1,#compare#/2,#less#/2
            ,insert#/2,insert#1#/2,insert#2#/4,insertD#/2,insertD#1#/2,insertD#2#/4,insertionsort#/1,insertionsort#1#/1
            ,insertionsortD#/1,insertionsortD#1#/1} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2
            ,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0
            ,c_16/0,c_17/1,c_18/0,c_19/1,c_20/1,c_21/1,c_22/2,c_23/0,c_24/0,c_25/1,c_26/1,c_27/2,c_28/0,c_29/0,c_30/1
            ,c_31/1,c_32/2,c_33/0,c_34/1,c_35/2,c_36/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {#abs#,#cklt#,#compare#,#less#,insert#,insert#1#,insert#2#
            ,insertD#,insertD#1#,insertD#2#,insertionsort#,insertionsort#1#,insertionsortD#
            ,insertionsortD#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))