YES(?,O(n^2))
16.43/7.91	YES(?,O(n^2))
16.43/7.92	
16.43/7.92	Problem:
16.43/7.92	 app(app(plus(),0()),y) -> y
16.43/7.92	 app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y))
16.43/7.92	 app(app(app(curry(),f),x),y) -> app(app(f,x),y)
16.43/7.92	 add() -> app(curry(),plus())
16.43/7.92	
16.43/7.92	Proof:
16.43/7.92	 Uncurry Processor:
16.43/7.92	  plus2(0(),y) -> y
16.43/7.92	  plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.92	  curry3(f,x,y) -> app(app(f,x),y)
16.43/7.92	  add() -> curry1(plus())
16.43/7.92	  app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.92	  app(plus(),x5) -> plus1(x5)
16.43/7.92	  app(s(),x5) -> s1(x5)
16.43/7.92	  app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.92	  app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.92	  app(curry(),x5) -> curry1(x5)
16.43/7.92	  Complexity Transformation Processor:
16.43/7.92	   strict:
16.43/7.92	    plus2(0(),y) -> y
16.43/7.92	    plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.92	    curry3(f,x,y) -> app(app(f,x),y)
16.43/7.92	    add() -> curry1(plus())
16.43/7.92	    app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.92	    app(plus(),x5) -> plus1(x5)
16.43/7.92	    app(s(),x5) -> s1(x5)
16.43/7.92	    app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.92	    app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.92	    app(curry(),x5) -> curry1(x5)
16.43/7.92	   weak:
16.43/7.92	    
16.43/7.92	   Matrix Interpretation Processor: dim=1
16.43/7.92	    
16.43/7.92	    max_matrix:
16.43/7.92	     1
16.43/7.92	    interpretation:
16.43/7.92	     [curry1](x0) = x0 + 226,
16.43/7.92	     
16.43/7.92	     [curry3](x0, x1, x2) = x0 + x1 + x2,
16.43/7.92	     
16.43/7.92	     [curry2](x0, x1) = x0 + x1 + 128,
16.43/7.92	     
16.43/7.92	     [s1](x0) = x0 + 192,
16.43/7.92	     
16.43/7.92	     [plus2](x0, x1) = x0 + x1 + 24,
16.43/7.92	     
16.43/7.92	     [plus1](x0) = x0 + 136,
16.43/7.92	     
16.43/7.92	     [add] = 0,
16.43/7.92	     
16.43/7.92	     [curry] = 194,
16.43/7.92	     
16.43/7.92	     [s] = 47,
16.43/7.92	     
16.43/7.92	     [app](x0, x1) = x0 + x1 + 33,
16.43/7.92	     
16.43/7.92	     [0] = 44,
16.43/7.92	     
16.43/7.92	     [plus] = 30
16.43/7.92	    orientation:
16.43/7.92	     plus2(0(),y) = y + 68 >= y = y
16.43/7.92	     
16.43/7.92	     plus2(s1(x),y) = x + y + 216 >= x + y + 216 = s1(plus2(x,y))
16.43/7.92	     
16.43/7.92	     curry3(f,x,y) = f + x + y >= f + x + y + 66 = app(app(f,x),y)
16.43/7.92	     
16.43/7.92	     add() = 0 >= 256 = curry1(plus())
16.43/7.92	     
16.43/7.92	     app(plus1(x4),x5) = x4 + x5 + 169 >= x4 + x5 + 24 = plus2(x4,x5)
16.43/7.92	     
16.43/7.92	     app(plus(),x5) = x5 + 63 >= x5 + 136 = plus1(x5)
16.43/7.92	     
16.43/7.92	     app(s(),x5) = x5 + 80 >= x5 + 192 = s1(x5)
16.43/7.92	     
16.43/7.92	     app(curry2(x4,x3),x5) = x3 + x4 + x5 + 161 >= x3 + x4 + x5 = curry3(x4,x3,x5)
16.43/7.92	     
16.43/7.92	     app(curry1(x4),x5) = x4 + x5 + 259 >= x4 + x5 + 128 = curry2(x4,x5)
16.43/7.92	     
16.43/7.92	     app(curry(),x5) = x5 + 227 >= x5 + 226 = curry1(x5)
16.43/7.92	    problem:
16.43/7.92	     strict:
16.43/7.92	      plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.92	      curry3(f,x,y) -> app(app(f,x),y)
16.43/7.92	      add() -> curry1(plus())
16.43/7.92	      app(plus(),x5) -> plus1(x5)
16.43/7.92	      app(s(),x5) -> s1(x5)
16.43/7.92	     weak:
16.43/7.92	      plus2(0(),y) -> y
16.43/7.92	      app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.92	      app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.92	      app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.92	      app(curry(),x5) -> curry1(x5)
16.43/7.92	    Matrix Interpretation Processor: dim=1
16.43/7.92	     
16.43/7.92	     max_matrix:
16.43/7.92	      1
16.43/7.92	     interpretation:
16.43/7.92	      [curry1](x0) = x0 + 176,
16.43/7.92	      
16.43/7.92	      [curry3](x0, x1, x2) = x0 + x1 + x2,
16.43/7.92	      
16.43/7.92	      [curry2](x0, x1) = x0 + x1 + 32,
16.43/7.92	      
16.43/7.92	      [s1](x0) = x0 + 152,
16.43/7.92	      
16.43/7.92	      [plus2](x0, x1) = x0 + x1,
16.43/7.92	      
16.43/7.92	      [plus1](x0) = x0 + 76,
16.43/7.92	      
16.43/7.92	      [add] = 0,
16.43/7.92	      
16.43/7.92	      [curry] = 209,
16.43/7.92	      
16.43/7.92	      [s] = 208,
16.43/7.92	      
16.43/7.92	      [app](x0, x1) = x0 + x1 + 88,
16.43/7.92	      
16.43/7.92	      [0] = 0,
16.43/7.92	      
16.43/7.92	      [plus] = 0
16.43/7.92	     orientation:
16.43/7.92	      plus2(s1(x),y) = x + y + 152 >= x + y + 152 = s1(plus2(x,y))
16.43/7.92	      
16.43/7.92	      curry3(f,x,y) = f + x + y >= f + x + y + 176 = app(app(f,x),y)
16.43/7.92	      
16.43/7.92	      add() = 0 >= 176 = curry1(plus())
16.43/7.92	      
16.43/7.92	      app(plus(),x5) = x5 + 88 >= x5 + 76 = plus1(x5)
16.43/7.92	      
16.43/7.92	      app(s(),x5) = x5 + 296 >= x5 + 152 = s1(x5)
16.43/7.92	      
16.43/7.92	      plus2(0(),y) = y >= y = y
16.43/7.92	      
16.43/7.92	      app(plus1(x4),x5) = x4 + x5 + 164 >= x4 + x5 = plus2(x4,x5)
16.43/7.92	      
16.43/7.92	      app(curry2(x4,x3),x5) = x3 + x4 + x5 + 120 >= x3 + x4 + x5 = curry3(x4,x3,x5)
16.43/7.92	      
16.43/7.92	      app(curry1(x4),x5) = x4 + x5 + 264 >= x4 + x5 + 32 = curry2(x4,x5)
16.43/7.92	      
16.43/7.92	      app(curry(),x5) = x5 + 297 >= x5 + 176 = curry1(x5)
16.43/7.92	     problem:
16.43/7.92	      strict:
16.43/7.92	       plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.92	       curry3(f,x,y) -> app(app(f,x),y)
16.43/7.92	       add() -> curry1(plus())
16.43/7.92	      weak:
16.43/7.92	       app(plus(),x5) -> plus1(x5)
16.43/7.92	       app(s(),x5) -> s1(x5)
16.43/7.92	       plus2(0(),y) -> y
16.43/7.92	       app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.92	       app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.92	       app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.92	       app(curry(),x5) -> curry1(x5)
16.43/7.92	     Matrix Interpretation Processor: dim=1
16.43/7.93	      
16.43/7.93	      max_matrix:
16.43/7.93	       1
16.43/7.93	      interpretation:
16.43/7.93	       [curry1](x0) = x0 + 19,
16.43/7.93	       
16.43/7.93	       [curry3](x0, x1, x2) = x0 + x1 + x2 + 20,
16.43/7.93	       
16.43/7.93	       [curry2](x0, x1) = x0 + x1,
16.43/7.93	       
16.43/7.93	       [s1](x0) = x0 + 66,
16.43/7.93	       
16.43/7.93	       [plus2](x0, x1) = x0 + x1 + 128,
16.43/7.93	       
16.43/7.93	       [plus1](x0) = x0 + 192,
16.43/7.93	       
16.43/7.93	       [add] = 240,
16.43/7.93	       
16.43/7.93	       [curry] = 8,
16.43/7.93	       
16.43/7.93	       [s] = 128,
16.43/7.93	       
16.43/7.93	       [app](x0, x1) = x0 + x1 + 20,
16.43/7.93	       
16.43/7.93	       [0] = 33,
16.43/7.93	       
16.43/7.93	       [plus] = 218
16.43/7.93	      orientation:
16.43/7.93	       plus2(s1(x),y) = x + y + 194 >= x + y + 194 = s1(plus2(x,y))
16.43/7.93	       
16.43/7.93	       curry3(f,x,y) = f + x + y + 20 >= f + x + y + 40 = app(app(f,x),y)
16.43/7.93	       
16.43/7.93	       add() = 240 >= 237 = curry1(plus())
16.43/7.93	       
16.43/7.93	       app(plus(),x5) = x5 + 238 >= x5 + 192 = plus1(x5)
16.43/7.93	       
16.43/7.93	       app(s(),x5) = x5 + 148 >= x5 + 66 = s1(x5)
16.43/7.93	       
16.43/7.93	       plus2(0(),y) = y + 161 >= y = y
16.43/7.93	       
16.43/7.93	       app(plus1(x4),x5) = x4 + x5 + 212 >= x4 + x5 + 128 = plus2(x4,x5)
16.43/7.93	       
16.43/7.93	       app(curry2(x4,x3),x5) = x3 + x4 + x5 + 20 >= x3 + x4 + x5 + 20 = curry3(x4,x3,x5)
16.43/7.93	       
16.43/7.93	       app(curry1(x4),x5) = x4 + x5 + 39 >= x4 + x5 = curry2(x4,x5)
16.43/7.93	       
16.43/7.93	       app(curry(),x5) = x5 + 28 >= x5 + 19 = curry1(x5)
16.43/7.93	      problem:
16.43/7.93	       strict:
16.43/7.93	        plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.93	        curry3(f,x,y) -> app(app(f,x),y)
16.43/7.93	       weak:
16.43/7.93	        add() -> curry1(plus())
16.43/7.93	        app(plus(),x5) -> plus1(x5)
16.43/7.93	        app(s(),x5) -> s1(x5)
16.43/7.93	        plus2(0(),y) -> y
16.43/7.93	        app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.93	        app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.93	        app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.93	        app(curry(),x5) -> curry1(x5)
16.43/7.93	      Matrix Interpretation Processor: dim=1
16.43/7.93	       
16.43/7.93	       max_matrix:
16.43/7.93	        1
16.43/7.93	       interpretation:
16.43/7.93	        [curry1](x0) = x0 + 65,
16.43/7.93	        
16.43/7.93	        [curry3](x0, x1, x2) = x0 + x1 + x2 + 193,
16.43/7.93	        
16.43/7.93	        [curry2](x0, x1) = x0 + x1 + 129,
16.43/7.93	        
16.43/7.93	        [s1](x0) = x0 + 40,
16.43/7.93	        
16.43/7.93	        [plus2](x0, x1) = x0 + x1 + 2,
16.43/7.93	        
16.43/7.93	        [plus1](x0) = x0 + 128,
16.43/7.93	        
16.43/7.93	        [add] = 129,
16.43/7.93	        
16.43/7.93	        [curry] = 2,
16.43/7.93	        
16.43/7.93	        [s] = 24,
16.43/7.93	        
16.43/7.93	        [app](x0, x1) = x0 + x1 + 64,
16.43/7.93	        
16.43/7.93	        [0] = 15,
16.43/7.93	        
16.43/7.93	        [plus] = 64
16.43/7.93	       orientation:
16.43/7.93	        plus2(s1(x),y) = x + y + 42 >= x + y + 42 = s1(plus2(x,y))
16.43/7.93	        
16.43/7.93	        curry3(f,x,y) = f + x + y + 193 >= f + x + y + 128 = app(app(f,x),y)
16.43/7.93	        
16.43/7.93	        add() = 129 >= 129 = curry1(plus())
16.43/7.93	        
16.43/7.93	        app(plus(),x5) = x5 + 128 >= x5 + 128 = plus1(x5)
16.43/7.93	        
16.43/7.93	        app(s(),x5) = x5 + 88 >= x5 + 40 = s1(x5)
16.43/7.93	        
16.43/7.93	        plus2(0(),y) = y + 17 >= y = y
16.43/7.93	        
16.43/7.93	        app(plus1(x4),x5) = x4 + x5 + 192 >= x4 + x5 + 2 = plus2(x4,x5)
16.43/7.93	        
16.43/7.93	        app(curry2(x4,x3),x5) = x3 + x4 + x5 + 193 >= x3 + x4 + x5 + 193 = curry3(x4,x3,x5)
16.43/7.93	        
16.43/7.93	        app(curry1(x4),x5) = x4 + x5 + 129 >= x4 + x5 + 129 = curry2(x4,x5)
16.43/7.93	        
16.43/7.93	        app(curry(),x5) = x5 + 66 >= x5 + 65 = curry1(x5)
16.43/7.93	       problem:
16.43/7.93	        strict:
16.43/7.93	         plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.93	        weak:
16.43/7.93	         curry3(f,x,y) -> app(app(f,x),y)
16.43/7.93	         add() -> curry1(plus())
16.43/7.93	         app(plus(),x5) -> plus1(x5)
16.43/7.93	         app(s(),x5) -> s1(x5)
16.43/7.93	         plus2(0(),y) -> y
16.43/7.93	         app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.93	         app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.93	         app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.93	         app(curry(),x5) -> curry1(x5)
16.43/7.93	       Matrix Interpretation Processor: dim=2
16.43/7.93	        
16.43/7.93	        max_matrix:
16.43/7.93	         [1 2]
16.43/7.93	         [0 1]
16.43/7.93	        interpretation:
16.43/7.93	                          
16.43/7.93	         [curry1](x0) = x0,
16.43/7.93	         
16.43/7.93	                                [1 2]     [1 1]       
16.43/7.93	         [curry3](x0, x1, x2) = [0 1]x0 + [0 1]x1 + x2,
16.43/7.93	         
16.43/7.93	                            [1 1]       
16.43/7.93	         [curry2](x0, x1) = [0 1]x0 + x1,
16.43/7.93	         
16.43/7.93	                         [0]
16.43/7.93	         [s1](x0) = x0 + [2],
16.43/7.93	         
16.43/7.93	                           [1 1]       
16.43/7.93	         [plus2](x0, x1) = [0 1]x0 + x1,
16.43/7.93	         
16.43/7.93	                            [2]
16.43/7.93	         [plus1](x0) = x0 + [1],
16.43/7.93	         
16.43/7.93	                 [2]
16.43/7.93	         [add] = [3],
16.43/7.93	         
16.43/7.93	                   [2]
16.43/7.93	         [curry] = [0],
16.43/7.93	         
16.43/7.93	               [0]
16.43/7.93	         [s] = [3],
16.43/7.93	         
16.43/7.93	                         [1 1]       
16.43/7.93	         [app](x0, x1) = [0 1]x0 + x1,
16.43/7.93	         
16.43/7.93	               [3]
16.43/7.93	         [0] = [0],
16.43/7.93	         
16.43/7.93	                  [0]
16.43/7.93	         [plus] = [3]
16.43/7.93	        orientation:
16.43/7.93	                          [1 1]        [2]    [1 1]        [0]                 
16.43/7.93	         plus2(s1(x),y) = [0 1]x + y + [2] >= [0 1]x + y + [2] = s1(plus2(x,y))
16.43/7.93	         
16.43/7.93	                         [1 2]    [1 1]         [1 2]    [1 1]                       
16.43/7.93	         curry3(f,x,y) = [0 1]f + [0 1]x + y >= [0 1]f + [0 1]x + y = app(app(f,x),y)
16.43/7.93	         
16.43/7.93	                 [2]    [0]                 
16.43/7.93	         add() = [3] >= [3] = curry1(plus())
16.43/7.93	         
16.43/7.93	                               [3]         [2]            
16.43/7.93	         app(plus(),x5) = x5 + [3] >= x5 + [1] = plus1(x5)
16.43/7.93	         
16.43/7.93	                            [3]         [0]         
16.43/7.93	         app(s(),x5) = x5 + [3] >= x5 + [2] = s1(x5)
16.43/7.93	         
16.43/7.93	                            [3]         
16.43/7.93	         plus2(0(),y) = y + [0] >= y = y
16.43/7.93	         
16.43/7.93	                             [1 1]          [3]    [1 1]                      
16.43/7.93	         app(plus1(x4),x5) = [0 1]x4 + x5 + [1] >= [0 1]x4 + x5 = plus2(x4,x5)
16.43/7.93	         
16.43/7.93	                                 [1 1]     [1 2]           [1 1]     [1 2]                          
16.43/7.93	         app(curry2(x4,x3),x5) = [0 1]x3 + [0 1]x4 + x5 >= [0 1]x3 + [0 1]x4 + x5 = curry3(x4,x3,x5)
16.43/7.93	         
16.43/7.93	                              [1 1]           [1 1]                       
16.43/7.93	         app(curry1(x4),x5) = [0 1]x4 + x5 >= [0 1]x4 + x5 = curry2(x4,x5)
16.43/7.93	         
16.43/7.93	                                [2]                   
16.43/7.93	         app(curry(),x5) = x5 + [0] >= x5 = curry1(x5)
16.43/7.93	        problem:
16.43/7.93	         strict:
16.43/7.93	          
16.43/7.93	         weak:
16.43/7.93	          plus2(s1(x),y) -> s1(plus2(x,y))
16.43/7.93	          curry3(f,x,y) -> app(app(f,x),y)
16.43/7.93	          add() -> curry1(plus())
16.43/7.93	          app(plus(),x5) -> plus1(x5)
16.43/7.93	          app(s(),x5) -> s1(x5)
16.43/7.93	          plus2(0(),y) -> y
16.43/7.93	          app(plus1(x4),x5) -> plus2(x4,x5)
16.43/7.93	          app(curry2(x4,x3),x5) -> curry3(x4,x3,x5)
16.43/7.93	          app(curry1(x4),x5) -> curry2(x4,x5)
16.43/7.93	          app(curry(),x5) -> curry1(x5)
16.43/7.93	        Qed
16.43/7.93	EOF