*** 1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))
        f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3}
      Obligation:
        Full
        basic terms: {f}/{.,a,b,b',c,d,d',e,g,h,i,if}
    Applied Processor:
      ToInnermost
    Proof:
      switch to innermost, as the system is overlay and right linear and does not contain weak rules
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))
        f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3}
      Obligation:
        Innermost
        basic terms: {f}/{.,a,b,b',c,d,d',e,g,h,i,if}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'()))
        f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'()))
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'()))
        f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'()))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))
        f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
      Signature:
        {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2}
      Obligation:
        Innermost
        basic terms: {f#}/{.,a,b,b',c,d,d',e,g,h,i,if}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'()))
        f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'()))
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'()))
        f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'()))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2}
      Obligation:
        Innermost
        basic terms: {f#}/{.,a,b,b',c,d,d',e,g,h,i,if}
    Applied Processor:
      Trivial
    Proof:
      Consider the dependency graph
        1:S:f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'()))
           
        
        2:S:f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'()))
           
        
      The dependency graph contains no loops, we remove all dependency pairs.
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2}
      Obligation:
        Innermost
        basic terms: {f#}/{.,a,b,b',c,d,d',e,g,h,i,if}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).