WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: admit(x,u){u -> .(y,.(z,.(w(),u)))} = admit(x,.(y,.(z,.(w(),u)))) ->^+ cond(=(sum(x,y,z),w()),.(y,.(z,.(w(),admit(carry(x,y,z),u))))) = C[admit(carry(x,y,z),u) = admit(x,u){x -> carry(x,y,z)}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = x2 p(=) = x2 p(admit) = 0 p(carry) = 0 p(cond) = 8*x1 + 4*x2 p(nil) = 0 p(sum) = 8 p(true) = 2 p(w) = 0 Following rules are strictly oriented: cond(true(),y) = 16 + 4*y > y = y Following rules are (at-least) weakly oriented: admit(x,.(u,.(v,.(w(),z)))) = 0 >= 0 = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) = 0 >= 0 = nil() ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() - Weak TRS: cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = x1 + x2 p(=) = 2 + x1 p(admit) = 2 + 8*x1 + 2*x2 p(carry) = 1 + x1 p(cond) = x1 + x2 p(nil) = 12 p(sum) = 2 + x3 p(true) = 1 p(w) = 12 Following rules are strictly oriented: admit(x,nil()) = 26 + 8*x > 12 = nil() Following rules are (at-least) weakly oriented: admit(x,.(u,.(v,.(w(),z)))) = 26 + 2*u + 2*v + 8*x + 2*z >= 26 + u + 2*v + 8*x + 2*z = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) cond(true(),y) = 1 + y >= y = y ** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) - Weak TRS: admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = x1 + x2 p(=) = 0 p(admit) = 3 + x1 + 2*x2 p(carry) = 6 + x3 p(cond) = x2 p(nil) = 2 p(sum) = 8 + x1 + x2 p(true) = 1 p(w) = 7 Following rules are strictly oriented: admit(x,.(u,.(v,.(w(),z)))) = 17 + 2*u + 2*v + x + 2*z > 16 + u + 2*v + 2*z = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) Following rules are (at-least) weakly oriented: admit(x,nil()) = 7 + x >= 2 = nil() cond(true(),y) = y >= y = y ** Step 1.b:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))