YES(?,O(n^1))
0.16/0.25	YES(?,O(n^1))
0.16/0.25	
0.16/0.25	Problem:
0.16/0.25	 app(app(app(compose(),f),g),x) -> app(f,app(g,x))
0.16/0.25	
0.16/0.25	Proof:
0.16/0.25	 Uncurry Processor:
0.16/0.25	  compose3(f,g,x) -> app(f,app(g,x))
0.16/0.25	  app(compose2(x4,x3),x5) -> compose3(x4,x3,x5)
0.16/0.25	  app(compose1(x4),x5) -> compose2(x4,x5)
0.16/0.25	  app(compose(),x5) -> compose1(x5)
0.16/0.25	  Complexity Transformation Processor:
0.16/0.25	   strict:
0.16/0.25	    compose3(f,g,x) -> app(f,app(g,x))
0.16/0.25	    app(compose2(x4,x3),x5) -> compose3(x4,x3,x5)
0.16/0.25	    app(compose1(x4),x5) -> compose2(x4,x5)
0.16/0.25	    app(compose(),x5) -> compose1(x5)
0.16/0.25	   weak:
0.16/0.25	    
0.16/0.25	   Matrix Interpretation Processor: dim=1
0.16/0.25	    
0.16/0.25	    max_matrix:
0.16/0.25	     1
0.16/0.25	    interpretation:
0.16/0.25	     [compose1](x0) = x0 + 18,
0.16/0.25	     
0.16/0.25	     [compose3](x0, x1, x2) = x0 + x1 + x2,
0.16/0.25	     
0.16/0.25	     [compose2](x0, x1) = x0 + x1 + 130,
0.16/0.25	     
0.16/0.25	     [app](x0, x1) = x0 + x1 + 120,
0.16/0.25	     
0.16/0.25	     [compose] = 7
0.16/0.25	    orientation:
0.16/0.25	     compose3(f,g,x) = f + g + x >= f + g + x + 240 = app(f,app(g,x))
0.16/0.25	     
0.16/0.25	     app(compose2(x4,x3),x5) = x3 + x4 + x5 + 250 >= x3 + x4 + x5 = compose3(x4,x3,x5)
0.16/0.25	     
0.16/0.25	     app(compose1(x4),x5) = x4 + x5 + 138 >= x4 + x5 + 130 = compose2(x4,x5)
0.16/0.25	     
0.16/0.25	     app(compose(),x5) = x5 + 127 >= x5 + 18 = compose1(x5)
0.16/0.25	    problem:
0.16/0.25	     strict:
0.16/0.25	      compose3(f,g,x) -> app(f,app(g,x))
0.16/0.25	     weak:
0.16/0.25	      app(compose2(x4,x3),x5) -> compose3(x4,x3,x5)
0.16/0.25	      app(compose1(x4),x5) -> compose2(x4,x5)
0.16/0.25	      app(compose(),x5) -> compose1(x5)
0.16/0.25	    Matrix Interpretation Processor: dim=1
0.16/0.25	     
0.16/0.25	     max_matrix:
0.16/0.25	      1
0.16/0.25	     interpretation:
0.16/0.25	      [compose1](x0) = x0 + 1,
0.16/0.25	      
0.16/0.25	      [compose3](x0, x1, x2) = x0 + x1 + x2 + 1,
0.16/0.25	      
0.16/0.25	      [compose2](x0, x1) = x0 + x1 + 1,
0.16/0.25	      
0.16/0.25	      [app](x0, x1) = x0 + x1,
0.16/0.25	      
0.16/0.25	      [compose] = 1
0.16/0.25	     orientation:
0.16/0.25	      compose3(f,g,x) = f + g + x + 1 >= f + g + x = app(f,app(g,x))
0.16/0.25	      
0.16/0.25	      app(compose2(x4,x3),x5) = x3 + x4 + x5 + 1 >= x3 + x4 + x5 + 1 = compose3(x4,x3,x5)
0.16/0.25	      
0.16/0.25	      app(compose1(x4),x5) = x4 + x5 + 1 >= x4 + x5 + 1 = compose2(x4,x5)
0.16/0.25	      
0.16/0.25	      app(compose(),x5) = x5 + 1 >= x5 + 1 = compose1(x5)
0.16/0.25	     problem:
0.16/0.25	      strict:
0.16/0.25	       
0.16/0.25	      weak:
0.16/0.25	       compose3(f,g,x) -> app(f,app(g,x))
0.16/0.25	       app(compose2(x4,x3),x5) -> compose3(x4,x3,x5)
0.16/0.25	       app(compose1(x4),x5) -> compose2(x4,x5)
0.16/0.25	       app(compose(),x5) -> compose1(x5)
0.16/0.25	     Qed
0.16/0.26	EOF