*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        active(f(x)) -> f(active(x))
        active(f(x)) -> mark(x)
        check(x) -> start(match(f(X()),x))
        check(f(x)) -> f(check(x))
        f(found(x)) -> found(f(x))
        f(mark(x)) -> mark(f(x))
        f(ok(x)) -> ok(f(x))
        match(X(),x) -> proper(x)
        match(f(x),f(y)) -> f(match(x,y))
        proper(c()) -> ok(c())
        proper(f(x)) -> f(proper(x))
        start(ok(x)) -> found(x)
        top(active(c())) -> top(mark(c()))
        top(found(x)) -> top(active(x))
        top(mark(x)) -> top(check(x))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
      Obligation:
        Full
        basic terms: {active,check,f,match,proper,start,top}/{X,c,found,mark,ok}
    Applied Processor:
      Bounds {initialAutomaton = perSymbol, enrichment = match}
    Proof:
      The problem is match-bounded by 3.
      The enriched problem is compatible with follwoing automaton.
        X_0() -> 1
        X_1() -> 15
        X_2() -> 21
        X_3() -> 25
        active_0(1) -> 2
        active_0(3) -> 2
        active_0(6) -> 2
        active_0(7) -> 2
        active_0(9) -> 2
        active_1(1) -> 18
        active_1(3) -> 18
        active_1(6) -> 18
        active_1(7) -> 18
        active_1(9) -> 18
        c_0() -> 3
        c_1() -> 17
        check_0(1) -> 4
        check_0(3) -> 4
        check_0(6) -> 4
        check_0(7) -> 4
        check_0(9) -> 4
        check_1(1) -> 18
        check_1(3) -> 18
        check_1(6) -> 18
        check_1(7) -> 18
        check_1(9) -> 18
        check_2(17) -> 22
        f_0(1) -> 5
        f_0(3) -> 5
        f_0(6) -> 5
        f_0(7) -> 5
        f_0(9) -> 5
        f_1(1) -> 16
        f_1(3) -> 16
        f_1(6) -> 16
        f_1(7) -> 16
        f_1(9) -> 16
        f_1(15) -> 14
        f_2(21) -> 20
        f_3(25) -> 24
        found_0(1) -> 6
        found_0(3) -> 6
        found_0(6) -> 6
        found_0(7) -> 6
        found_0(9) -> 6
        found_1(1) -> 11
        found_1(3) -> 11
        found_1(6) -> 11
        found_1(7) -> 11
        found_1(9) -> 11
        found_1(16) -> 5
        found_1(16) -> 16
        mark_0(1) -> 7
        mark_0(3) -> 7
        mark_0(6) -> 7
        mark_0(7) -> 7
        mark_0(9) -> 7
        mark_1(16) -> 5
        mark_1(16) -> 16
        mark_1(17) -> 18
        match_0(1,1) -> 8
        match_0(1,3) -> 8
        match_0(1,6) -> 8
        match_0(1,7) -> 8
        match_0(1,9) -> 8
        match_0(3,1) -> 8
        match_0(3,3) -> 8
        match_0(3,6) -> 8
        match_0(3,7) -> 8
        match_0(3,9) -> 8
        match_0(6,1) -> 8
        match_0(6,3) -> 8
        match_0(6,6) -> 8
        match_0(6,7) -> 8
        match_0(6,9) -> 8
        match_0(7,1) -> 8
        match_0(7,3) -> 8
        match_0(7,6) -> 8
        match_0(7,7) -> 8
        match_0(7,9) -> 8
        match_0(9,1) -> 8
        match_0(9,3) -> 8
        match_0(9,6) -> 8
        match_0(9,7) -> 8
        match_0(9,9) -> 8
        match_1(14,1) -> 13
        match_1(14,3) -> 13
        match_1(14,6) -> 13
        match_1(14,7) -> 13
        match_1(14,9) -> 13
        match_2(20,1) -> 19
        match_2(20,3) -> 19
        match_2(20,6) -> 19
        match_2(20,7) -> 19
        match_2(20,9) -> 19
        match_3(24,17) -> 23
        ok_0(1) -> 9
        ok_0(3) -> 9
        ok_0(6) -> 9
        ok_0(7) -> 9
        ok_0(9) -> 9
        ok_1(16) -> 5
        ok_1(16) -> 16
        ok_1(17) -> 8
        ok_1(17) -> 10
        proper_0(1) -> 10
        proper_0(3) -> 10
        proper_0(6) -> 10
        proper_0(7) -> 10
        proper_0(9) -> 10
        proper_1(1) -> 8
        proper_1(3) -> 8
        proper_1(6) -> 8
        proper_1(7) -> 8
        proper_1(9) -> 8
        start_0(1) -> 11
        start_0(3) -> 11
        start_0(6) -> 11
        start_0(7) -> 11
        start_0(9) -> 11
        start_1(13) -> 4
        start_2(19) -> 18
        start_3(23) -> 22
        top_0(1) -> 12
        top_0(3) -> 12
        top_0(6) -> 12
        top_0(7) -> 12
        top_0(9) -> 12
        top_1(18) -> 12
        top_2(22) -> 12
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        active(f(x)) -> f(active(x))
        active(f(x)) -> mark(x)
        check(x) -> start(match(f(X()),x))
        check(f(x)) -> f(check(x))
        f(found(x)) -> found(f(x))
        f(mark(x)) -> mark(f(x))
        f(ok(x)) -> ok(f(x))
        match(X(),x) -> proper(x)
        match(f(x),f(y)) -> f(match(x,y))
        proper(c()) -> ok(c())
        proper(f(x)) -> f(proper(x))
        start(ok(x)) -> found(x)
        top(active(c())) -> top(mark(c()))
        top(found(x)) -> top(active(x))
        top(mark(x)) -> top(check(x))
      Signature:
        {active/1,check/1,f/1,match/2,proper/1,start/1,top/1} / {X/0,c/0,found/1,mark/1,ok/1}
      Obligation:
        Full
        basic terms: {active,check,f,match,proper,start,top}/{X,c,found,mark,ok}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).