YES(O(1),O(1))
348.07/148.03	YES(O(1),O(1))
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Strict Trs:
348.07/148.03	  { f(s(a()), s(b()), x) -> f(x, x, x)
348.07/148.03	  , g(f(s(x), s(y), z)) -> g(f(x, y, z))
348.07/148.03	  , cons(x, y) -> x
348.07/148.03	  , cons(x, y) -> y }
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	We add the following dependency tuples:
348.07/148.03	
348.07/148.03	Strict DPs:
348.07/148.03	  { f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	  , g^#(f(s(x), s(y), z)) -> c_2(g^#(f(x, y, z)), f^#(x, y, z))
348.07/148.03	  , cons^#(x, y) -> c_3()
348.07/148.03	  , cons^#(x, y) -> c_4() }
348.07/148.03	
348.07/148.03	and mark the set of starting terms.
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Strict DPs:
348.07/148.03	  { f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	  , g^#(f(s(x), s(y), z)) -> c_2(g^#(f(x, y, z)), f^#(x, y, z))
348.07/148.03	  , cons^#(x, y) -> c_3()
348.07/148.03	  , cons^#(x, y) -> c_4() }
348.07/148.03	Weak Trs:
348.07/148.03	  { f(s(a()), s(b()), x) -> f(x, x, x)
348.07/148.03	  , g(f(s(x), s(y), z)) -> g(f(x, y, z))
348.07/148.03	  , cons(x, y) -> x
348.07/148.03	  , cons(x, y) -> y }
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	Consider the dependency graph:
348.07/148.03	
348.07/148.03	  1: f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	  
348.07/148.03	  2: g^#(f(s(x), s(y), z)) -> c_2(g^#(f(x, y, z)), f^#(x, y, z))
348.07/148.03	     -->_1 g^#(f(s(x), s(y), z)) ->
348.07/148.03	           c_2(g^#(f(x, y, z)), f^#(x, y, z)) :2
348.07/148.03	     -->_2 f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x)) :1
348.07/148.03	  
348.07/148.03	  3: cons^#(x, y) -> c_3()
348.07/148.03	  
348.07/148.03	  4: cons^#(x, y) -> c_4()
348.07/148.03	  
348.07/148.03	
348.07/148.03	Only the nodes {1,3,4} are reachable from nodes {1,3,4} that start
348.07/148.03	derivation from marked basic terms. The nodes not reachable are
348.07/148.03	removed from the problem.
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Strict DPs:
348.07/148.03	  { f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	  , cons^#(x, y) -> c_3()
348.07/148.03	  , cons^#(x, y) -> c_4() }
348.07/148.03	Weak Trs:
348.07/148.03	  { f(s(a()), s(b()), x) -> f(x, x, x)
348.07/148.03	  , g(f(s(x), s(y), z)) -> g(f(x, y, z))
348.07/148.03	  , cons(x, y) -> x
348.07/148.03	  , cons(x, y) -> y }
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	We estimate the number of application of {1,2,3} by applications of
348.07/148.03	Pre({1,2,3}) = {}. Here rules are labeled as follows:
348.07/148.03	
348.07/148.03	  DPs:
348.07/148.03	    { 1: f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	    , 2: cons^#(x, y) -> c_3()
348.07/148.03	    , 3: cons^#(x, y) -> c_4() }
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Weak DPs:
348.07/148.03	  { f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	  , cons^#(x, y) -> c_3()
348.07/148.03	  , cons^#(x, y) -> c_4() }
348.07/148.03	Weak Trs:
348.07/148.03	  { f(s(a()), s(b()), x) -> f(x, x, x)
348.07/148.03	  , g(f(s(x), s(y), z)) -> g(f(x, y, z))
348.07/148.03	  , cons(x, y) -> x
348.07/148.03	  , cons(x, y) -> y }
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	The following weak DPs constitute a sub-graph of the DG that is
348.07/148.03	closed under successors. The DPs are removed.
348.07/148.03	
348.07/148.03	{ f^#(s(a()), s(b()), x) -> c_1(f^#(x, x, x))
348.07/148.03	, cons^#(x, y) -> c_3()
348.07/148.03	, cons^#(x, y) -> c_4() }
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Weak Trs:
348.07/148.03	  { f(s(a()), s(b()), x) -> f(x, x, x)
348.07/148.03	  , g(f(s(x), s(y), z)) -> g(f(x, y, z))
348.07/148.03	  , cons(x, y) -> x
348.07/148.03	  , cons(x, y) -> y }
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	No rule is usable, rules are removed from the input problem.
348.07/148.03	
348.07/148.03	We are left with following problem, upon which TcT provides the
348.07/148.03	certificate YES(O(1),O(1)).
348.07/148.03	
348.07/148.03	Rules: Empty
348.07/148.03	Obligation:
348.07/148.03	  innermost runtime complexity
348.07/148.03	Answer:
348.07/148.03	  YES(O(1),O(1))
348.07/148.03	
348.07/148.03	Empty rules are trivially bounded
348.07/148.03	
348.07/148.03	Hurray, we answered YES(O(1),O(1))
348.52/148.41	EOF