WORST_CASE(?,O(n^1)) * Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(A,B,C,D) -> f(0,1,1,D) True (1,1) 1. f(A,B,C,D) -> f(1 + A,2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1) 2. f(A,B,C,D) -> end(A,B,C,D) [C >= 1 + D] (?,1) Signature: {(end,4);(f,4);(sqrt,4)} Flow Graph: [0->{1,2},1->{1,2},2->{}] + Applied Processor: RestrictVarsProcessor + Details: We removed the arguments [A] . * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(B,C,D) -> f(1,1,D) True (1,1) 1. f(B,C,D) -> f(2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1) 2. f(B,C,D) -> end(B,C,D) [C >= 1 + D] (?,1) Signature: {(end,3);(f,3);(sqrt,3)} Flow Graph: [0->{1,2},1->{1,2},2->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,B>, 1, .= 1) (<0,0,C>, 1, .= 1) (<0,0,D>, D, .= 0) (<1,0,B>, 2 + B, .+ 2) (<1,0,C>, 2 + B + C, .* 2) (<1,0,D>, D, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>, C, .= 0) (<2,0,D>, D, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(B,C,D) -> f(1,1,D) True (1,1) 1. f(B,C,D) -> f(2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1) 2. f(B,C,D) -> end(B,C,D) [C >= 1 + D] (?,1) Signature: {(end,3);(f,3);(sqrt,3)} Flow Graph: [0->{1,2},1->{1,2},2->{}] Sizebounds: (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,B>, 1) (<0,0,C>, 1) (<0,0,D>, D) (<1,0,B>, ?) (<1,0,C>, 3 + D) (<1,0,D>, D) (<2,0,B>, ?) (<2,0,C>, 3 + D) (<2,0,D>, D) * Step 4: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(B,C,D) -> f(1,1,D) True (1,1) 1. f(B,C,D) -> f(2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1) 2. f(B,C,D) -> end(B,C,D) [C >= 1 + D] (?,1) Signature: {(end,3);(f,3);(sqrt,3)} Flow Graph: [0->{1,2},1->{1,2},2->{}] Sizebounds: (<0,0,B>, 1) (<0,0,C>, 1) (<0,0,D>, D) (<1,0,B>, ?) (<1,0,C>, 3 + D) (<1,0,D>, D) (<2,0,B>, ?) (<2,0,C>, 3 + D) (<2,0,D>, D) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [2] * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(B,C,D) -> f(1,1,D) True (1,1) 1. f(B,C,D) -> f(2 + B,2 + B + C,D) [D >= C && B >= 0] (?,1) Signature: {(end,3);(f,3);(sqrt,3)} Flow Graph: [0->{1},1->{1}] Sizebounds: (<0,0,B>, 1) (<0,0,C>, 1) (<0,0,D>, D) (<1,0,B>, ?) (<1,0,C>, 3 + D) (<1,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f) = 1 + -1*x2 + x3 p(sqrt) = x3 The following rules are strictly oriented: [D >= C && B >= 0] ==> f(B,C,D) = 1 + -1*C + D > -1 + -1*B + -1*C + D = f(2 + B,2 + B + C,D) The following rules are weakly oriented: True ==> sqrt(B,C,D) = D >= D = f(1,1,D) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. sqrt(B,C,D) -> f(1,1,D) True (1,1) 1. f(B,C,D) -> f(2 + B,2 + B + C,D) [D >= C && B >= 0] (D,1) Signature: {(end,3);(f,3);(sqrt,3)} Flow Graph: [0->{1},1->{1}] Sizebounds: (<0,0,B>, 1) (<0,0,C>, 1) (<0,0,D>, D) (<1,0,B>, ?) (<1,0,C>, 3 + D) (<1,0,D>, D) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^1))