YES(?,O(n^2))
14.00/7.52	YES(?,O(n^2))
14.00/7.52	
14.00/7.52	Problem:
14.00/7.52	 app(id(),x) -> x
14.00/7.52	 app(plus(),0()) -> id()
14.00/7.52	 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
14.00/7.52	
14.00/7.52	Proof:
14.00/7.52	 Uncurry Processor:
14.00/7.52	  id1(x) -> x
14.00/7.52	  plus2(0(),x4) -> id1(x4)
14.00/7.52	  plus1(0()) -> id()
14.00/7.52	  plus2(s1(x),y) -> s1(plus2(x,y))
14.00/7.52	  app(id(),x3) -> id1(x3)
14.00/7.52	  app(plus1(x2),x3) -> plus2(x2,x3)
14.00/7.52	  app(plus(),x3) -> plus1(x3)
14.00/7.52	  app(s(),x3) -> s1(x3)
14.00/7.52	  Complexity Transformation Processor:
14.00/7.52	   strict:
14.00/7.52	    id1(x) -> x
14.00/7.52	    plus2(0(),x4) -> id1(x4)
14.00/7.52	    plus1(0()) -> id()
14.00/7.52	    plus2(s1(x),y) -> s1(plus2(x,y))
14.00/7.52	    app(id(),x3) -> id1(x3)
14.00/7.52	    app(plus1(x2),x3) -> plus2(x2,x3)
14.00/7.52	    app(plus(),x3) -> plus1(x3)
14.00/7.52	    app(s(),x3) -> s1(x3)
14.00/7.52	   weak:
14.00/7.52	    
14.00/7.52	   Matrix Interpretation Processor: dim=1
14.00/7.52	    
14.00/7.52	    max_matrix:
14.00/7.52	     1
14.00/7.52	    interpretation:
14.00/7.52	     [s1](x0) = x0 + 32,
14.00/7.52	     
14.00/7.52	     [plus2](x0, x1) = x0 + x1 + 238,
14.00/7.52	     
14.00/7.52	     [plus1](x0) = x0,
14.00/7.52	     
14.00/7.52	     [id1](x0) = x0,
14.00/7.52	     
14.00/7.52	     [s] = 2,
14.00/7.52	     
14.00/7.52	     [0] = 20,
14.00/7.52	     
14.00/7.52	     [plus] = 208,
14.00/7.52	     
14.00/7.52	     [app](x0, x1) = x0 + x1 + 97,
14.00/7.52	     
14.00/7.52	     [id] = 162
14.00/7.52	    orientation:
14.00/7.52	     id1(x) = x >= x = x
14.00/7.52	     
14.00/7.52	     plus2(0(),x4) = x4 + 258 >= x4 = id1(x4)
14.00/7.52	     
14.00/7.52	     plus1(0()) = 20 >= 162 = id()
14.00/7.52	     
14.00/7.52	     plus2(s1(x),y) = x + y + 270 >= x + y + 270 = s1(plus2(x,y))
14.00/7.52	     
14.00/7.52	     app(id(),x3) = x3 + 259 >= x3 = id1(x3)
14.00/7.52	     
14.00/7.52	     app(plus1(x2),x3) = x2 + x3 + 97 >= x2 + x3 + 238 = plus2(x2,x3)
14.00/7.52	     
14.00/7.52	     app(plus(),x3) = x3 + 305 >= x3 = plus1(x3)
14.00/7.52	     
14.00/7.52	     app(s(),x3) = x3 + 99 >= x3 + 32 = s1(x3)
14.00/7.52	    problem:
14.00/7.52	     strict:
14.00/7.52	      id1(x) -> x
14.00/7.52	      plus1(0()) -> id()
14.00/7.52	      plus2(s1(x),y) -> s1(plus2(x,y))
14.00/7.52	      app(plus1(x2),x3) -> plus2(x2,x3)
14.00/7.52	     weak:
14.00/7.52	      plus2(0(),x4) -> id1(x4)
14.00/7.52	      app(id(),x3) -> id1(x3)
14.00/7.52	      app(plus(),x3) -> plus1(x3)
14.00/7.52	      app(s(),x3) -> s1(x3)
14.00/7.52	    Matrix Interpretation Processor: dim=1
14.00/7.52	     
14.00/7.52	     max_matrix:
14.00/7.52	      1
14.00/7.52	     interpretation:
14.00/7.52	      [s1](x0) = x0 + 28,
14.00/7.52	      
14.00/7.52	      [plus2](x0, x1) = x0 + x1 + 16,
14.00/7.52	      
14.00/7.52	      [plus1](x0) = x0 + 157,
14.00/7.52	      
14.00/7.52	      [id1](x0) = x0 + 64,
14.00/7.52	      
14.00/7.52	      [s] = 0,
14.00/7.52	      
14.00/7.52	      [0] = 48,
14.00/7.52	      
14.00/7.52	      [plus] = 129,
14.00/7.52	      
14.00/7.52	      [app](x0, x1) = x0 + x1 + 28,
14.00/7.52	      
14.00/7.52	      [id] = 36
14.00/7.52	     orientation:
14.00/7.52	      id1(x) = x + 64 >= x = x
14.00/7.52	      
14.00/7.52	      plus1(0()) = 205 >= 36 = id()
14.00/7.52	      
14.00/7.52	      plus2(s1(x),y) = x + y + 44 >= x + y + 44 = s1(plus2(x,y))
14.00/7.52	      
14.00/7.52	      app(plus1(x2),x3) = x2 + x3 + 185 >= x2 + x3 + 16 = plus2(x2,x3)
14.00/7.52	      
14.00/7.52	      plus2(0(),x4) = x4 + 64 >= x4 + 64 = id1(x4)
14.00/7.52	      
14.00/7.52	      app(id(),x3) = x3 + 64 >= x3 + 64 = id1(x3)
14.00/7.52	      
14.00/7.52	      app(plus(),x3) = x3 + 157 >= x3 + 157 = plus1(x3)
14.00/7.52	      
14.00/7.52	      app(s(),x3) = x3 + 28 >= x3 + 28 = s1(x3)
14.00/7.52	     problem:
14.00/7.52	      strict:
14.00/7.52	       plus2(s1(x),y) -> s1(plus2(x,y))
14.00/7.52	      weak:
14.00/7.52	       id1(x) -> x
14.00/7.52	       plus1(0()) -> id()
14.00/7.52	       app(plus1(x2),x3) -> plus2(x2,x3)
14.00/7.52	       plus2(0(),x4) -> id1(x4)
14.00/7.52	       app(id(),x3) -> id1(x3)
14.00/7.52	       app(plus(),x3) -> plus1(x3)
14.00/7.52	       app(s(),x3) -> s1(x3)
14.00/7.52	     Matrix Interpretation Processor: dim=2
14.00/7.52	      
14.00/7.52	      max_matrix:
14.00/7.52	       [1 2]
14.00/7.52	       [0 1]
14.00/7.52	      interpretation:
14.00/7.52	                       [1]
14.00/7.52	       [s1](x0) = x0 + [1],
14.00/7.52	       
14.00/7.52	                         [1 2]     [1 2]     [2]
14.00/7.52	       [plus2](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
14.00/7.52	       
14.00/7.52	                     [1 1]     [0]
14.00/7.52	       [plus1](x0) = [0 1]x0 + [2],
14.00/7.52	       
14.00/7.52	                   [1 2]  
14.00/7.52	       [id1](x0) = [0 1]x0,
14.00/7.52	       
14.00/7.52	             [1]
14.00/7.52	       [s] = [0],
14.00/7.52	       
14.00/7.52	             [2]
14.00/7.52	       [0] = [2],
14.00/7.52	       
14.00/7.52	                [0]
14.00/7.52	       [plus] = [1],
14.00/7.52	       
14.00/7.52	                       [1 2]     [1 2]     [0]
14.00/7.52	       [app](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
14.00/7.52	       
14.00/7.52	              [0]
14.00/7.52	       [id] = [0]
14.00/7.52	      orientation:
14.00/7.52	                        [1 2]    [1 2]    [5]    [1 2]    [1 2]    [3]                 
14.00/7.52	       plus2(s1(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = s1(plus2(x,y))
14.00/7.52	       
14.00/7.52	                [1 2]          
14.00/7.52	       id1(x) = [0 1]x >= x = x
14.00/7.52	       
14.00/7.52	                    [4]    [0]       
14.00/7.52	       plus1(0()) = [4] >= [0] = id()
14.00/7.52	       
14.00/7.52	                           [1 3]     [1 2]     [4]    [1 2]     [1 2]     [2]               
14.00/7.52	       app(plus1(x2),x3) = [0 1]x2 + [0 1]x3 + [3] >= [0 1]x2 + [0 1]x3 + [0] = plus2(x2,x3)
14.00/7.52	       
14.00/7.52	                       [1 2]     [8]    [1 2]            
14.00/7.52	       plus2(0(),x4) = [0 1]x4 + [2] >= [0 1]x4 = id1(x4)
14.00/7.52	       
14.00/7.52	                      [1 2]     [0]    [1 2]            
14.00/7.52	       app(id(),x3) = [0 1]x3 + [1] >= [0 1]x3 = id1(x3)
14.00/7.52	       
14.00/7.52	                        [1 2]     [2]    [1 1]     [0]            
14.00/7.52	       app(plus(),x3) = [0 1]x3 + [2] >= [0 1]x3 + [2] = plus1(x3)
14.00/7.52	       
14.00/7.52	                     [1 2]     [1]         [1]         
14.00/7.52	       app(s(),x3) = [0 1]x3 + [1] >= x3 + [1] = s1(x3)
14.00/7.52	      problem:
14.00/7.52	       strict:
14.00/7.52	        
14.00/7.52	       weak:
14.00/7.52	        plus2(s1(x),y) -> s1(plus2(x,y))
14.00/7.52	        id1(x) -> x
14.00/7.52	        plus1(0()) -> id()
14.00/7.52	        app(plus1(x2),x3) -> plus2(x2,x3)
14.00/7.52	        plus2(0(),x4) -> id1(x4)
14.00/7.52	        app(id(),x3) -> id1(x3)
14.00/7.52	        app(plus(),x3) -> plus1(x3)
14.00/7.52	        app(s(),x3) -> s1(x3)
14.00/7.52	      Qed
14.00/7.53	EOF