YES(?,O(n^1)) * Step 1: TrivialSCCs 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) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= C && B >= 0] 2. f(A,B,C,D) -> end(A,B,C,D) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + D] Signature: {(end,4);(f,4);(sqrt,4)} Flow Graph: [0->{1,2},1->{1,2},2->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks 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) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= C && B >= 0] 2. f(A,B,C,D) -> end(A,B,C,D) [-1 + C >= 0 (1,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + D] Signature: {(end,4);(f,4);(sqrt,4)} Flow Graph: [0->{1,2},1->{1,2},2->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer 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) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= C && B >= 0] 2. f(A,B,C,D) -> end(A,B,C,D) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + D] 3. f(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(end,4);(exitus616,4);(f,4);(sqrt,4)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{},3->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3] | `- p:[1] c: [1] * Step 4: SizeAbstraction 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) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= C && B >= 0] 2. f(A,B,C,D) -> end(A,B,C,D) [-1 + C >= 0 (?,1) && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + D] 3. f(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(end,4);(exitus616,4);(f,4);(sqrt,4)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{},3->{}] ,We construct a looptree: P: [0,1,2,3] | `- p:[1] c: [1]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,C,D,0.0] sqrt ~> f [A <= 0*K, B <= K, C <= K, D <= D] f ~> f [A <= D, B <= B + C + D, C <= 2*K + B + C, D <= D] f ~> end [A <= A, B <= B, C <= C, D <= D] f ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + B + D] f ~> f [A <= D, B <= B + C + D, C <= 2*K + B + C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0] sqrt ~> f [K ~=> A,K ~=> B,K ~=> C] f ~> f [D ~=> A,B ~+> B,B ~+> C,C ~+> B,C ~+> C,D ~+> B,K ~*> C] f ~> end [] f ~> exitus616 [] + Loop: [B ~+> 0.0,D ~+> 0.0,K ~+> 0.0] f ~> f [D ~=> A,B ~+> B,B ~+> C,C ~+> B,C ~+> C,D ~+> B,K ~*> C] + Applied Processor: LareProcessor + Details: sqrt ~> exitus616 [D ~=> A ,K ~=> A ,K ~=> B ,K ~=> C ,D ~+> B ,D ~+> C ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,D ~*> B ,D ~*> C ,K ~*> B ,K ~*> C ,K ~*> 0.0 ,K ~*> tick ,D ~^> B ,D ~^> C ,K ~^> B ,K ~^> C] sqrt ~> end [D ~=> A ,K ~=> A ,K ~=> B ,K ~=> C ,D ~+> B ,D ~+> C ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,D ~*> B ,D ~*> C ,K ~*> B ,K ~*> C ,K ~*> 0.0 ,K ~*> tick ,D ~^> B ,D ~^> C ,K ~^> B ,K ~^> C] + f> [D ~=> A ,B ~+> B ,B ~+> C ,B ~+> 0.0 ,B ~+> tick ,C ~+> B ,C ~+> C ,D ~+> B ,D ~+> C ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,B ~*> B ,B ~*> C ,C ~*> B ,C ~*> C ,D ~*> B ,D ~*> C ,K ~*> B ,K ~*> C ,B ~^> B ,B ~^> C ,D ~^> B ,D ~^> C ,K ~^> B ,K ~^> C] YES(?,O(n^1))