YES(?,O(n^1))
48.95/13.37	YES(?,O(n^1))
48.95/13.37	
48.95/13.37	Problem:
48.95/13.37	 active(f(X,X)) -> mark(f(a(),b()))
48.95/13.37	 active(b()) -> mark(a())
48.95/13.37	 active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.37	 f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.37	 proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.37	 proper(a()) -> ok(a())
48.95/13.37	 proper(b()) -> ok(b())
48.95/13.37	 f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.37	 top(mark(X)) -> top(proper(X))
48.95/13.37	 top(ok(X)) -> top(active(X))
48.95/13.37	
48.95/13.37	Proof:
48.95/13.37	 Complexity Transformation Processor:
48.95/13.37	  strict:
48.95/13.37	   active(f(X,X)) -> mark(f(a(),b()))
48.95/13.37	   active(b()) -> mark(a())
48.95/13.37	   active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.37	   f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.37	   proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.37	   proper(a()) -> ok(a())
48.95/13.37	   proper(b()) -> ok(b())
48.95/13.37	   f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.37	   top(mark(X)) -> top(proper(X))
48.95/13.37	   top(ok(X)) -> top(active(X))
48.95/13.37	  weak:
48.95/13.37	   
48.95/13.37	  Matrix Interpretation Processor: dim=1
48.95/13.37	   
48.95/13.37	   max_matrix:
48.95/13.37	    1
48.95/13.37	   interpretation:
48.95/13.37	    [top](x0) = x0,
48.95/13.37	    
48.95/13.37	    [ok](x0) = x0 + 7,
48.95/13.37	    
48.95/13.37	    [proper](x0) = x0,
48.95/13.37	    
48.95/13.37	    [mark](x0) = x0 + 6,
48.95/13.37	    
48.95/13.37	    [b] = 8,
48.95/13.37	    
48.95/13.37	    [a] = 0,
48.95/13.37	    
48.95/13.37	    [active](x0) = x0 + 4,
48.95/13.37	    
48.95/13.37	    [f](x0, x1) = x0 + x1
48.95/13.37	   orientation:
48.95/13.37	    active(f(X,X)) = 2X + 4 >= 14 = mark(f(a(),b()))
48.95/13.37	    
48.95/13.37	    active(b()) = 12 >= 6 = mark(a())
48.95/13.37	    
48.95/13.37	    active(f(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = f(active(X1),X2)
48.95/13.37	    
48.95/13.37	    f(mark(X1),X2) = X1 + X2 + 6 >= X1 + X2 + 6 = mark(f(X1,X2))
48.95/13.37	    
48.95/13.37	    proper(f(X1,X2)) = X1 + X2 >= X1 + X2 = f(proper(X1),proper(X2))
48.95/13.37	    
48.95/13.37	    proper(a()) = 0 >= 7 = ok(a())
48.95/13.37	    
48.95/13.37	    proper(b()) = 8 >= 15 = ok(b())
48.95/13.37	    
48.95/13.37	    f(ok(X1),ok(X2)) = X1 + X2 + 14 >= X1 + X2 + 7 = ok(f(X1,X2))
48.95/13.37	    
48.95/13.37	    top(mark(X)) = X + 6 >= X = top(proper(X))
48.95/13.37	    
48.95/13.37	    top(ok(X)) = X + 7 >= X + 4 = top(active(X))
48.95/13.37	   problem:
48.95/13.37	    strict:
48.95/13.37	     active(f(X,X)) -> mark(f(a(),b()))
48.95/13.37	     active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.37	     f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.37	     proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.37	     proper(a()) -> ok(a())
48.95/13.37	     proper(b()) -> ok(b())
48.95/13.37	    weak:
48.95/13.37	     active(b()) -> mark(a())
48.95/13.37	     f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.37	     top(mark(X)) -> top(proper(X))
48.95/13.37	     top(ok(X)) -> top(active(X))
48.95/13.37	   Matrix Interpretation Processor: dim=1
48.95/13.37	    
48.95/13.37	    max_matrix:
48.95/13.37	     1
48.95/13.37	    interpretation:
48.95/13.37	     [top](x0) = x0,
48.95/13.37	     
48.95/13.37	     [ok](x0) = x0,
48.95/13.37	     
48.95/13.37	     [proper](x0) = x0 + 2,
48.95/13.37	     
48.95/13.37	     [mark](x0) = x0 + 2,
48.95/13.37	     
48.95/13.37	     [b] = 10,
48.95/13.37	     
48.95/13.37	     [a] = 8,
48.95/13.37	     
48.95/13.37	     [active](x0) = x0,
48.95/13.37	     
48.95/13.37	     [f](x0, x1) = x0 + x1 + 9
48.95/13.37	    orientation:
48.95/13.37	     active(f(X,X)) = 2X + 9 >= 29 = mark(f(a(),b()))
48.95/13.37	     
48.95/13.37	     active(f(X1,X2)) = X1 + X2 + 9 >= X1 + X2 + 9 = f(active(X1),X2)
48.95/13.37	     
48.95/13.37	     f(mark(X1),X2) = X1 + X2 + 11 >= X1 + X2 + 11 = mark(f(X1,X2))
48.95/13.37	     
48.95/13.37	     proper(f(X1,X2)) = X1 + X2 + 11 >= X1 + X2 + 13 = f(proper(X1),proper(X2))
48.95/13.37	     
48.95/13.37	     proper(a()) = 10 >= 8 = ok(a())
48.95/13.37	     
48.95/13.37	     proper(b()) = 12 >= 10 = ok(b())
48.95/13.37	     
48.95/13.37	     active(b()) = 10 >= 10 = mark(a())
48.95/13.37	     
48.95/13.37	     f(ok(X1),ok(X2)) = X1 + X2 + 9 >= X1 + X2 + 9 = ok(f(X1,X2))
48.95/13.37	     
48.95/13.37	     top(mark(X)) = X + 2 >= X + 2 = top(proper(X))
48.95/13.37	     
48.95/13.37	     top(ok(X)) = X >= X = top(active(X))
48.95/13.37	    problem:
48.95/13.37	     strict:
48.95/13.37	      active(f(X,X)) -> mark(f(a(),b()))
48.95/13.37	      active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.37	      f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.37	      proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.37	     weak:
48.95/13.37	      proper(a()) -> ok(a())
48.95/13.37	      proper(b()) -> ok(b())
48.95/13.37	      active(b()) -> mark(a())
48.95/13.37	      f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.37	      top(mark(X)) -> top(proper(X))
48.95/13.37	      top(ok(X)) -> top(active(X))
48.95/13.37	    Bounds Processor:
48.95/13.37	     bound: 0
48.95/13.37	     enrichment: match
48.95/13.37	     automaton:
48.95/13.37	      final states: {13,10,8,7,6,5}
48.95/13.37	      transitions:
48.95/13.37	       active0(10) -> 5*
48.95/13.37	       active0(2) -> 5*
48.95/13.37	       active0(4) -> 5*
48.95/13.37	       active0(1) -> 5*
48.95/13.37	       active0(13) -> 5*
48.95/13.37	       active0(3) -> 5*
48.95/13.37	       f0(13,1) -> 6*
48.95/13.37	       f0(13,3) -> 6*
48.95/13.37	       f0(3,1) -> 6*
48.95/13.37	       f0(3,3) -> 6*
48.95/13.37	       f0(13,13) -> 6*
48.95/13.37	       f0(3,13) -> 6*
48.95/13.37	       f0(4,2) -> 6*
48.95/13.37	       f0(4,4) -> 6*
48.95/13.37	       f0(4,10) -> 6*
48.95/13.37	       f0(10,1) -> 6*
48.95/13.37	       f0(10,3) -> 6*
48.95/13.37	       f0(10,13) -> 6*
48.95/13.37	       f0(1,2) -> 6*
48.95/13.37	       f0(1,4) -> 6*
48.95/13.37	       f0(1,10) -> 6*
48.95/13.37	       f0(2,1) -> 6*
48.95/13.37	       f0(2,3) -> 6*
48.95/13.37	       f0(2,13) -> 6*
48.95/13.37	       f0(13,2) -> 6*
48.95/13.37	       f0(13,4) -> 6*
48.95/13.37	       f0(3,2) -> 6*
48.95/13.37	       f0(3,4) -> 6*
48.95/13.38	       f0(13,10) -> 6*
48.95/13.38	       f0(3,10) -> 6*
48.95/13.38	       f0(4,1) -> 6*
48.95/13.38	       f0(4,3) -> 6*
48.95/13.38	       f0(4,13) -> 6*
48.95/13.38	       f0(10,2) -> 6*
48.95/13.38	       f0(10,4) -> 6*
48.95/13.38	       f0(10,10) -> 6*
48.95/13.38	       f0(1,1) -> 6*
48.95/13.38	       f0(1,3) -> 6*
48.95/13.38	       f0(1,13) -> 6*
48.95/13.38	       f0(2,2) -> 6*
48.95/13.38	       f0(2,4) -> 6*
48.95/13.38	       f0(2,10) -> 6*
48.95/13.38	       mark0(10) -> 1*
48.95/13.38	       mark0(2) -> 13*,5,1
48.95/13.38	       mark0(4) -> 1*
48.95/13.38	       mark0(6) -> 6*
48.95/13.38	       mark0(1) -> 1*
48.95/13.38	       mark0(13) -> 1*
48.95/13.38	       mark0(3) -> 1*
48.95/13.38	       a0() -> 2*
48.95/13.38	       b0() -> 3*
48.95/13.38	       proper0(10) -> 7*
48.95/13.38	       proper0(2) -> 7*
48.95/13.38	       proper0(4) -> 7*
48.95/13.38	       proper0(1) -> 7*
48.95/13.38	       proper0(13) -> 7*
48.95/13.38	       proper0(3) -> 7*
48.95/13.38	       ok0(10) -> 4*
48.95/13.38	       ok0(2) -> 10*,7,4
48.95/13.38	       ok0(4) -> 4*
48.95/13.38	       ok0(6) -> 6*
48.95/13.38	       ok0(1) -> 4*
48.95/13.38	       ok0(13) -> 4*
48.95/13.38	       ok0(3) -> 10*,7,4
48.95/13.38	       top0(10) -> 8*
48.95/13.38	       top0(5) -> 8*
48.95/13.38	       top0(7) -> 8*
48.95/13.38	       top0(2) -> 8*
48.95/13.38	       top0(4) -> 8*
48.95/13.38	       top0(1) -> 8*
48.95/13.38	       top0(13) -> 8*
48.95/13.38	       top0(3) -> 8*
48.95/13.38	     problem:
48.95/13.38	      strict:
48.95/13.38	       active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.38	       f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.38	       proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.38	      weak:
48.95/13.38	       active(f(X,X)) -> mark(f(a(),b()))
48.95/13.38	       proper(a()) -> ok(a())
48.95/13.38	       proper(b()) -> ok(b())
48.95/13.38	       active(b()) -> mark(a())
48.95/13.38	       f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.38	       top(mark(X)) -> top(proper(X))
48.95/13.38	       top(ok(X)) -> top(active(X))
48.95/13.38	     Bounds Processor:
48.95/13.38	      bound: 0
48.95/13.38	      enrichment: match
48.95/13.38	      automaton:
48.95/13.38	       final states: {12,10,8,7,6,5}
48.95/13.38	       transitions:
48.95/13.38	        active0(10) -> 5*
48.95/13.38	        active0(12) -> 5*
48.95/13.38	        active0(2) -> 5*
48.95/13.38	        active0(4) -> 5*
48.95/13.38	        active0(1) -> 5*
48.95/13.38	        active0(3) -> 5*
48.95/13.38	        f0(2,12) -> 6*
48.95/13.38	        f0(3,1) -> 6*
48.95/13.38	        f0(3,3) -> 6*
48.95/13.38	        f0(4,2) -> 6*
48.95/13.38	        f0(4,4) -> 6*
48.95/13.38	        f0(4,10) -> 6*
48.95/13.38	        f0(4,12) -> 6*
48.95/13.38	        f0(10,1) -> 6*
48.95/13.38	        f0(10,3) -> 6*
48.95/13.38	        f0(1,2) -> 6*
48.95/13.38	        f0(1,4) -> 6*
48.95/13.38	        f0(1,10) -> 6*
48.95/13.38	        f0(1,12) -> 6*
48.95/13.38	        f0(12,1) -> 6*
48.95/13.38	        f0(12,3) -> 6*
48.95/13.38	        f0(2,1) -> 6*
48.95/13.38	        f0(2,3) -> 6*
48.95/13.38	        f0(3,2) -> 6*
48.95/13.38	        f0(3,4) -> 6*
48.95/13.38	        f0(3,10) -> 6*
48.95/13.38	        f0(3,12) -> 6*
48.95/13.38	        f0(4,1) -> 6*
48.95/13.38	        f0(4,3) -> 6*
48.95/13.38	        f0(10,2) -> 6*
48.95/13.38	        f0(10,4) -> 6*
48.95/13.38	        f0(10,10) -> 6*
48.95/13.38	        f0(10,12) -> 6*
48.95/13.38	        f0(1,1) -> 6*
48.95/13.38	        f0(1,3) -> 6*
48.95/13.38	        f0(12,2) -> 6*
48.95/13.38	        f0(12,4) -> 6*
48.95/13.38	        f0(2,2) -> 6*
48.95/13.38	        f0(2,4) -> 6*
48.95/13.38	        f0(12,10) -> 6*
48.95/13.38	        f0(12,12) -> 6*
48.95/13.38	        f0(2,10) -> 6*
48.95/13.38	        mark0(10) -> 1*
48.95/13.38	        mark0(12) -> 1*
48.95/13.38	        mark0(2) -> 12*,5,1
48.95/13.38	        mark0(4) -> 1*
48.95/13.38	        mark0(6) -> 6*
48.95/13.38	        mark0(1) -> 1*
48.95/13.38	        mark0(3) -> 1*
48.95/13.38	        a0() -> 2*
48.95/13.38	        b0() -> 3*
48.95/13.38	        proper0(10) -> 7*
48.95/13.38	        proper0(12) -> 7*
48.95/13.38	        proper0(2) -> 7*
48.95/13.38	        proper0(4) -> 7*
48.95/13.38	        proper0(1) -> 7*
48.95/13.38	        proper0(3) -> 7*
48.95/13.38	        ok0(10) -> 4*
48.95/13.38	        ok0(12) -> 4*
48.95/13.38	        ok0(2) -> 10*,7,4
48.95/13.38	        ok0(4) -> 4*
48.95/13.38	        ok0(6) -> 6*
48.95/13.38	        ok0(1) -> 4*
48.95/13.38	        ok0(3) -> 10*,7,4
48.95/13.38	        top0(10) -> 8*
48.95/13.38	        top0(5) -> 8*
48.95/13.38	        top0(12) -> 8*
48.95/13.38	        top0(7) -> 8*
48.95/13.38	        top0(2) -> 8*
48.95/13.38	        top0(4) -> 8*
48.95/13.38	        top0(1) -> 8*
48.95/13.38	        top0(3) -> 8*
48.95/13.38	      problem:
48.95/13.38	       strict:
48.95/13.38	        f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.38	        proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.38	       weak:
48.95/13.38	        active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.38	        active(f(X,X)) -> mark(f(a(),b()))
48.95/13.38	        proper(a()) -> ok(a())
48.95/13.38	        proper(b()) -> ok(b())
48.95/13.38	        active(b()) -> mark(a())
48.95/13.38	        f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.38	        top(mark(X)) -> top(proper(X))
48.95/13.38	        top(ok(X)) -> top(active(X))
48.95/13.38	      Bounds Processor:
48.95/13.38	       bound: 0
48.95/13.38	       enrichment: match
48.95/13.38	       automaton:
48.95/13.38	        final states: {11,10,8,7,6,5}
48.95/13.38	        transitions:
48.95/13.38	         active0(10) -> 7*
48.95/13.38	         active0(2) -> 7*
48.95/13.38	         active0(4) -> 7*
48.95/13.38	         active0(11) -> 7*
48.95/13.38	         active0(1) -> 7*
48.95/13.38	         active0(3) -> 7*
48.95/13.38	         f0(3,1) -> 5*
48.95/13.38	         f0(3,3) -> 5*
48.95/13.38	         f0(3,11) -> 5*
48.95/13.38	         f0(4,2) -> 5*
48.95/13.38	         f0(4,4) -> 5*
48.95/13.38	         f0(4,10) -> 5*
48.95/13.38	         f0(10,1) -> 5*
48.95/13.38	         f0(10,3) -> 5*
48.95/13.38	         f0(10,11) -> 5*
48.95/13.38	         f0(11,2) -> 5*
48.95/13.38	         f0(11,4) -> 5*
48.95/13.38	         f0(1,2) -> 5*
48.95/13.38	         f0(1,4) -> 5*
48.95/13.38	         f0(11,10) -> 5*
48.95/13.38	         f0(1,10) -> 5*
48.95/13.38	         f0(2,1) -> 5*
48.95/13.38	         f0(2,3) -> 5*
48.95/13.38	         f0(2,11) -> 5*
48.95/13.38	         f0(3,2) -> 5*
48.95/13.38	         f0(3,4) -> 5*
48.95/13.38	         f0(3,10) -> 5*
48.95/13.38	         f0(4,1) -> 5*
48.95/13.38	         f0(4,3) -> 5*
48.95/13.38	         f0(4,11) -> 5*
48.95/13.38	         f0(10,2) -> 5*
48.95/13.38	         f0(10,4) -> 5*
48.95/13.38	         f0(10,10) -> 5*
48.95/13.38	         f0(11,1) -> 5*
48.95/13.38	         f0(11,3) -> 5*
48.95/13.38	         f0(1,1) -> 5*
48.95/13.38	         f0(1,3) -> 5*
48.95/13.38	         f0(11,11) -> 5*
48.95/13.38	         f0(1,11) -> 5*
48.95/13.38	         f0(2,2) -> 5*
48.95/13.38	         f0(2,4) -> 5*
48.95/13.38	         f0(2,10) -> 5*
48.95/13.38	         mark0(10) -> 1*
48.95/13.38	         mark0(5) -> 5*
48.95/13.38	         mark0(2) -> 11*,7,1
48.95/13.38	         mark0(4) -> 1*
48.95/13.38	         mark0(11) -> 1*
48.95/13.38	         mark0(1) -> 1*
48.95/13.38	         mark0(3) -> 1*
48.95/13.38	         a0() -> 2*
48.95/13.38	         b0() -> 3*
48.95/13.38	         proper0(10) -> 6*
48.95/13.38	         proper0(2) -> 6*
48.95/13.38	         proper0(4) -> 6*
48.95/13.38	         proper0(11) -> 6*
48.95/13.38	         proper0(1) -> 6*
48.95/13.38	         proper0(3) -> 6*
48.95/13.38	         ok0(10) -> 4*
48.95/13.38	         ok0(5) -> 5*
48.95/13.38	         ok0(2) -> 10*,6,4
48.95/13.38	         ok0(4) -> 4*
48.95/13.38	         ok0(11) -> 4*
48.95/13.38	         ok0(1) -> 4*
48.95/13.38	         ok0(3) -> 10*,6,4
48.95/13.38	         top0(10) -> 8*
48.95/13.38	         top0(7) -> 8*
48.95/13.38	         top0(2) -> 8*
48.95/13.38	         top0(4) -> 8*
48.95/13.38	         top0(11) -> 8*
48.95/13.38	         top0(6) -> 8*
48.95/13.38	         top0(1) -> 8*
48.95/13.38	         top0(3) -> 8*
48.95/13.38	       problem:
48.95/13.38	        strict:
48.95/13.38	         f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.38	        weak:
48.95/13.38	         proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.38	         active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.38	         active(f(X,X)) -> mark(f(a(),b()))
48.95/13.38	         proper(a()) -> ok(a())
48.95/13.38	         proper(b()) -> ok(b())
48.95/13.38	         active(b()) -> mark(a())
48.95/13.38	         f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.38	         top(mark(X)) -> top(proper(X))
48.95/13.38	         top(ok(X)) -> top(active(X))
48.95/13.38	       Bounds Processor:
48.95/13.38	        bound: 1
48.95/13.38	        enrichment: match
48.95/13.38	        automaton:
48.95/13.38	         final states: {16,14,12,8,7,6,5}
48.95/13.38	         transitions:
48.95/13.38	          active0(2) -> 7*
48.95/13.38	          active0(14) -> 7*
48.95/13.38	          active0(4) -> 7*
48.95/13.38	          active0(16) -> 7*
48.95/13.38	          active0(1) -> 7*
48.95/13.38	          active0(3) -> 7*
48.95/13.38	          f0(2,14) -> 5*
48.95/13.38	          f0(2,16) -> 5*
48.95/13.38	          f0(3,1) -> 5*
48.95/13.38	          f0(3,3) -> 5*
48.95/13.38	          f0(14,2) -> 5*
48.95/13.38	          f0(14,4) -> 5*
48.95/13.38	          f0(4,2) -> 5*
48.95/13.38	          f0(4,4) -> 5*
48.95/13.38	          f0(14,14) -> 5*
48.95/13.38	          f0(4,14) -> 5*
48.95/13.38	          f0(14,16) -> 5*
48.95/13.38	          f0(4,16) -> 5*
48.95/13.38	          f0(16,2) -> 5*
48.95/13.38	          f0(16,4) -> 5*
48.95/13.38	          f0(1,2) -> 5*
48.95/13.38	          f0(1,4) -> 5*
48.95/13.38	          f0(16,14) -> 5*
48.95/13.38	          f0(16,16) -> 5*
48.95/13.38	          f0(1,14) -> 5*
48.95/13.38	          f0(1,16) -> 5*
48.95/13.38	          f0(2,1) -> 5*
48.95/13.38	          f0(2,3) -> 5*
48.95/13.38	          f0(3,2) -> 5*
48.95/13.38	          f0(3,4) -> 5*
48.95/13.38	          f0(3,14) -> 5*
48.95/13.38	          f0(3,16) -> 5*
48.95/13.38	          f0(14,1) -> 5*
48.95/13.38	          f0(14,3) -> 5*
48.95/13.38	          f0(4,1) -> 5*
48.95/13.38	          f0(4,3) -> 5*
48.95/13.38	          f0(16,1) -> 5*
48.95/13.38	          f0(16,3) -> 5*
48.95/13.38	          f0(1,1) -> 5*
48.95/13.38	          f0(1,3) -> 5*
48.95/13.38	          f0(2,2) -> 5*
48.95/13.38	          f0(2,4) -> 5*
48.95/13.38	          mark0(2) -> 16*,7,1
48.95/13.38	          mark0(14) -> 1*
48.95/13.38	          mark0(4) -> 1*
48.95/13.38	          mark0(16) -> 1*
48.95/13.38	          mark0(1) -> 1*
48.95/13.38	          mark0(3) -> 1*
48.95/13.38	          a0() -> 2*
48.95/13.38	          b0() -> 3*
48.95/13.38	          proper0(2) -> 6*
48.95/13.38	          proper0(14) -> 6*
48.95/13.38	          proper0(4) -> 6*
48.95/13.38	          proper0(16) -> 6*
48.95/13.38	          proper0(1) -> 6*
48.95/13.38	          proper0(3) -> 6*
48.95/13.38	          ok0(5) -> 5*
48.95/13.38	          ok0(12) -> 5*
48.95/13.38	          ok0(2) -> 14*,6,4
48.95/13.38	          ok0(14) -> 4*
48.95/13.38	          ok0(4) -> 4*
48.95/13.38	          ok0(16) -> 4*
48.95/13.38	          ok0(1) -> 4*
48.95/13.38	          ok0(3) -> 14*,6,4
48.95/13.38	          top0(7) -> 8*
48.95/13.38	          top0(2) -> 8*
48.95/13.38	          top0(14) -> 8*
48.95/13.38	          top0(4) -> 8*
48.95/13.38	          top0(16) -> 8*
48.95/13.38	          top0(6) -> 8*
48.95/13.38	          top0(1) -> 8*
48.95/13.38	          top0(3) -> 8*
48.95/13.38	          mark1(10) -> 5*
48.95/13.38	          mark1(5) -> 12*
48.95/13.38	          mark1(12) -> 12*,5
48.95/13.38	          f1(2,14) -> 5,12*
48.95/13.38	          f1(2,16) -> 5,12*
48.95/13.38	          f1(3,1) -> 12*,5,10
48.95/13.38	          f1(3,3) -> 12*,5,10
48.95/13.38	          f1(14,2) -> 5,12*
48.95/13.38	          f1(14,4) -> 5,12*
48.95/13.38	          f1(4,2) -> 12*,5,10
48.95/13.38	          f1(4,4) -> 12*,5,10
48.95/13.38	          f1(14,14) -> 5,12*
48.95/13.38	          f1(4,14) -> 5,12*
48.95/13.38	          f1(14,16) -> 5,12*
48.95/13.38	          f1(4,16) -> 5,12*
48.95/13.38	          f1(16,2) -> 5,12*
48.95/13.38	          f1(16,4) -> 5,12*
48.95/13.38	          f1(1,2) -> 12*,5,10
48.95/13.38	          f1(1,4) -> 12*,5,10
48.95/13.38	          f1(16,14) -> 5,12*
48.95/13.38	          f1(16,16) -> 5,12*
48.95/13.38	          f1(1,14) -> 5,12*
48.95/13.38	          f1(1,16) -> 5,12*
48.95/13.38	          f1(2,1) -> 12*,5,10
48.95/13.38	          f1(2,3) -> 12*,5,10
48.95/13.38	          f1(3,2) -> 12*,5,10
48.95/13.38	          f1(3,4) -> 12*,5,10
48.95/13.38	          f1(3,14) -> 5,12*
48.95/13.38	          f1(3,16) -> 5,12*
48.95/13.38	          f1(14,1) -> 5,12*
48.95/13.38	          f1(14,3) -> 5,12*
48.95/13.38	          f1(4,1) -> 12*,5,10
48.95/13.38	          f1(4,3) -> 12*,5,10
48.95/13.38	          f1(16,1) -> 5,12*
48.95/13.38	          f1(16,3) -> 5,12*
48.95/13.38	          f1(1,1) -> 12*,5,10
48.95/13.38	          f1(1,3) -> 12*,5,10
48.95/13.38	          f1(2,2) -> 12*,5,10
48.95/13.38	          f1(2,4) -> 12*,5,10
48.95/13.38	          ok1(5) -> 5,12*
48.95/13.38	          ok1(12) -> 5,12*
48.95/13.38	        problem:
48.95/13.38	         strict:
48.95/13.38	          
48.95/13.38	         weak:
48.95/13.38	          f(mark(X1),X2) -> mark(f(X1,X2))
48.95/13.38	          proper(f(X1,X2)) -> f(proper(X1),proper(X2))
48.95/13.38	          active(f(X1,X2)) -> f(active(X1),X2)
48.95/13.38	          active(f(X,X)) -> mark(f(a(),b()))
48.95/13.38	          proper(a()) -> ok(a())
48.95/13.38	          proper(b()) -> ok(b())
48.95/13.38	          active(b()) -> mark(a())
48.95/13.38	          f(ok(X1),ok(X2)) -> ok(f(X1,X2))
48.95/13.38	          top(mark(X)) -> top(proper(X))
48.95/13.38	          top(ok(X)) -> top(active(X))
48.95/13.38	        Qed
48.95/13.39	EOF