YES(?,PRIMREC) * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f(A,B,C) -> g(A,1,1) True (1,1) 1. g(A,B,C) -> g(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] (?,1) 2. g(A,B,C) -> h(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1) 3. h(A,B,C) -> h(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] (?,1) 4. h(A,B,C) -> i(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] (?,1) 5. i(A,B,C) -> i(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] (?,1) Signature: {(f,3);(g,3);(h,3);(i,3)} Flow Graph: [0->{1,2},1->{1,2},2->{3,4},3->{3,4},4->{5},5->{5}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f(A,B,C) -> g(A,1,1) True (1,1) 1. g(A,B,C) -> g(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] (?,1) 2. g(A,B,C) -> h(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] (?,1) 3. h(A,B,C) -> h(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] (?,1) 4. h(A,B,C) -> i(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] (?,1) 5. i(A,B,C) -> i(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] (?,1) Signature: {(f,3);(g,3);(h,3);(i,3)} Flow Graph: [0->{1,2},1->{1,2},2->{3},3->{3,4},4->{5},5->{5}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f(A,B,C) -> g(A,1,1) True g(A,B,C) -> g(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g(A,B,C) -> h(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] h(A,B,C) -> h(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h(A,B,C) -> i(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] i(A,B,C) -> i(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] Signature: {(f,3);(g,3);(h,3);(i,3)} Rule Graph: [0->{1,2},1->{1,2},2->{3},3->{3,4},4->{5},5->{5}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f.0(A,B,C) -> g.1(A,1,1) True f.0(A,B,C) -> g.2(A,1,1) True g.1(A,B,C) -> g.1(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.1(A,B,C) -> g.2(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.2(A,B,C) -> h.3(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] h.3(A,B,C) -> h.3(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.3(A,B,C) -> h.4(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.4(A,B,C) -> i.5(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] i.5(A,B,C) -> i.5(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] Signature: {(f.0,3);(g.1,3);(g.2,3);(h.3,3);(h.4,3);(i.5,3)} Rule Graph: [0->{2,3},1->{4},2->{2,3},3->{4},4->{5,6},5->{5,6},6->{7},7->{8},8->{8}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: f.0(A,B,C) -> g.1(A,1,1) True f.0(A,B,C) -> g.2(A,1,1) True g.1(A,B,C) -> g.1(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.1(A,B,C) -> g.2(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.2(A,B,C) -> h.3(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] h.3(A,B,C) -> h.3(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.3(A,B,C) -> h.4(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.4(A,B,C) -> i.5(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] i.5(A,B,C) -> i.5(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] i.5(A,B,C) -> exitus616(A,B,C) True i.5(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3);(f.0,3);(g.1,3);(g.2,3);(h.3,3);(h.4,3);(i.5,3)} Rule Graph: [0->{2,3},1->{4},2->{2,3},3->{4},4->{5,6},5->{5,6},6->{7},7->{8},8->{8,9,10}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | +- p:[2] c: [2] | +- p:[5] c: [5] | `- p:[8] c: [8] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: f.0(A,B,C) -> g.1(A,1,1) True f.0(A,B,C) -> g.2(A,1,1) True g.1(A,B,C) -> g.1(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.1(A,B,C) -> g.2(-1 + A,2*B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && -1 + A >= 0] g.2(A,B,C) -> h.3(A,B,C) [1 + -1*C >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + B >= 0 && 0 >= A] h.3(A,B,C) -> h.3(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.3(A,B,C) -> h.4(A,-1 + B,2*C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && -1 + B >= 0] h.4(A,B,C) -> i.5(A,B,C) [-1 + C >= 0 && -2 + B + C >= 0 && -1 + -1*A + C >= 0 && -1*A >= 0 && 0 >= B] i.5(A,B,C) -> i.5(A,B,-1 + C) [-1*B >= 0 && -1*A + -1*B >= 0 && -1*A >= 0 && -1 + C >= 0] i.5(A,B,C) -> exitus616(A,B,C) True i.5(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3);(f.0,3);(g.1,3);(g.2,3);(h.3,3);(h.4,3);(i.5,3)} Rule Graph: [0->{2,3},1->{4},2->{2,3},3->{4},4->{5,6},5->{5,6},6->{7},7->{8},8->{8,9,10}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | +- p:[2] c: [2] | +- p:[5] c: [5] | `- p:[8] c: [8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,0.0,0.1,0.2] f.0 ~> g.1 [A <= A, B <= K, C <= K] f.0 ~> g.2 [A <= A, B <= K, C <= K] g.1 ~> g.1 [A <= A, B <= 2*B, C <= C] g.1 ~> g.2 [A <= A, B <= 2*B, C <= C] g.2 ~> h.3 [A <= A, B <= B, C <= C] h.3 ~> h.3 [A <= A, B <= B, C <= 2*C] h.3 ~> h.4 [A <= A, B <= B, C <= 2*C] h.4 ~> i.5 [A <= A, B <= B, C <= C] i.5 ~> i.5 [A <= A, B <= B, C <= C] i.5 ~> exitus616 [A <= A, B <= B, C <= C] i.5 ~> exitus616 [A <= A, B <= B, C <= C] + Loop: [0.0 <= K + A] g.1 ~> g.1 [A <= A, B <= 2*B, C <= C] + Loop: [0.1 <= K + B] h.3 ~> h.3 [A <= A, B <= B, C <= 2*C] + Loop: [0.2 <= K + C] i.5 ~> i.5 [A <= A, B <= B, C <= C] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,0.0,0.1,0.2] f.0 ~> g.1 [K ~=> B,K ~=> C] f.0 ~> g.2 [K ~=> B,K ~=> C] g.1 ~> g.1 [B ~*> B] g.1 ~> g.2 [B ~*> B] g.2 ~> h.3 [] h.3 ~> h.3 [C ~*> C] h.3 ~> h.4 [C ~*> C] h.4 ~> i.5 [] i.5 ~> i.5 [] i.5 ~> exitus616 [] i.5 ~> exitus616 [] + Loop: [A ~+> 0.0,K ~+> 0.0] g.1 ~> g.1 [B ~*> B] + Loop: [B ~+> 0.1,K ~+> 0.1] h.3 ~> h.3 [C ~*> C] + Loop: [C ~+> 0.2,K ~+> 0.2] i.5 ~> i.5 [] + Applied Processor: Lare + Details: f.0 ~> exitus616 [K ~=> B ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> tick ,K ~*> B ,K ~*> C ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> tick ,A ~^> B ,A ~^> C ,A ~^> 0.1 ,A ~^> 0.2 ,A ~^> tick ,K ~^> B ,K ~^> C ,K ~^> 0.1 ,K ~^> 0.2 ,K ~^> tick] + g.1> [A ~+> 0.0,A ~+> tick,tick ~+> tick,K ~+> 0.0,K ~+> tick,B ~*> B,A ~^> B,K ~^> B] + h.3> [B ~+> 0.1,B ~+> tick,tick ~+> tick,K ~+> 0.1,K ~+> tick,C ~*> C,B ~^> C,K ~^> C] + i.5> [C ~+> 0.2,C ~+> tick,tick ~+> tick,K ~+> 0.2,K ~+> tick] YES(?,PRIMREC)