/bin/sh: line 1: 2727 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP2596-28 > /tmp/SMTS2596-29 /bin/sh: line 1: 2734 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP2596-44 > /tmp/SMTS2596-45 /bin/sh: line 1: 2747 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP2596-70 > /tmp/SMTS2596-71 WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2} / {0/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0} and constructors {0,S} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2} / {0/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0} and constructors {0,S} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2} / {0/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0} and constructors {0,S} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: eq0(x,y){x -> S(x),y -> S(y)} = eq0(S(x),S(y)) ->^+ eq0(x,y) = C[eq0(x,y) = eq0(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2} / {0/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0} and constructors {0,S} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs eq0#(0(),0()) -> c_1() eq0#(0(),S(x)) -> c_2() eq0#(S(x),0()) -> c_3() eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq0#(0(),0()) -> c_1() eq0#(0(),S(x)) -> c_2() eq0#(S(x),0()) -> c_3() eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) - Weak TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2,eq0#/2} / {0/0,S/1,c_1/0,c_2/0,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0#} and constructors {0,S} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3} by application of Pre({1,2,3}) = {4}. Here rules are labelled as follows: 1: eq0#(0(),0()) -> c_1() 2: eq0#(0(),S(x)) -> c_2() 3: eq0#(S(x),0()) -> c_3() 4: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) - Weak DPs: eq0#(0(),0()) -> c_1() eq0#(0(),S(x)) -> c_2() eq0#(S(x),0()) -> c_3() - Weak TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2,eq0#/2} / {0/0,S/1,c_1/0,c_2/0,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0#} and constructors {0,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) -->_1 eq0#(S(x),0()) -> c_3():4 -->_1 eq0#(0(),S(x)) -> c_2():3 -->_1 eq0#(0(),0()) -> c_1():2 -->_1 eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)):1 2:W:eq0#(0(),0()) -> c_1() 3:W:eq0#(0(),S(x)) -> c_2() 4:W:eq0#(S(x),0()) -> c_3() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: eq0#(0(),0()) -> c_1() 3: eq0#(0(),S(x)) -> c_2() 4: eq0#(S(x),0()) -> c_3() ** Step 1.b:4: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) - Weak TRS: eq0(0(),0()) -> S(0()) eq0(0(),S(x)) -> 0() eq0(S(x),0()) -> 0() eq0(S(x'),S(x)) -> eq0(x',x) - Signature: {eq0/2,eq0#/2} / {0/0,S/1,c_1/0,c_2/0,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0#} and constructors {0,S} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) ** Step 1.b:5: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) - Signature: {eq0/2,eq0#/2} / {0/0,S/1,c_1/0,c_2/0,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0#} and constructors {0,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1} Following symbols are considered usable: {eq0#} TcT has computed the following interpretation: p(0) = [0] p(S) = [1] x1 + [8] p(eq0) = [4] x1 + [1] p(eq0#) = [2] x1 + [4] p(c_1) = [2] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] x1 + [8] Following rules are strictly oriented: eq0#(S(x'),S(x)) = [2] x' + [20] > [2] x' + [12] = c_4(eq0#(x',x)) Following rules are (at-least) weakly oriented: ** Step 1.b:6: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq0#(S(x'),S(x)) -> c_4(eq0#(x',x)) - Signature: {eq0/2,eq0#/2} / {0/0,S/1,c_1/0,c_2/0,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {eq0#} and constructors {0,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))