YES * Step 1: FromIts YES + Considered Problem: Rules: 0. evalndloopstart(A) -> evalndloopentryin(A) True (1,1) 1. evalndloopentryin(A) -> evalndloopbbin(0) True (?,1) 2. evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] (?,1) 3. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] (?,1) 4. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] (?,1) 5. evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] (?,1) 6. evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] (?,1) Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Flow Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: evalndloopstart(A) -> evalndloopentryin(A) True evalndloopentryin(A) -> evalndloopbbin(0) True evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Rule Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[2] c: [2] * Step 3: CloseWith YES + Considered Problem: (Rules: evalndloopstart(A) -> evalndloopentryin(A) True evalndloopentryin(A) -> evalndloopbbin(0) True evalndloopbbin(A) -> evalndloopbbin(B) [A >= 0 && 2 + A >= B && B >= 1 + A && 9 >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 3 + A] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && A >= B] evalndloopbbin(A) -> evalndloopreturnin(A) [A >= 0 && B >= 10] evalndloopreturnin(A) -> evalndloopstop(A) [A >= 0] Signature: {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)} Rule Graph: [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES