YES(?,O(n^2))
29.99/14.58	YES(?,O(n^2))
29.99/14.58	
29.99/14.58	Problem:
29.99/14.58	 merge(x,nil()) -> x
29.99/14.58	 merge(nil(),y) -> y
29.99/14.58	 merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.58	 merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.58	
29.99/14.58	Proof:
29.99/14.58	 Complexity Transformation Processor:
29.99/14.58	  strict:
29.99/14.58	   merge(x,nil()) -> x
29.99/14.58	   merge(nil(),y) -> y
29.99/14.58	   merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.58	   merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.58	  weak:
29.99/14.58	   
29.99/14.58	  Matrix Interpretation Processor: dim=1
29.99/14.58	   
29.99/14.58	   max_matrix:
29.99/14.58	    1
29.99/14.58	   interpretation:
29.99/14.58	    [v] = 214,
29.99/14.58	    
29.99/14.58	    [u] = 40,
29.99/14.58	    
29.99/14.58	    [++](x0, x1) = x0 + x1 + 6,
29.99/14.58	    
29.99/14.58	    [merge](x0, x1) = x0 + x1 + 188,
29.99/14.58	    
29.99/14.58	    [nil] = 64
29.99/14.58	   orientation:
29.99/14.58	    merge(x,nil()) = x + 252 >= x = x
29.99/14.58	    
29.99/14.58	    merge(nil(),y) = y + 252 >= y = y
29.99/14.58	    
29.99/14.58	    merge(++(x,y),++(u(),v())) = x + y + 454 >= x + y + 454 = ++(x,merge(y,++(u(),v())))
29.99/14.58	    
29.99/14.58	    merge(++(x,y),++(u(),v())) = x + y + 454 >= x + y + 454 = ++(u(),merge(++(x,y),v()))
29.99/14.58	   problem:
29.99/14.58	    strict:
29.99/14.58	     merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.58	     merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.58	    weak:
29.99/14.58	     merge(x,nil()) -> x
29.99/14.58	     merge(nil(),y) -> y
29.99/14.58	   Splitting Processor:
29.99/14.58	    strict:
29.99/14.58	     merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.58	    weak:
29.99/14.58	     merge(x,nil()) -> x
29.99/14.58	     merge(nil(),y) -> y
29.99/14.58	     merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.58	    Bounds Processor:
29.99/14.58	     bound: 4
29.99/14.58	     enrichment: match
29.99/14.58	     automaton:
29.99/14.58	      final states: {5,4,3,2,1}
29.99/14.58	      transitions:
29.99/14.58	       v3() -> 42*
29.99/14.58	       ++4(1,29) -> 54*
29.99/14.58	       ++4(56,53) -> 61*
29.99/14.58	       ++4(56,55) -> 29*
29.99/14.58	       ++4(11,46) -> 54*
29.99/14.58	       ++4(34,59) -> 29*
29.99/14.58	       ++4(45,44) -> 54*
29.99/14.58	       u4() -> 56*
29.99/14.58	       merge4(55,61) -> 55*
29.99/14.58	       merge4(54,53) -> 55*
29.99/14.58	       merge4(29,53) -> 55*
29.99/14.58	       merge4(59,61) -> 59*
29.99/14.58	       v4() -> 53*
29.99/14.58	       merge0(3,1) -> 1*
29.99/14.58	       merge0(3,3) -> 1*
29.99/14.58	       merge0(3,5) -> 1*
29.99/14.58	       merge0(4,2) -> 1*
29.99/14.58	       merge0(4,4) -> 1*
29.99/14.58	       merge0(5,1) -> 1*
29.99/14.58	       merge0(5,3) -> 1*
29.99/14.58	       merge0(5,5) -> 1*
29.99/14.58	       merge0(1,2) -> 1*
29.99/14.58	       merge0(1,4) -> 1*
29.99/14.58	       merge0(2,1) -> 1*
29.99/14.58	       merge0(2,3) -> 1*
29.99/14.58	       merge0(2,5) -> 1*
29.99/14.58	       merge0(3,2) -> 1*
29.99/14.58	       merge0(3,4) -> 1*
29.99/14.58	       merge0(4,1) -> 1*
29.99/14.58	       merge0(4,3) -> 1*
29.99/14.58	       merge0(4,5) -> 1*
29.99/14.58	       merge0(5,2) -> 1*
29.99/14.58	       merge0(5,4) -> 1*
29.99/14.58	       merge0(1,1) -> 1*
29.99/14.58	       merge0(1,3) -> 1*
29.99/14.58	       merge0(1,5) -> 1*
29.99/14.58	       merge0(2,2) -> 1*
29.99/14.58	       merge0(2,4) -> 1*
29.99/14.58	       ++0(3,1) -> 2*
29.99/14.58	       ++0(3,3) -> 2*
29.99/14.58	       ++0(3,5) -> 2*
29.99/14.58	       ++0(4,2) -> 2*
29.99/14.58	       ++0(4,4) -> 2*
29.99/14.58	       ++0(5,1) -> 2*
29.99/14.58	       ++0(5,3) -> 2*
29.99/14.58	       ++0(5,5) -> 2*
29.99/14.58	       ++0(1,2) -> 2*
29.99/14.58	       ++0(1,4) -> 2*
29.99/14.58	       ++0(2,1) -> 2*
29.99/14.58	       ++0(2,3) -> 2*
29.99/14.58	       ++0(2,5) -> 2*
29.99/14.58	       ++0(3,2) -> 2*
29.99/14.58	       ++0(3,4) -> 2*
29.99/14.58	       ++0(4,1) -> 2*
29.99/14.58	       ++0(4,3) -> 2*
29.99/14.58	       ++0(4,5) -> 2*
29.99/14.58	       ++0(5,2) -> 2*
29.99/14.58	       ++0(5,4) -> 2*
29.99/14.58	       ++0(1,1) -> 2*
29.99/14.58	       ++0(1,3) -> 2*
29.99/14.58	       ++0(1,5) -> 2*
29.99/14.58	       ++0(2,2) -> 2*
29.99/14.58	       ++0(2,4) -> 2*
29.99/14.58	       u0() -> 3*
29.99/14.58	       v0() -> 4*
29.99/14.58	       nil0() -> 5*
29.99/14.58	       ++1(3,1) -> 9*
29.99/14.58	       ++1(3,3) -> 9*
29.99/14.58	       ++1(56,55) -> 29,1
29.99/14.58	       ++1(3,5) -> 9*
29.99/14.58	       ++1(2,30) -> 29*
29.99/14.58	       ++1(4,2) -> 9*
29.99/14.58	       ++1(4,4) -> 9*
29.99/14.58	       ++1(5,1) -> 9*
29.99/14.58	       ++1(5,3) -> 9*
29.99/14.58	       ++1(5,5) -> 9*
29.99/14.58	       ++1(4,30) -> 29*
29.99/14.58	       ++1(1,2) -> 9*
29.99/14.58	       ++1(1,4) -> 9*
29.99/14.58	       ++1(11,8) -> 28*
29.99/14.58	       ++1(11,10) -> 30,29,1
29.99/14.58	       ++1(2,1) -> 9*
29.99/14.58	       ++1(2,3) -> 9*
29.99/14.58	       ++1(2,5) -> 9*
29.99/14.58	       ++1(1,30) -> 29,1
29.99/14.58	       ++1(3,2) -> 9*
29.99/14.58	       ++1(3,4) -> 9*
29.99/14.58	       ++1(11,46) -> 1*
29.99/14.58	       ++1(2,29) -> 1*
29.99/14.58	       ++1(4,1) -> 9*
29.99/14.58	       ++1(4,3) -> 9*
29.99/14.58	       ++1(4,5) -> 9*
29.99/14.58	       ++1(3,30) -> 29*
29.99/14.58	       ++1(5,2) -> 9*
29.99/14.58	       ++1(5,4) -> 9*
29.99/14.58	       ++1(34,33) -> 29,1
29.99/14.58	       ++1(4,29) -> 29*
29.99/14.58	       ++1(1,1) -> 9*
29.99/14.58	       ++1(1,3) -> 9*
29.99/14.58	       ++1(1,5) -> 9*
29.99/14.58	       ++1(5,30) -> 29*
29.99/14.58	       ++1(34,59) -> 1*
29.99/14.58	       ++1(45,44) -> 29,1
29.99/14.58	       ++1(2,2) -> 9*
29.99/14.58	       ++1(2,4) -> 9*
29.99/14.58	       ++1(1,29) -> 30,29
29.99/14.58	       u1() -> 11*
29.99/14.58	       merge1(33,1) -> 33*
29.99/14.58	       merge1(3,1) -> 30*
29.99/14.58	       merge1(29,8) -> 10*
29.99/14.58	       merge1(9,8) -> 10*
29.99/14.58	       merge1(55,1) -> 55*
29.99/14.58	       merge1(30,1) -> 30*
29.99/14.59	       merge1(5,1) -> 30*
29.99/14.59	       merge1(1,8) -> 10*
29.99/14.59	       merge1(2,1) -> 29*
29.99/14.59	       merge1(59,1) -> 33*
29.99/14.59	       merge1(44,1) -> 44*
29.99/14.59	       merge1(29,1) -> 29*
29.99/14.59	       merge1(4,1) -> 29*
29.99/14.59	       merge1(46,1) -> 10*
29.99/14.59	       merge1(1,1) -> 30*
29.99/14.59	       merge1(10,28) -> 10*
29.99/14.59	       v1() -> 8*
29.99/14.59	       ++2(56,55) -> 29,30
29.99/14.59	       ++2(11,10) -> 32*
29.99/14.59	       ++2(1,30) -> 32*
29.99/14.59	       ++2(11,46) -> 29,30
29.99/14.59	       ++2(2,29) -> 29,32
29.99/14.59	       ++2(34,33) -> 29,30
29.99/14.59	       ++2(4,29) -> 29,30
29.99/14.59	       ++2(34,59) -> 30*
29.99/14.59	       ++2(45,44) -> 29,30
29.99/14.59	       ++2(1,29) -> 29,30
29.99/14.59	       u2() -> 34*
29.99/14.59	       merge2(33,29) -> 33*
29.99/14.59	       merge2(55,29) -> 55*
29.99/14.59	       merge2(30,29) -> 29*
29.99/14.59	       merge2(30,31) -> 33*
29.99/14.59	       merge2(10,29) -> 46*
29.99/14.59	       merge2(32,31) -> 33*
29.99/14.59	       merge2(59,29) -> 33*
29.99/14.59	       merge2(44,29) -> 44*
29.99/14.59	       merge2(29,29) -> 29*
29.99/14.59	       merge2(46,29) -> 46*
29.99/14.59	       v2() -> 31*
29.99/14.59	       ++3(56,55) -> 29*
29.99/14.59	       ++3(11,46) -> 29*
29.99/14.59	       ++3(34,33) -> 43*
29.99/14.59	       ++3(34,59) -> 29*
29.99/14.59	       ++3(45,42) -> 48*
29.99/14.59	       ++3(45,44) -> 29*
29.99/14.59	       ++3(1,29) -> 29*
29.99/14.59	       u3() -> 45*
29.99/14.59	       merge3(59,48) -> 59*
29.99/14.59	       merge3(29,42) -> 44*
29.99/14.59	       merge3(44,48) -> 44*
29.99/14.59	       merge3(29,48) -> 29*
29.99/14.59	       merge3(46,48) -> 46*
29.99/14.59	       merge3(43,42) -> 44*
29.99/14.59	       merge3(33,48) -> 59*
29.99/14.59	       merge3(55,48) -> 55*
29.99/14.59	       1 -> 30*
29.99/14.59	       2 -> 29,1
29.99/14.59	       3 -> 1*
29.99/14.59	       4 -> 29,1
29.99/14.59	       5 -> 1*
29.99/14.59	       8 -> 10*
29.99/14.59	       31 -> 33*
29.99/14.59	       46 -> 10*
29.99/14.59	       59 -> 33*
29.99/14.59	     problem:
29.99/14.59	      strict:
29.99/14.59	       
29.99/14.59	      weak:
29.99/14.59	       merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.59	       merge(x,nil()) -> x
29.99/14.59	       merge(nil(),y) -> y
29.99/14.59	       merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.59	     Qed
29.99/14.59	    
29.99/14.59	    strict:
29.99/14.59	     merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.59	    weak:
29.99/14.59	     merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.59	     merge(x,nil()) -> x
29.99/14.59	     merge(nil(),y) -> y
29.99/14.59	    Matrix Interpretation Processor: dim=2
29.99/14.59	     
29.99/14.59	     max_matrix:
29.99/14.59	      [1 1]
29.99/14.59	      [0 1]
29.99/14.59	     interpretation:
29.99/14.59	            [0]
29.99/14.59	      [v] = [1],
29.99/14.59	      
29.99/14.59	            [1]
29.99/14.59	      [u] = [1],
29.99/14.59	      
29.99/14.59	                               [2]
29.99/14.59	      [++](x0, x1) = x0 + x1 + [1],
29.99/14.59	      
29.99/14.59	                        [1 1]          [1]
29.99/14.59	      [merge](x0, x1) = [0 1]x0 + x1 + [2],
29.99/14.59	      
29.99/14.59	              [2]
29.99/14.59	      [nil] = [0]
29.99/14.59	     orientation:
29.99/14.59	                                   [1 1]    [1 1]    [7]        [1 1]    [6]                             
29.99/14.59	      merge(++(x,y),++(u(),v())) = [0 1]x + [0 1]y + [6] >= x + [0 1]y + [6] = ++(x,merge(y,++(u(),v())))
29.99/14.59	      
29.99/14.59	                                   [1 1]    [1 1]    [7]    [1 1]    [1 1]    [7]                             
29.99/14.59	      merge(++(x,y),++(u(),v())) = [0 1]x + [0 1]y + [6] >= [0 1]x + [0 1]y + [6] = ++(u(),merge(++(x,y),v()))
29.99/14.59	      
29.99/14.59	                       [1 1]    [3]         
29.99/14.59	      merge(x,nil()) = [0 1]x + [2] >= x = x
29.99/14.59	      
29.99/14.59	                           [3]         
29.99/14.59	      merge(nil(),y) = y + [2] >= y = y
29.99/14.59	     problem:
29.99/14.59	      strict:
29.99/14.59	       
29.99/14.59	      weak:
29.99/14.59	       merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v())))
29.99/14.59	       merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v()))
29.99/14.59	       merge(x,nil()) -> x
29.99/14.59	       merge(nil(),y) -> y
29.99/14.59	     Qed
29.99/14.59	EOF