*** 1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w)))
        h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w))))))
        h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x)))))
        t(x) -> x
        t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x)))))
        t(t(x)) -> t(c(t(x),x))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {h/3,t/1} / {0/0,c/2,s/1}
      Obligation:
        Innermost
        basic terms: {h,t}/{0,c,s}
    Applied Processor:
      InnermostRuleRemoval
    Proof:
      Arguments of following rules are not normal-forms.
        h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w)))
        h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w))))))
        h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x)))))
        t(t(x)) -> t(c(t(x),x))
      All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        t(x) -> x
        t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x)))))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {h/3,t/1} / {0/0,c/2,s/1}
      Obligation:
        Innermost
        basic terms: {h,t}/{0,c,s}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        t#(x) -> c_1()
        t#(x) -> c_2()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        t#(x) -> c_1()
        t#(x) -> c_2()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        t(x) -> x
        t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x)))))
      Signature:
        {h/3,t/1,h#/3,t#/1} / {0/0,c/2,s/1,c_1/0,c_2/0}
      Obligation:
        Innermost
        basic terms: {h#,t#}/{0,c,s}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        t#(x) -> c_1()
        t#(x) -> c_2()
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        t#(x) -> c_1()
        t#(x) -> c_2()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {h/3,t/1,h#/3,t#/1} / {0/0,c/2,s/1,c_1/0,c_2/0}
      Obligation:
        Innermost
        basic terms: {h#,t#}/{0,c,s}
    Applied Processor:
      Trivial
    Proof:
      Consider the dependency graph
        1:S:t#(x) -> c_1()
           
        
        2:S:t#(x) -> c_2()
           
        
      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:
        {h/3,t/1,h#/3,t#/1} / {0/0,c/2,s/1,c_1/0,c_2/0}
      Obligation:
        Innermost
        basic terms: {h#,t#}/{0,c,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).