*** 1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
        D(+(x,y)) -> +(D(x),D(y))
        D(-(x,y)) -> -(D(x),D(y))
        D(constant()) -> 0()
        D(t()) -> 1()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0}
      Obligation:
        Innermost
        basic terms: {D}/{*,+,-,0,1,constant,t}
    Applied Processor:
      DependencyPairs {dpKind_ = WIDP}
    Proof:
      We add the following weak innermost dependency pairs:
      
      Strict DPs
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
      Strict TRS Rules:
        D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
        D(+(x,y)) -> +(D(x),D(y))
        D(-(x,y)) -> -(D(x),D(y))
        D(constant()) -> 0()
        D(t()) -> 1()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
      Obligation:
        Innermost
        basic terms: {D#}/{*,+,-,0,1,constant,t}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
*** 1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
      Obligation:
        Innermost
        basic terms: {D#}/{*,+,-,0,1,constant,t}
    Applied Processor:
      Succeeding
    Proof:
      ()
*** 1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
      Obligation:
        Innermost
        basic terms: {D#}/{*,+,-,0,1,constant,t}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {4,5}
      by application of
        Pre({4,5}) = {1,2,3}.
      Here rules are labelled as follows:
        1: D#(*(x,y)) -> c_1(D#(x),D#(y))
        2: D#(+(x,y)) -> c_2(D#(x),D#(y))
        3: D#(-(x,y)) -> c_3(D#(x),D#(y))
        4: D#(constant()) -> c_4()       
        5: D#(t()) -> c_5()              
*** 1.1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        D#(constant()) -> c_4()
        D#(t()) -> c_5()
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
      Obligation:
        Innermost
        basic terms: {D#}/{*,+,-,0,1,constant,t}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:D#(*(x,y)) -> c_1(D#(x),D#(y))
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(t()) -> c_5():5
           -->_1 D#(t()) -> c_5():5
           -->_2 D#(constant()) -> c_4():4
           -->_1 D#(constant()) -> c_4():4
           -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
        
        2:S:D#(+(x,y)) -> c_2(D#(x),D#(y))
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(t()) -> c_5():5
           -->_1 D#(t()) -> c_5():5
           -->_2 D#(constant()) -> c_4():4
           -->_1 D#(constant()) -> c_4():4
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
        
        3:S:D#(-(x,y)) -> c_3(D#(x),D#(y))
           -->_2 D#(t()) -> c_5():5
           -->_1 D#(t()) -> c_5():5
           -->_2 D#(constant()) -> c_4():4
           -->_1 D#(constant()) -> c_4():4
           -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
           -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
           -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
           -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
        
        4:W:D#(constant()) -> c_4()
           
        
        5:W:D#(t()) -> c_5()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        4: D#(constant()) -> c_4()
        5: D#(t()) -> c_5()       
*** 1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        D#(*(x,y)) -> c_1(D#(x),D#(y))
        D#(+(x,y)) -> c_2(D#(x),D#(y))
        D#(-(x,y)) -> c_3(D#(x),D#(y))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
      Obligation:
        Innermost
        basic terms: {D#}/{*,+,-,0,1,constant,t}
    Applied Processor:
      PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
    Proof:
      We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
        2: D#(+(x,y)) -> c_2(D#(x),D#(y))
        
      The strictly oriented rules are moved into the weak component.
  *** 1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(D#(x),D#(y))
          D#(+(x,y)) -> c_2(D#(x),D#(y))
          D#(-(x,y)) -> c_3(D#(x),D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
        Obligation:
          Innermost
          basic terms: {D#}/{*,+,-,0,1,constant,t}
      Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
      Proof:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1,2},
          uargs(c_2) = {1,2},
          uargs(c_3) = {1,2}
        
        Following symbols are considered usable:
          {D#}
        TcT has computed the following interpretation:
                 p(*) = [1] x1 + [1] x2 + [0]
                 p(+) = [1] x1 + [1] x2 + [2]
                 p(-) = [1] x1 + [1] x2 + [0]
                 p(0) = [2]                  
                 p(1) = [1]                  
                 p(D) = [0]                  
          p(constant) = [1]                  
                 p(t) = [1]                  
                p(D#) = [8] x1 + [0]         
               p(c_1) = [1] x1 + [1] x2 + [0]
               p(c_2) = [1] x1 + [1] x2 + [6]
               p(c_3) = [1] x1 + [1] x2 + [0]
               p(c_4) = [2]                  
               p(c_5) = [0]                  
        
        Following rules are strictly oriented:
        D#(+(x,y)) = [8] x + [8] y + [16]
                   > [8] x + [8] y + [6] 
                   = c_2(D#(x),D#(y))    
        
        
        Following rules are (at-least) weakly oriented:
        D#(*(x,y)) =  [8] x + [8] y + [0]
                   >= [8] x + [8] y + [0]
                   =  c_1(D#(x),D#(y))   
        
        D#(-(x,y)) =  [8] x + [8] y + [0]
                   >= [8] x + [8] y + [0]
                   =  c_3(D#(x),D#(y))   
        
  *** 1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(D#(x),D#(y))
          D#(-(x,y)) -> c_3(D#(x),D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          D#(+(x,y)) -> c_2(D#(x),D#(y))
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
        Obligation:
          Innermost
          basic terms: {D#}/{*,+,-,0,1,constant,t}
      Applied Processor:
        Assumption
      Proof:
        ()
  
  *** 1.1.1.1.1.1.2 Progress [(?,O(n^1))]  ***
      Considered Problem:
        Strict DP Rules:
          D#(*(x,y)) -> c_1(D#(x),D#(y))
          D#(-(x,y)) -> c_3(D#(x),D#(y))
        Strict TRS Rules:
          
        Weak DP Rules:
          D#(+(x,y)) -> c_2(D#(x),D#(y))
        Weak TRS Rules:
          
        Signature:
          {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
        Obligation:
          Innermost
          basic terms: {D#}/{*,+,-,0,1,constant,t}
      Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
      Proof:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
          2: D#(-(x,y)) -> c_3(D#(x),D#(y))
          
        The strictly oriented rules are moved into the weak component.
    *** 1.1.1.1.1.1.2.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(*(x,y)) -> c_1(D#(x),D#(y))
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(+(x,y)) -> c_2(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
          Obligation:
            Innermost
            basic terms: {D#}/{*,+,-,0,1,constant,t}
        Applied Processor:
          NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
        Proof:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_1) = {1,2},
            uargs(c_2) = {1,2},
            uargs(c_3) = {1,2}
          
          Following symbols are considered usable:
            {D#}
          TcT has computed the following interpretation:
                   p(*) = [1] x1 + [1] x2 + [0]
                   p(+) = [1] x1 + [1] x2 + [4]
                   p(-) = [1] x1 + [1] x2 + [4]
                   p(0) = [2]                  
                   p(1) = [2]                  
                   p(D) = [1]                  
            p(constant) = [1]                  
                   p(t) = [1]                  
                  p(D#) = [1] x1 + [0]         
                 p(c_1) = [1] x1 + [1] x2 + [0]
                 p(c_2) = [1] x1 + [1] x2 + [1]
                 p(c_3) = [1] x1 + [1] x2 + [0]
                 p(c_4) = [1]                  
                 p(c_5) = [0]                  
          
          Following rules are strictly oriented:
          D#(-(x,y)) = [1] x + [1] y + [4]
                     > [1] x + [1] y + [0]
                     = c_3(D#(x),D#(y))   
          
          
          Following rules are (at-least) weakly oriented:
          D#(*(x,y)) =  [1] x + [1] y + [0]
                     >= [1] x + [1] y + [0]
                     =  c_1(D#(x),D#(y))   
          
          D#(+(x,y)) =  [1] x + [1] y + [4]
                     >= [1] x + [1] y + [1]
                     =  c_2(D#(x),D#(y))   
          
    *** 1.1.1.1.1.1.2.1.1 Progress [(?,O(1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(*(x,y)) -> c_1(D#(x),D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(+(x,y)) -> c_2(D#(x),D#(y))
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
          Obligation:
            Innermost
            basic terms: {D#}/{*,+,-,0,1,constant,t}
        Applied Processor:
          Assumption
        Proof:
          ()
    
    *** 1.1.1.1.1.1.2.2 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            D#(*(x,y)) -> c_1(D#(x),D#(y))
          Strict TRS Rules:
            
          Weak DP Rules:
            D#(+(x,y)) -> c_2(D#(x),D#(y))
            D#(-(x,y)) -> c_3(D#(x),D#(y))
          Weak TRS Rules:
            
          Signature:
            {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
          Obligation:
            Innermost
            basic terms: {D#}/{*,+,-,0,1,constant,t}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: D#(*(x,y)) -> c_1(D#(x),D#(y))
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.2.2.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              D#(*(x,y)) -> c_1(D#(x),D#(y))
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
            Obligation:
              Innermost
              basic terms: {D#}/{*,+,-,0,1,constant,t}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_1) = {1,2},
              uargs(c_2) = {1,2},
              uargs(c_3) = {1,2}
            
            Following symbols are considered usable:
              {D#}
            TcT has computed the following interpretation:
                     p(*) = [1] x1 + [1] x2 + [2] 
                     p(+) = [1] x1 + [1] x2 + [0] 
                     p(-) = [1] x1 + [1] x2 + [0] 
                     p(0) = [4]                   
                     p(1) = [0]                   
                     p(D) = [2] x1 + [0]          
              p(constant) = [8]                   
                     p(t) = [1]                   
                    p(D#) = [8] x1 + [0]          
                   p(c_1) = [1] x1 + [1] x2 + [13]
                   p(c_2) = [1] x1 + [1] x2 + [0] 
                   p(c_3) = [1] x1 + [1] x2 + [0] 
                   p(c_4) = [0]                   
                   p(c_5) = [0]                   
            
            Following rules are strictly oriented:
            D#(*(x,y)) = [8] x + [8] y + [16]
                       > [8] x + [8] y + [13]
                       = c_1(D#(x),D#(y))    
            
            
            Following rules are (at-least) weakly oriented:
            D#(+(x,y)) =  [8] x + [8] y + [0]
                       >= [8] x + [8] y + [0]
                       =  c_2(D#(x),D#(y))   
            
            D#(-(x,y)) =  [8] x + [8] y + [0]
                       >= [8] x + [8] y + [0]
                       =  c_3(D#(x),D#(y))   
            
      *** 1.1.1.1.1.1.2.2.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(*(x,y)) -> c_1(D#(x),D#(y))
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
            Obligation:
              Innermost
              basic terms: {D#}/{*,+,-,0,1,constant,t}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.2.2.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              D#(*(x,y)) -> c_1(D#(x),D#(y))
              D#(+(x,y)) -> c_2(D#(x),D#(y))
              D#(-(x,y)) -> c_3(D#(x),D#(y))
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
            Obligation:
              Innermost
              basic terms: {D#}/{*,+,-,0,1,constant,t}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:D#(*(x,y)) -> c_1(D#(x),D#(y))
                 -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
                 -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
              
              2:W:D#(+(x,y)) -> c_2(D#(x),D#(y))
                 -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
                 -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
              
              3:W:D#(-(x,y)) -> c_3(D#(x),D#(y))
                 -->_2 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_1 D#(-(x,y)) -> c_3(D#(x),D#(y)):3
                 -->_2 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_1 D#(+(x,y)) -> c_2(D#(x),D#(y)):2
                 -->_2 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
                 -->_1 D#(*(x,y)) -> c_1(D#(x),D#(y)):1
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              1: D#(*(x,y)) -> c_1(D#(x),D#(y))
              3: D#(-(x,y)) -> c_3(D#(x),D#(y))
              2: D#(+(x,y)) -> c_2(D#(x),D#(y))
      *** 1.1.1.1.1.1.2.2.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              
            Signature:
              {D/1,D#/1} / {*/2,+/2,-/2,0/0,1/0,constant/0,t/0,c_1/2,c_2/2,c_3/2,c_4/0,c_5/0}
            Obligation:
              Innermost
              basic terms: {D#}/{*,+,-,0,1,constant,t}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).