WORST_CASE(?,O(n^3)) * Step 1: NaturalPI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = 0 p(div) = 2 + x1 + x2 p(div_active) = 4 + x1 + 2*x2 p(false) = 0 p(ge) = x1 p(ge_active) = x1 p(if) = x1 + x2 + x3 p(if_active) = x1 + 2*x2 + 2*x3 p(mark) = 2*x1 p(minus) = 0 p(minus_active) = 0 p(s) = x1 p(true) = 0 Following rules are strictly oriented: div_active(x,y) = 4 + x + 2*y > 2 + x + y = div(x,y) div_active(0(),s(y)) = 4 + 2*y > 0 = 0() Following rules are (at-least) weakly oriented: div_active(s(x),s(y)) = 4 + x + 2*y >= 4 + x + 2*y = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = x >= x = ge(x,y) ge_active(x,0()) = x >= 0 = true() ge_active(0(),s(y)) = 0 >= 0 = false() ge_active(s(x),s(y)) = x >= x = ge_active(x,y) if_active(x,y,z) = x + 2*y + 2*z >= x + y + z = if(x,y,z) if_active(false(),x,y) = 2*x + 2*y >= 2*y = mark(y) if_active(true(),x,y) = 2*x + 2*y >= 2*x = mark(x) mark(0()) = 0 >= 0 = 0() mark(div(x,y)) = 4 + 2*x + 2*y >= 4 + 2*x + 2*y = div_active(mark(x),y) mark(ge(x,y)) = 2*x >= x = ge_active(x,y) mark(if(x,y,z)) = 2*x + 2*y + 2*z >= 2*x + 2*y + 2*z = if_active(mark(x),y,z) mark(minus(x,y)) = 0 >= 0 = minus_active(x,y) mark(s(x)) = 2*x >= 2*x = s(mark(x)) minus_active(x,y) = 0 >= 0 = minus(x,y) minus_active(0(),y) = 0 >= 0 = 0() minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y) * Step 2: NaturalPI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = 0 p(div) = x1 p(div_active) = x1 p(false) = 0 p(ge) = 0 p(ge_active) = 0 p(if) = x1 + x2 + x3 p(if_active) = x1 + x2 + x3 p(mark) = x1 p(minus) = x1 p(minus_active) = x1 p(s) = 4 + x1 p(true) = 0 Following rules are strictly oriented: minus_active(s(x),s(y)) = 4 + x > x = minus_active(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = x >= x = div(x,y) div_active(0(),s(y)) = 0 >= 0 = 0() div_active(s(x),s(y)) = 4 + x >= 4 + x = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = 0 >= 0 = ge(x,y) ge_active(x,0()) = 0 >= 0 = true() ge_active(0(),s(y)) = 0 >= 0 = false() ge_active(s(x),s(y)) = 0 >= 0 = ge_active(x,y) if_active(x,y,z) = x + y + z >= x + y + z = if(x,y,z) if_active(false(),x,y) = x + y >= y = mark(y) if_active(true(),x,y) = x + y >= x = mark(x) mark(0()) = 0 >= 0 = 0() mark(div(x,y)) = x >= x = div_active(mark(x),y) mark(ge(x,y)) = 0 >= 0 = ge_active(x,y) mark(if(x,y,z)) = x + y + z >= x + y + z = if_active(mark(x),y,z) mark(minus(x,y)) = x >= x = minus_active(x,y) mark(s(x)) = 4 + x >= 4 + x = s(mark(x)) minus_active(x,y) = x >= x = minus(x,y) minus_active(0(),y) = 0 >= 0 = 0() * Step 3: NaturalPI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = 0 p(div) = x1 + x2 p(div_active) = x1 + x2 p(false) = 0 p(ge) = x1 p(ge_active) = x1 p(if) = x1 + x2 + x3 p(if_active) = x1 + x2 + x3 p(mark) = x1 p(minus) = 0 p(minus_active) = 0 p(s) = 4 + x1 p(true) = 0 Following rules are strictly oriented: ge_active(s(x),s(y)) = 4 + x > x = ge_active(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = x + y >= x + y = div(x,y) div_active(0(),s(y)) = 4 + y >= 0 = 0() div_active(s(x),s(y)) = 8 + x + y >= 8 + x + y = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = x >= x = ge(x,y) ge_active(x,0()) = x >= 0 = true() ge_active(0(),s(y)) = 0 >= 0 = false() if_active(x,y,z) = x + y + z >= x + y + z = if(x,y,z) if_active(false(),x,y) = x + y >= y = mark(y) if_active(true(),x,y) = x + y >= x = mark(x) mark(0()) = 0 >= 0 = 0() mark(div(x,y)) = x + y >= x + y = div_active(mark(x),y) mark(ge(x,y)) = x >= x = ge_active(x,y) mark(if(x,y,z)) = x + y + z >= x + y + z = if_active(mark(x),y,z) mark(minus(x,y)) = 0 >= 0 = minus_active(x,y) mark(s(x)) = 4 + x >= 4 + x = s(mark(x)) minus_active(x,y) = 0 >= 0 = minus(x,y) minus_active(0(),y) = 0 >= 0 = 0() minus_active(s(x),s(y)) = 0 >= 0 = minus_active(x,y) * Step 4: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() ge_active(s(x),s(y)) -> ge_active(x,y) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 0] [1] p(div_active) = [1 0 0] [0] [0 1 1] x1 + [0] [0 0 0] [1] p(false) = [0] [0] [0] p(ge) = [0] [0] [0] p(ge_active) = [0] [0] [0] p(if) = [0 0 0] [0 0 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [1] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [1] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0 1 0] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] > [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 0] [0] [0 1 1] x + [0] [0 0 0] [1] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 0] [1] = div(x,y) div_active(0(),s(y)) = [0] [0] [1] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [0] [0 1 0] x + [1] [0 0 0] [1] >= [0] [1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [0] [0] >= [0] [0] [0] = ge(x,y) ge_active(x,0()) = [0] [0] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0] [0 1 1] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 1] x + [0] [0 0 0] [1] = div_active(mark(x),y) mark(ge(x,y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 5: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() ge_active(s(x),s(y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0 0 0] [0] [0 1 1] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 1] [1] p(div_active) = [1 0 0] [0 0 0] [0] [0 1 1] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 1] [1] p(false) = [0] [1] [0] p(ge) = [0] [1] [1] p(ge_active) = [0] [1] [1] p(if) = [0 0 0] [0 1 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 1] [0 0 1] [0 0 1] [1] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 1] [0 0 1] [0 0 1] [1] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [1] Following rules are strictly oriented: mark(ge(x,y)) = [1] [1] [1] > [0] [1] [1] = ge_active(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 0] [0 0 0] [0] [0 1 1] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [1] >= [0 0 0] [0 0 0] [0] [0 1 1] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [1] = div(x,y) div_active(0(),s(y)) = [0] [0] [2] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [0] [0 1 0] x + [1] [0 0 0] [3] >= [0] [1] [3] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [1] [1] >= [0] [1] [1] = ge(x,y) ge_active(x,0()) = [0] [1] [1] >= [0] [0] [1] = true() ge_active(0(),s(y)) = [0] [1] [1] >= [0] [1] [0] = false() ge_active(s(x),s(y)) = [0] [1] [1] >= [0] [1] [1] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 1] [0 0 1] [0 0 1] [1] >= [0 0 0] [0 1 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 1] [0 0 1] [0 0 1] [1] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [1] [0 0 1] [0 0 1] [1] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [2] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0 0 0] [0] [0 1 1] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [1] >= [0 1 0] [0 0 0] [0] [0 1 1] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [1] = div_active(mark(x),y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 1] [0 0 1] [0 0 1] [1] >= [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 1] [0 0 1] [0 0 1] [1] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 6: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() ge_active(s(x),s(y)) -> ge_active(x,y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [1 0 1] [0 1 1] [0] [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 0] [0] p(div_active) = [1 0 1] [0 1 1] [0] [0 1 0] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 0] [0] p(false) = [1] [0] [0] p(ge) = [1] [0] [0] p(ge_active) = [1] [0] [0] p(if) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 1] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [1 0 0] [1 0 0] [0] [0 1 0] x1 + [0 0 1] x2 + [0 0 1] x3 + [0] [0 0 1] [0 0 1] [0 0 1] [0] p(mark) = [1 0 0] [0] [0 0 1] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: ge_active(x,0()) = [1] [0] [0] > [0] [0] [0] = true() if_active(false(),x,y) = [1 0 0] [1 0 0] [1] [0 0 1] x + [0 0 1] y + [0] [0 0 1] [0 0 1] [0] > [1 0 0] [0] [0 0 1] y + [0] [0 0 1] [0] = mark(y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0 1 1] [0] [0 1 0] x + [0 0 0] y + [0] [0 0 1] [0 0 0] [0] >= [1 0 1] [0 1 1] [0] [0 0 0] x + [0 0 0] y + [0] [0 0 1] [0 0 0] [0] = div(x,y) div_active(0(),s(y)) = [2] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [3] [0 0 0] x + [1] [0 0 0] [1] >= [3] [1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [1] [0] [0] >= [1] [0] [0] = ge(x,y) ge_active(0(),s(y)) = [1] [0] [0] >= [1] [0] [0] = false() ge_active(s(x),s(y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [1 0 0] [1 0 0] [0] [0 1 0] x + [0 0 1] y + [0 0 1] z + [0] [0 0 1] [0 0 1] [0 0 1] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 0 0] y + [0 0 0] z + [0] [0 0 1] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(true(),x,y) = [1 0 0] [1 0 0] [0] [0 0 1] x + [0 0 1] y + [0] [0 0 1] [0 0 1] [0] >= [1 0 0] [0] [0 0 1] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [1 0 1] [0 1 1] [0] [0 0 1] x + [0 0 0] y + [0] [0 0 1] [0 0 0] [0] >= [1 0 1] [0 1 1] [0] [0 0 1] x + [0 0 0] y + [0] [0 0 1] [0 0 0] [0] = div_active(mark(x),y) mark(ge(x,y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 1] x + [0 0 1] y + [0 0 1] z + [0] [0 0 1] [0 0 1] [0 0 1] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 1] x + [0 0 1] y + [0 0 1] z + [0] [0 0 1] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [1 0 0] [0] [0 0 0] x + [1] [0 0 0] [1] >= [1 0 0] [0] [0 0 0] x + [1] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 7: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(false) = [0] [0] [0] p(ge) = [0] [0] [0] p(ge_active) = [0] [0] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [1] [0 0 0] [1] > [0] [0] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() ge_active(x,y) = [0] [0] [0] >= [0] [0] [0] = ge(x,y) ge_active(x,0()) = [0] [0] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 8: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 0] [1] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 0] [1] p(false) = [0] [0] [0] p(ge) = [0] [0] [0] p(ge_active) = [0] [0] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [1] [0] p(minus_active) = [0] [1] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: mark(minus(x,y)) = [1] [1] [0] > [0] [1] [0] = minus_active(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 0] [1] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 0] [1] = div(x,y) div_active(0(),s(y)) = [0] [0] [1] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [1] [0 0 0] [1] >= [1] [1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [0] [0] >= [0] [0] [0] = ge(x,y) ge_active(x,0()) = [0] [0] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0] [0 1 1] x + [0] [0 0 0] [1] >= [0 1 1] [0] [0 1 1] x + [0] [0 0 0] [1] = div_active(mark(x),y) mark(ge(x,y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [1] [0] >= [0] [1] [0] = minus(x,y) minus_active(0(),y) = [0] [1] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [1] [0] >= [0] [1] [0] = minus_active(x,y) * Step 9: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(false) = [1] [0] [0] p(ge) = [1] [0] [0] p(ge_active) = [1] [0] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [1] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [1] [0] [0] p(minus_active) = [1] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [1] [0] [0] Following rules are strictly oriented: mark(0()) = [1] [0] [0] > [0] [0] [0] = 0() minus_active(0(),y) = [1] [0] [0] > [0] [0] [0] = 0() Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [1] [0 0 0] [1] >= [1] [0] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [1] [0] [0] >= [1] [0] [0] = ge(x,y) ge_active(x,0()) = [1] [0] [0] >= [1] [0] [0] = true() ge_active(0(),s(y)) = [1] [0] [0] >= [1] [0] [0] = false() ge_active(s(x),s(y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [1] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [1] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(div(x,y)) = [0 1 1] [1] [0 1 1] x + [0] [0 0 1] [0] >= [0 1 1] [1] [0 1 1] x + [0] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [1] [0] [0] >= [1] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [1] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [1] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [1] [0] [0] >= [1] [0] [0] = minus(x,y) minus_active(s(x),s(y)) = [1] [0] [0] >= [1] [0] [0] = minus_active(x,y) * Step 10: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(true(),x,y) -> mark(x) mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [1] [0 0 1] [0] p(div_active) = [1 0 1] [1] [0 1 1] x1 + [1] [0 0 1] [0] p(false) = [0] [0] [0] p(ge) = [0] [0] [0] p(ge_active) = [0] [0] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0 0 0] [0] [0 0 1] x1 + [1] [0 0 0] [0] p(minus_active) = [0 0 0] [1] [0 0 1] x1 + [1] [0 0 0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 1] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: minus_active(x,y) = [0 0 0] [1] [0 0 1] x + [1] [0 0 0] [0] > [0 0 0] [0] [0 0 1] x + [1] [0 0 0] [0] = minus(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [1] [0 1 1] x + [1] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [1] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [1] [1] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 1] [2] [0 1 1] x + [2] [0 0 1] [1] >= [0 0 1] [2] [0 0 1] x + [2] [0 0 0] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [0] [0] >= [0] [0] [0] = ge(x,y) ge_active(x,0()) = [0] [0] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [1] [0 1 1] x + [1] [0 0 1] [0] >= [0 1 1] [1] [0 1 1] x + [1] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0 0 1] [1] [0 0 1] x + [1] [0 0 0] [0] >= [0 0 0] [1] [0 0 1] x + [1] [0 0 0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [1] = s(mark(x)) minus_active(0(),y) = [1] [1] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0 0 0] [1] [0 0 1] x + [2] [0 0 0] [0] >= [0 0 0] [1] [0 0 1] x + [1] [0 0 0] [0] = minus_active(x,y) * Step 11: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) if_active(true(),x,y) -> mark(x) mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [1 1 1] [0] [0 0 0] x1 + [0] [0 0 0] [1] p(div_active) = [1 1 1] [0] [0 0 0] x1 + [0] [0 0 0] [1] p(false) = [1] [0] [0] p(ge) = [1] [0] [0] p(ge_active) = [1] [0] [0] p(if) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [1] [0 0 0] x1 + [0] [0 0 0] [1] p(true) = [1] [0] [0] Following rules are strictly oriented: if_active(true(),x,y) = [1 0 0] [1 0 0] [1] [0 0 0] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [0] > [1 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] = mark(x) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 1 1] [0] [0 0 0] x + [0] [0 0 0] [1] >= [1 1 1] [0] [0 0 0] x + [0] [0 0 0] [1] = div(x,y) div_active(0(),s(y)) = [0] [0] [1] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [2] [0 0 0] x + [0] [0 0 0] [1] >= [2] [0] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [1] [0] [0] >= [1] [0] [0] = ge(x,y) ge_active(x,0()) = [1] [0] [0] >= [1] [0] [0] = true() ge_active(0(),s(y)) = [1] [0] [0] >= [1] [0] [0] = false() ge_active(s(x),s(y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 0 0] y + [0 0 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 0 0] y + [0 0 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [1 0 0] [1 0 0] [1] [0 0 0] x + [0 0 0] y + [0] [0 0 1] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] y + [0] [0 0 1] [0] = mark(y) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [1 1 1] [0] [0 0 0] x + [0] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] x + [0] [0 0 0] [1] = div_active(mark(x),y) mark(ge(x,y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 0 0] y + [0 0 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 0 0] y + [0 0 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [1 0 0] [1] [0 0 0] x + [0] [0 0 0] [1] >= [1 0 0] [1] [0 0 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 12: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) ge_active(0(),s(y)) -> false() if_active(x,y,z) -> if(x,y,z) mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [1 1 0] [0] [0 1 0] x1 + [0] [0 0 0] [0] p(div_active) = [1 1 0] [0] [0 1 0] x1 + [0] [0 0 0] [0] p(false) = [0] [0] [0] p(ge) = [1] [0] [0] p(ge_active) = [1] [0] [0] p(if) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 0] [0 0 0] [0] p(if_active) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 0] [0 0 0] [0] p(mark) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [0] p(true) = [1] [0] [0] Following rules are strictly oriented: ge_active(0(),s(y)) = [1] [0] [0] > [0] [0] [0] = false() Following rules are (at-least) weakly oriented: div_active(x,y) = [1 1 0] [0] [0 1 0] x + [0] [0 0 0] [0] >= [1 1 0] [0] [0 1 0] x + [0] [0 0 0] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 0 0] x + [1] [0 0 0] [0] >= [1] [1] [0] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [1] [0] [0] >= [1] [0] [0] = ge(x,y) ge_active(x,0()) = [1] [0] [0] >= [1] [0] [0] = true() ge_active(s(x),s(y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 0] [0 0 0] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 0] [0 0 0] [0] = if(x,y,z) if_active(false(),x,y) = [1 0 0] [1 0 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 0] [0 0 0] [0] >= [1 0 0] [0] [0 1 0] y + [0] [0 0 0] [0] = mark(y) if_active(true(),x,y) = [1 0 0] [1 0 0] [1] [0 1 0] x + [0 1 0] y + [0] [0 0 0] [0 0 0] [0] >= [1 0 0] [0] [0 1 0] x + [0] [0 0 0] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [1 1 0] [0] [0 1 0] x + [0] [0 0 0] [0] >= [1 1 0] [0] [0 1 0] x + [0] [0 0 0] [0] = div_active(mark(x),y) mark(ge(x,y)) = [1] [0] [0] >= [1] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 0] [0 0 0] [0] >= [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 0] [0 0 0] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [1 0 0] [0] [0 0 0] x + [1] [0 0 0] [0] >= [1 0 0] [0] [0 0 0] x + [1] [0 0 0] [0] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 13: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ge_active(x,y) -> ge(x,y) if_active(x,y,z) -> if(x,y,z) mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(false) = [0] [1] [0] p(ge) = [0] [1] [0] p(ge_active) = [1] [1] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 1] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 1] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [1] [1] [0] Following rules are strictly oriented: ge_active(x,y) = [1] [1] [0] > [0] [1] [0] = ge(x,y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [1] [0 0 0] [1] >= [1] [1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,0()) = [1] [1] [0] >= [1] [1] [0] = true() ge_active(0(),s(y)) = [1] [1] [0] >= [0] [1] [0] = false() ge_active(s(x),s(y)) = [1] [1] [0] >= [1] [1] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [1] [1] [0] >= [1] [1] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 1] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 14: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: if_active(x,y,z) -> if(x,y,z) mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(false) = [0] [0] [0] p(ge) = [0] [0] [0] p(ge_active) = [0] [0] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 1] x3 + [1] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 0] [0 1 0] [1] [0 1 0] x1 + [0 1 0] x2 + [0 1 1] x3 + [1] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: if_active(x,y,z) = [1 0 0] [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] > [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [1] [0 0 0] [1] >= [1] [1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [0] [0] >= [0] [0] [0] = ge(x,y) ge_active(x,0()) = [0] [0] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) if_active(false(),x,y) = [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 1] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 1] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 1 1] [0] [0 1 1] x + [0] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [0] [0] [0] >= [0] [0] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 0] [0 1 0] [0 1 1] [1] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0 1 0] [0 1 0] [1] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 15: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: mark(div(x,y)) -> div_active(mark(x),y) mark(s(x)) -> s(mark(x)) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [0] [0 0 1] [0] p(false) = [0] [0] [0] p(ge) = [0 0 0] [0] [0 0 0] x1 + [0] [0 0 1] [0] p(ge_active) = [0 0 0] [0] [0 0 0] x1 + [0] [0 0 1] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 1] x3 + [1] [0 0 1] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 0] [0 1 1] [0 1 1] [0] [0 1 0] x1 + [0 1 0] x2 + [0 1 1] x3 + [1] [0 0 1] [0 0 1] [0 0 1] [0] p(mark) = [0 1 1] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 1] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: mark(s(x)) = [0 1 1] [1] [0 1 0] x + [0] [0 0 1] [1] > [0 1 1] [0] [0 1 0] x + [0] [0 0 1] [1] = s(mark(x)) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [0] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 1] [1] [0 1 1] x + [1] [0 0 1] [1] >= [0 0 0] [1] [0 0 0] x + [1] [0 0 1] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] = ge(x,y) ge_active(x,0()) = [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [0] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 0] [0 1 1] [0 1 1] [0] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 1] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 1] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 1] [0 1 1] [0] [0 1 0] x + [0 1 1] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 1] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 1] [0 1 1] [0] [0 1 0] x + [0 1 1] y + [1] [0 0 1] [0 0 1] [0] >= [0 1 1] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(div(x,y)) = [0 1 2] [0] [0 1 1] x + [0] [0 0 1] [0] >= [0 1 2] [0] [0 1 1] x + [0] [0 0 1] [0] = div_active(mark(x),y) mark(ge(x,y)) = [0 0 1] [0] [0 0 0] x + [0] [0 0 1] [0] >= [0 0 0] [0] [0 0 0] x + [0] [0 0 1] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 1] [0 1 1] [0 1 2] [1] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 1] [0 0 1] [0 0 1] [0] >= [0 1 1] [0 1 1] [0 1 1] [0] [0 1 0] x + [0 1 0] y + [0 1 1] z + [1] [0 0 1] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 16: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: mark(div(x,y)) -> div_active(mark(x),y) - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(div_active) = {1}, uargs(if_active) = {1}, uargs(s) = {1} Following symbols are considered usable: {div_active,ge_active,if_active,mark,minus_active} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(div) = [0 0 0] [0] [0 1 1] x1 + [1] [0 0 1] [0] p(div_active) = [1 0 1] [0] [0 1 1] x1 + [1] [0 0 1] [0] p(false) = [0] [0] [0] p(ge) = [0] [1] [0] p(ge_active) = [0] [1] [0] p(if) = [0 0 0] [0 0 0] [0 0 0] [0] [0 1 1] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(if_active) = [1 0 1] [0 1 0] [0 1 0] [0] [0 1 1] x1 + [0 1 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0 0 1] [0] p(mark) = [0 1 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(minus) = [0] [0] [0] p(minus_active) = [0] [0] [0] p(s) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(true) = [0] [0] [0] Following rules are strictly oriented: mark(div(x,y)) = [0 1 1] [1] [0 1 1] x + [1] [0 0 1] [0] > [0 1 1] [0] [0 1 1] x + [1] [0 0 1] [0] = div_active(mark(x),y) Following rules are (at-least) weakly oriented: div_active(x,y) = [1 0 1] [0] [0 1 1] x + [1] [0 0 1] [0] >= [0 0 0] [0] [0 1 1] x + [1] [0 0 1] [0] = div(x,y) div_active(0(),s(y)) = [0] [1] [0] >= [0] [0] [0] = 0() div_active(s(x),s(y)) = [1 0 0] [1] [0 1 0] x + [2] [0 0 0] [1] >= [1] [2] [1] = if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) = [0] [1] [0] >= [0] [1] [0] = ge(x,y) ge_active(x,0()) = [0] [1] [0] >= [0] [0] [0] = true() ge_active(0(),s(y)) = [0] [1] [0] >= [0] [0] [0] = false() ge_active(s(x),s(y)) = [0] [1] [0] >= [0] [1] [0] = ge_active(x,y) if_active(x,y,z) = [1 0 1] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 0] [0 0 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if(x,y,z) if_active(false(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] y + [0] [0 0 1] [0] = mark(y) if_active(true(),x,y) = [0 1 0] [0 1 0] [0] [0 1 0] x + [0 1 0] y + [0] [0 0 1] [0 0 1] [0] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 1] [0] = mark(x) mark(0()) = [0] [0] [0] >= [0] [0] [0] = 0() mark(ge(x,y)) = [1] [1] [0] >= [0] [1] [0] = ge_active(x,y) mark(if(x,y,z)) = [0 1 1] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] >= [0 1 1] [0 1 0] [0 1 0] [0] [0 1 1] x + [0 1 0] y + [0 1 0] z + [0] [0 0 0] [0 0 1] [0 0 1] [0] = if_active(mark(x),y,z) mark(minus(x,y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) mark(s(x)) = [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] x + [0] [0 0 0] [1] = s(mark(x)) minus_active(x,y) = [0] [0] [0] >= [0] [0] [0] = minus(x,y) minus_active(0(),y) = [0] [0] [0] >= [0] [0] [0] = 0() minus_active(s(x),s(y)) = [0] [0] [0] >= [0] [0] [0] = minus_active(x,y) * Step 17: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: div_active(x,y) -> div(x,y) div_active(0(),s(y)) -> 0() div_active(s(x),s(y)) -> if_active(ge_active(x,y),s(div(minus(x,y),s(y))),0()) ge_active(x,y) -> ge(x,y) ge_active(x,0()) -> true() ge_active(0(),s(y)) -> false() ge_active(s(x),s(y)) -> ge_active(x,y) if_active(x,y,z) -> if(x,y,z) if_active(false(),x,y) -> mark(y) if_active(true(),x,y) -> mark(x) mark(0()) -> 0() mark(div(x,y)) -> div_active(mark(x),y) mark(ge(x,y)) -> ge_active(x,y) mark(if(x,y,z)) -> if_active(mark(x),y,z) mark(minus(x,y)) -> minus_active(x,y) mark(s(x)) -> s(mark(x)) minus_active(x,y) -> minus(x,y) minus_active(0(),y) -> 0() minus_active(s(x),s(y)) -> minus_active(x,y) - Signature: {div_active/2,ge_active/2,if_active/3,mark/1,minus_active/2} / {0/0,div/2,false/0,ge/2,if/3,minus/2,s/1 ,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {div_active,ge_active,if_active,mark ,minus_active} and constructors {0,div,false,ge,if,minus,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))