* Step 1: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y))) b(y,z) -> z f(c(a(),z,x)) -> b(a(),z) - Signature: {b/2,f/1} / {a/0,c/3} - Obligation: runtime complexity wrt. defined symbols {b,f} and constructors {a,c} + Applied Processor: MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 1))), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 1))): Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] [1] p(b) = [2 1] x_1 + [1 1] x_2 + [0] [3 0] [2 2] [5] p(c) = [1 0] x_1 + [1 1] x_2 + [1 0] x_3 + [2] [0 0] [0 0] [0 0] [0] p(f) = [1 0] x_1 + [0] [2 0] [1] Following rules are strictly oriented: b(x,b(z,y)) = [2 1] x + [3 3] y + [ 5 1] z + [5] [3 0] [6 6] [10 2] [15] > [1 0] x + [1 0] y + [ 5 1] z + [3] [2 0] [2 0] [10 2] [7] = f(b(f(f(z)),c(x,z,y))) f(c(a(),z,x)) = [1 0] x + [1 1] z + [2] [2 0] [2 2] [5] > [1 1] z + [1] [2 2] [5] = b(a(),z) Following rules are (at-least) weakly oriented: b(y,z) = [2 1] y + [1 1] z + [0] [3 0] [2 2] [5] >= [1 0] z + [0] [0 1] [0] = z * Step 2: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: b(y,z) -> z - Weak TRS: b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y))) f(c(a(),z,x)) -> b(a(),z) - Signature: {b/2,f/1} / {a/0,c/3} - Obligation: runtime complexity wrt. defined symbols {b,f} and constructors {a,c} + Applied Processor: MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 1))), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 1))): Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] [1] p(b) = [2 1] x_1 + [1 1] x_2 + [1] [7 0] [2 1] [5] p(c) = [1 0] x_1 + [1 1] x_2 + [1 0] x_3 + [3] [0 0] [0 0] [0 0] [0] p(f) = [1 0] x_1 + [0] [2 0] [1] Following rules are strictly oriented: b(y,z) = [2 1] y + [1 1] z + [1] [7 0] [2 1] [5] > [1 0] z + [0] [0 1] [0] = z Following rules are (at-least) weakly oriented: b(x,b(z,y)) = [2 1] x + [3 2] y + [ 9 1] z + [7] [7 0] [4 3] [11 2] [12] >= [1 0] x + [1 0] y + [ 5 1] z + [5] [2 0] [2 0] [10 2] [11] = f(b(f(f(z)),c(x,z,y))) f(c(a(),z,x)) = [1 0] x + [1 1] z + [3] [2 0] [2 2] [7] >= [1 1] z + [2] [2 1] [5] = b(a(),z) * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y))) b(y,z) -> z f(c(a(),z,x)) -> b(a(),z) - Signature: {b/2,f/1} / {a/0,c/3} - Obligation: runtime complexity wrt. defined symbols {b,f} and constructors {a,c} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))