*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
        comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
        foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
        foldr#3(Nil()) -> id()
        foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
        foldr_f#3(Nil(),0()) -> 0()
        main(x3) -> foldr_f#3(map#2(x3),0())
        map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
        map#2(Nil()) -> Nil()
        plus_x#1(0(),x6) -> x6
        plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0,plus_x/1}
      Obligation:
        Innermost
        basic terms: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1}/{0,Cons,Nil,S,comp_f_g,id,plus_x}
    Applied Processor:
      Bounds {initialAutomaton = minimal, enrichment = match}
    Proof:
      The problem is match-bounded by 2.
      The enriched problem is compatible with follwoing automaton.
        0_0() -> 1
        0_0() -> 2
        0_0() -> 8
        0_0() -> 10
        0_1() -> 1
        0_1() -> 3
        0_1() -> 4
        0_1() -> 10
        0_2() -> 1
        0_2() -> 10
        Cons_0(2,2) -> 1
        Cons_0(2,2) -> 2
        Cons_0(2,2) -> 8
        Cons_0(2,2) -> 10
        Cons_1(7,6) -> 1
        Cons_1(7,6) -> 6
        Cons_1(7,6) -> 10
        Nil_0() -> 1
        Nil_0() -> 2
        Nil_0() -> 8
        Nil_0() -> 10
        Nil_1() -> 1
        Nil_1() -> 6
        Nil_1() -> 10
        S_0(2) -> 1
        S_0(2) -> 2
        S_0(2) -> 8
        S_0(2) -> 10
        S_1(1) -> 1
        S_1(1) -> 10
        S_1(3) -> 1
        S_1(3) -> 3
        S_1(3) -> 10
        S_1(8) -> 1
        S_1(8) -> 8
        S_1(8) -> 10
        comp_f_g_0(2,2) -> 1
        comp_f_g_0(2,2) -> 2
        comp_f_g_0(2,2) -> 8
        comp_f_g_0(2,2) -> 10
        comp_f_g_1(2,5) -> 1
        comp_f_g_1(2,5) -> 5
        comp_f_g_1(2,5) -> 10
        comp_f_g_2(7,9) -> 9
        comp_f_g#1_0(2,2,2) -> 1
        comp_f_g#1_0(2,2,2) -> 10
        comp_f_g#1_1(2,2,4) -> 1
        comp_f_g#1_1(2,2,4) -> 3
        comp_f_g#1_1(2,2,4) -> 10
        comp_f_g#1_1(2,5,2) -> 1
        comp_f_g#1_1(2,5,2) -> 10
        comp_f_g#1_1(2,5,4) -> 1
        comp_f_g#1_1(2,5,4) -> 3
        comp_f_g#1_1(2,5,4) -> 10
        comp_f_g#1_1(7,9,10) -> 1
        comp_f_g#1_1(7,9,10) -> 10
        comp_f_g#1_2(7,9,1) -> 1
        comp_f_g#1_2(7,9,1) -> 10
        comp_f_g#1_2(7,9,4) -> 1
        comp_f_g#1_2(7,9,4) -> 10
        foldr#3_0(2) -> 1
        foldr#3_0(2) -> 10
        foldr#3_1(2) -> 5
        foldr#3_2(6) -> 9
        foldr_f#3_0(2,2) -> 1
        foldr_f#3_0(2,2) -> 10
        foldr_f#3_1(6,4) -> 1
        foldr_f#3_1(6,4) -> 10
        id_0() -> 1
        id_0() -> 2
        id_0() -> 8
        id_0() -> 10
        id_1() -> 1
        id_1() -> 5
        id_1() -> 10
        id_2() -> 9
        main_0(2) -> 1
        main_0(2) -> 10
        map#2_0(2) -> 1
        map#2_0(2) -> 10
        map#2_1(2) -> 6
        plus_x_0(2) -> 1
        plus_x_0(2) -> 2
        plus_x_0(2) -> 8
        plus_x_0(2) -> 10
        plus_x_1(2) -> 7
        plus_x#1_0(2,2) -> 1
        plus_x#1_0(2,2) -> 10
        plus_x#1_1(2,1) -> 1
        plus_x#1_1(2,1) -> 10
        plus_x#1_1(2,2) -> 8
        plus_x#1_1(2,3) -> 1
        plus_x#1_1(2,3) -> 3
        plus_x#1_1(2,3) -> 10
        plus_x#1_1(2,4) -> 1
        plus_x#1_1(2,4) -> 3
        plus_x#1_1(2,4) -> 10
        plus_x#1_1(2,10) -> 1
        plus_x#1_1(2,10) -> 10
        plus_x#1_2(2,1) -> 1
        plus_x#1_2(2,1) -> 10
        plus_x#1_2(2,10) -> 1
        plus_x#1_2(2,10) -> 10
        1 -> 10
        2 -> 1
        2 -> 8
        2 -> 10
        3 -> 1
        3 -> 10
        4 -> 1
        4 -> 3
        4 -> 10
        10 -> 1
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
        comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
        foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
        foldr#3(Nil()) -> id()
        foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
        foldr_f#3(Nil(),0()) -> 0()
        main(x3) -> foldr_f#3(map#2(x3),0())
        map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
        map#2(Nil()) -> Nil()
        plus_x#1(0(),x6) -> x6
        plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
      Signature:
        {comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0,plus_x/1}
      Obligation:
        Innermost
        basic terms: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1}/{0,Cons,Nil,S,comp_f_g,id,plus_x}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).