YES(O(1),O(n^1))
19.15/10.76	YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	We add the following dependency tuples:
19.15/10.76	
19.15/10.76	Strict DPs:
19.15/10.76	  { a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	  , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	  , a__c^#() -> c_3()
19.15/10.76	  , a__c^#() -> c_4()
19.15/10.76	  , mark^#(b()) -> c_5()
19.15/10.76	  , mark^#(c()) -> c_6(a__c^#())
19.15/10.76	  , mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	
19.15/10.76	and mark the set of starting terms.
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs:
19.15/10.76	  { a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	  , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	  , a__c^#() -> c_3()
19.15/10.76	  , a__c^#() -> c_4()
19.15/10.76	  , mark^#(b()) -> c_5()
19.15/10.76	  , mark^#(c()) -> c_6(a__c^#())
19.15/10.76	  , mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	Weak Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	We estimate the number of application of {1,3,4,5} by applications
19.15/10.76	of Pre({1,3,4,5}) = {2,6,7}. Here rules are labeled as follows:
19.15/10.76	
19.15/10.76	  DPs:
19.15/10.76	    { 1: a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	    , 2: a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	    , 3: a__c^#() -> c_3()
19.15/10.76	    , 4: a__c^#() -> c_4()
19.15/10.76	    , 5: mark^#(b()) -> c_5()
19.15/10.76	    , 6: mark^#(c()) -> c_6(a__c^#())
19.15/10.76	    , 7: mark^#(f(X1, X2, X3)) ->
19.15/10.76	         c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs:
19.15/10.76	  { a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	  , mark^#(c()) -> c_6(a__c^#())
19.15/10.76	  , mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	Weak DPs:
19.15/10.76	  { a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	  , a__c^#() -> c_3()
19.15/10.76	  , a__c^#() -> c_4()
19.15/10.76	  , mark^#(b()) -> c_5() }
19.15/10.76	Weak Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	We estimate the number of application of {1,2} by applications of
19.15/10.76	Pre({1,2}) = {3}. Here rules are labeled as follows:
19.15/10.76	
19.15/10.76	  DPs:
19.15/10.76	    { 1: a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	    , 2: mark^#(c()) -> c_6(a__c^#())
19.15/10.76	    , 3: mark^#(f(X1, X2, X3)) ->
19.15/10.76	         c_7(a__f^#(X1, mark(X2), X3), mark^#(X2))
19.15/10.76	    , 4: a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	    , 5: a__c^#() -> c_3()
19.15/10.76	    , 6: a__c^#() -> c_4()
19.15/10.76	    , 7: mark^#(b()) -> c_5() }
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs:
19.15/10.76	  { mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	Weak DPs:
19.15/10.76	  { a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	  , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	  , a__c^#() -> c_3()
19.15/10.76	  , a__c^#() -> c_4()
19.15/10.76	  , mark^#(b()) -> c_5()
19.15/10.76	  , mark^#(c()) -> c_6(a__c^#()) }
19.15/10.76	Weak Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	The following weak DPs constitute a sub-graph of the DG that is
19.15/10.76	closed under successors. The DPs are removed.
19.15/10.76	
19.15/10.76	{ a__f^#(X1, X2, X3) -> c_1()
19.15/10.76	, a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X), a__c^#())
19.15/10.76	, a__c^#() -> c_3()
19.15/10.76	, a__c^#() -> c_4()
19.15/10.76	, mark^#(b()) -> c_5()
19.15/10.76	, mark^#(c()) -> c_6(a__c^#()) }
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs:
19.15/10.76	  { mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	Weak Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	Due to missing edges in the dependency-graph, the right-hand sides
19.15/10.76	of following rules could be simplified:
19.15/10.76	
19.15/10.76	  { mark^#(f(X1, X2, X3)) ->
19.15/10.76	    c_7(a__f^#(X1, mark(X2), X3), mark^#(X2)) }
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs: { mark^#(f(X1, X2, X3)) -> c_1(mark^#(X2)) }
19.15/10.76	Weak Trs:
19.15/10.76	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
19.15/10.76	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
19.15/10.76	  , a__c() -> b()
19.15/10.76	  , a__c() -> c()
19.15/10.76	  , mark(b()) -> b()
19.15/10.76	  , mark(c()) -> a__c()
19.15/10.76	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	No rule is usable, rules are removed from the input problem.
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(n^1)).
19.15/10.76	
19.15/10.76	Strict DPs: { mark^#(f(X1, X2, X3)) -> c_1(mark^#(X2)) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(n^1))
19.15/10.76	
19.15/10.76	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
19.15/10.76	to orient following rules strictly.
19.15/10.76	
19.15/10.76	DPs:
19.15/10.76	  { 1: mark^#(f(X1, X2, X3)) -> c_1(mark^#(X2)) }
19.15/10.76	
19.15/10.76	Sub-proof:
19.15/10.76	----------
19.15/10.76	  The input was oriented with the instance of 'Small Polynomial Path
19.15/10.76	  Order (PS,1-bounded)' as induced by the safe mapping
19.15/10.76	  
19.15/10.76	   safe(f) = {1, 2, 3}, safe(mark^#) = {}, safe(c_1) = {}
19.15/10.76	  
19.15/10.76	  and precedence
19.15/10.76	  
19.15/10.76	   empty .
19.15/10.76	  
19.15/10.76	  Following symbols are considered recursive:
19.15/10.76	  
19.15/10.76	   {mark^#}
19.15/10.76	  
19.15/10.76	  The recursion depth is 1.
19.15/10.76	  
19.15/10.76	  Further, following argument filtering is employed:
19.15/10.76	  
19.15/10.76	   pi(f) = [1, 2, 3], pi(mark^#) = [1], pi(c_1) = [1]
19.15/10.76	  
19.15/10.76	  Usable defined function symbols are a subset of:
19.15/10.76	  
19.15/10.76	   {mark^#}
19.15/10.76	  
19.15/10.76	  For your convenience, here are the satisfied ordering constraints:
19.15/10.76	  
19.15/10.76	    pi(mark^#(f(X1, X2, X3))) = mark^#(f(; X1,  X2,  X3);)
19.15/10.76	                              > c_1(mark^#(X2;);)         
19.15/10.76	                              = pi(c_1(mark^#(X2)))       
19.15/10.76	                                                          
19.15/10.76	
19.15/10.76	The strictly oriented rules are moved into the weak component.
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(1)).
19.15/10.76	
19.15/10.76	Weak DPs: { mark^#(f(X1, X2, X3)) -> c_1(mark^#(X2)) }
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(1))
19.15/10.76	
19.15/10.76	The following weak DPs constitute a sub-graph of the DG that is
19.15/10.76	closed under successors. The DPs are removed.
19.15/10.76	
19.15/10.76	{ mark^#(f(X1, X2, X3)) -> c_1(mark^#(X2)) }
19.15/10.76	
19.15/10.76	We are left with following problem, upon which TcT provides the
19.15/10.76	certificate YES(O(1),O(1)).
19.15/10.76	
19.15/10.76	Rules: Empty
19.15/10.76	Obligation:
19.15/10.76	  innermost runtime complexity
19.15/10.76	Answer:
19.15/10.76	  YES(O(1),O(1))
19.15/10.76	
19.15/10.76	Empty rules are trivially bounded
19.15/10.76	
19.15/10.76	Hurray, we answered YES(O(1),O(n^1))
19.15/10.76	EOF