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: Sum. 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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: 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: Ara. 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: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun ".") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "=") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "admit") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "carry") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "cond") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "sum") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "w") :: [] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: admit(x,nil()) -> nil() 2. Weak: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) cond(true(),y) -> y ** Step 1.b:2: NaturalMI. 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))))) cond(true(),y) -> y - Weak TRS: admit(x,nil()) -> nil() - 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: 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = [1] x2 + [0] p(=) = [1] x2 + [0] p(admit) = [0] p(carry) = [1] x1 + [8] p(cond) = [4] x1 + [8] x2 + [0] p(nil) = [0] p(sum) = [1] x2 + [1] x3 + [0] p(true) = [5] p(w) = [0] Following rules are strictly oriented: cond(true(),y) = [8] y + [20] > [1] y + [0] = 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:3: NaturalMI. 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: 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = [1] x1 + [1] x2 + [0] p(=) = [1] x1 + [1] x2 + [0] p(admit) = [8] x1 + [4] x2 + [0] p(carry) = [0] p(cond) = [2] x1 + [1] x2 + [0] p(nil) = [0] p(sum) = [1] x1 + [1] x3 + [2] p(true) = [1] p(w) = [6] Following rules are strictly oriented: admit(x,.(u,.(v,.(w(),z)))) = [4] u + [4] v + [8] x + [4] z + [24] > [1] u + [3] v + [2] x + [4] z + [22] = 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()) = [8] x + [0] >= [0] = nil() cond(true(),y) = [1] y + [2] >= [1] y + [0] = 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))