YES(?,PRIMREC) * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{3,4,5 ,6,7,8},9->{2},10->{2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,3),(8,4),(8,5),(8,6),(8,7),(8,8)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] (1,1) 1. eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] (1,1) 2. eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] (?,1) 3. eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] (?,1) 4. eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] (?,1) 5. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 6. eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] (?,1) 7. eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] (?,1) 8. eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] (?,1) 9. eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] (?,1) 10. eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] (?,1) Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Flow Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{} ,9->{2},10->{2}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: eval1(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2] eval1(A,B,C,D) -> eval2(A,-1 + B,C,D) [1 >= A] eval2(A,B,C,D) -> eval3(A,B,A,2*A) [B >= 2] eval3(A,B,C,D) -> eval4(A,B,C,D) [B >= D && B >= 1 + D] eval3(A,B,C,D) -> eval4(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3(A,B,C,D) -> eval3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3(A,B,C,D) -> eval3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3(A,B,C,D) -> eval4(A,B,C,D) [B = D] eval3(A,B,C,D) -> eval3(A,B,D,2*D) [D >= 1 && B = D] eval4(A,B,C,D) -> eval2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] eval4(A,B,C,D) -> eval2(A,-1 + B,C,D) [B >= 2 && A = 1] Signature: {(eval1,4);(eval2,4);(eval3,4);(eval4,4)} Rule Graph: [0->{2},1->{2},2->{3,4,5,6,7,8},3->{9,10},4->{9,10},5->{3,4,5,6,7,8},6->{3,4,5,6,7,8},7->{9,10},8->{} ,9->{2},10->{2}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: eval1.0(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2] eval1.1(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [1 >= A] eval2.2(A,B,C,D) -> eval3.3(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.4(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.5(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.6(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.7(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.8(A,B,A,2*A) [B >= 2] eval3.3(A,B,C,D) -> eval4.9(A,B,C,D) [B >= D && B >= 1 + D] eval3.3(A,B,C,D) -> eval4.10(A,B,C,D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.9(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.10(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.5(A,B,C,D) -> eval3.3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.4(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.5(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.6(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.7(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.8(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.4(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.5(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.6(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.7(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.8(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.7(A,B,C,D) -> eval4.9(A,B,C,D) [B = D] eval3.7(A,B,C,D) -> eval4.10(A,B,C,D) [B = D] eval3.8(A,B,C,D) -> eval3.11(A,B,D,2*D) [D >= 1 && B = D] eval4.9(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] eval4.10(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [B >= 2 && A = 1] Signature: {(eval1.0,4) ;(eval1.1,4) ;(eval2.2,4) ;(eval3.11,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval3.5,4) ;(eval3.6,4) ;(eval3.7,4) ;(eval3.8,4) ;(eval4.10,4) ;(eval4.9,4)} Rule Graph: [0->{2,3,4,5,6,7},1->{2,3,4,5,6,7},2->{8,9},3->{10,11},4->{12,13,14,15,16,17},5->{18,19,20,21,22,23} ,6->{24,25},7->{26},8->{27},9->{28},10->{27},11->{28},12->{8,9},13->{10,11},14->{12,13,14,15,16,17},15->{18 ,19,20,21,22,23},16->{24,25},17->{26},18->{8,9},19->{10,11},20->{12,13,14,15,16,17},21->{18,19,20,21,22,23} ,22->{24,25},23->{26},24->{27},25->{28},26->{},27->{2,3,4,5,6,7},28->{2,3,4,5,6,7}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: eval1.0(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2] eval1.1(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [1 >= A] eval2.2(A,B,C,D) -> eval3.3(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.4(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.5(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.6(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.7(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.8(A,B,A,2*A) [B >= 2] eval3.3(A,B,C,D) -> eval4.9(A,B,C,D) [B >= D && B >= 1 + D] eval3.3(A,B,C,D) -> eval4.10(A,B,C,D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.9(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.10(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.5(A,B,C,D) -> eval3.3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.4(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.5(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.6(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.7(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.8(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.4(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.5(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.6(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.7(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.8(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.7(A,B,C,D) -> eval4.9(A,B,C,D) [B = D] eval3.7(A,B,C,D) -> eval4.10(A,B,C,D) [B = D] eval3.8(A,B,C,D) -> eval3.11(A,B,D,2*D) [D >= 1 && B = D] eval4.9(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] eval4.10(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [B >= 2 && A = 1] eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(eval1.0,4) ;(eval1.1,4) ;(eval2.2,4) ;(eval3.11,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval3.5,4) ;(eval3.6,4) ;(eval3.7,4) ;(eval3.8,4) ;(eval4.10,4) ;(eval4.9,4) ;(exitus616,4)} Rule Graph: [0->{2,3,4,5,6,7},1->{2,3,4,5,6,7},2->{8,9},3->{10,11},4->{12,13,14,15,16,17},5->{18,19,20,21,22,23} ,6->{24,25},7->{26},8->{27},9->{28},10->{27},11->{28},12->{8,9},13->{10,11},14->{12,13,14,15,16,17},15->{18 ,19,20,21,22,23},16->{24,25},17->{26},18->{8,9},19->{10,11},20->{12,13,14,15,16,17},21->{18,19,20,21,22,23} ,22->{24,25},23->{26},24->{27},25->{28},26->{29,30,31,32,33,34},27->{2,3,4,5,6,7},28->{2,3,4,5,6,7}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] | `- p:[2,27,8,12,4,28,9,18,5,15,14,20,21,11,3,13,19,25,6,16,22,10,24] c: [2,3,4,5,6,8,9,10,11,12,13,16,18,19,22,24,25,27,28] | `- p:[14,20,15,21] c: [14,15,20,21] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: eval1.0(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2] eval1.1(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [1 >= A] eval2.2(A,B,C,D) -> eval3.3(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.4(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.5(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.6(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.7(A,B,A,2*A) [B >= 2] eval2.2(A,B,C,D) -> eval3.8(A,B,A,2*A) [B >= 2] eval3.3(A,B,C,D) -> eval4.9(A,B,C,D) [B >= D && B >= 1 + D] eval3.3(A,B,C,D) -> eval4.10(A,B,C,D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.9(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.4(A,B,C,D) -> eval4.10(A,B,C,1 + D) [B >= D && B >= 1 + D] eval3.5(A,B,C,D) -> eval3.3(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.4(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.5(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.6(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.7(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.5(A,B,C,D) -> eval3.8(A,B,D,2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.3(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.4(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.5(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.6(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.7(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.6(A,B,C,D) -> eval3.8(A,B,1 + D,2 + 2*D) [B >= D && B >= 1 + D && D >= 1] eval3.7(A,B,C,D) -> eval4.9(A,B,C,D) [B = D] eval3.7(A,B,C,D) -> eval4.10(A,B,C,D) [B = D] eval3.8(A,B,C,D) -> eval3.11(A,B,D,2*D) [D >= 1 && B = D] eval4.9(A,B,C,D) -> eval2.2(-1 + A,B,C,D) [A >= 2 && A >= 1 && B >= 2] eval4.10(A,B,C,D) -> eval2.2(A,-1 + B,C,D) [B >= 2 && A = 1] eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True eval3.11(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(eval1.0,4) ;(eval1.1,4) ;(eval2.2,4) ;(eval3.11,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval3.5,4) ;(eval3.6,4) ;(eval3.7,4) ;(eval3.8,4) ;(eval4.10,4) ;(eval4.9,4) ;(exitus616,4)} Rule Graph: [0->{2,3,4,5,6,7},1->{2,3,4,5,6,7},2->{8,9},3->{10,11},4->{12,13,14,15,16,17},5->{18,19,20,21,22,23} ,6->{24,25},7->{26},8->{27},9->{28},10->{27},11->{28},12->{8,9},13->{10,11},14->{12,13,14,15,16,17},15->{18 ,19,20,21,22,23},16->{24,25},17->{26},18->{8,9},19->{10,11},20->{12,13,14,15,16,17},21->{18,19,20,21,22,23} ,22->{24,25},23->{26},24->{27},25->{28},26->{29,30,31,32,33,34},27->{2,3,4,5,6,7},28->{2,3,4,5,6,7}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34] | `- p:[2,27,8,12,4,28,9,18,5,15,14,20,21,11,3,13,19,25,6,16,22,10,24] c: [2,3,4,5,6,8,9,10,11,12,13,16,18,19,22,24,25,27,28] | `- p:[14,20,15,21] c: [14,15,20,21]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] eval1.0 ~> eval2.2 [A <= A, B <= B, C <= C, D <= D] eval1.1 ~> eval2.2 [A <= A, B <= K + B, C <= C, D <= D] eval2.2 ~> eval3.3 [A <= A, B <= B, C <= A, D <= 2*A] eval2.2 ~> eval3.4 [A <= A, B <= B, C <= A, D <= 2*A] eval2.2 ~> eval3.5 [A <= A, B <= B, C <= A, D <= 2*A] eval2.2 ~> eval3.6 [A <= A, B <= B, C <= A, D <= 2*A] eval2.2 ~> eval3.7 [A <= A, B <= B, C <= A, D <= 2*A] eval2.2 ~> eval3.8 [A <= A, B <= B, C <= A, D <= 2*A] eval3.3 ~> eval4.9 [A <= A, B <= B, C <= C, D <= D] eval3.3 ~> eval4.10 [A <= A, B <= B, C <= C, D <= D] eval3.4 ~> eval4.9 [A <= A, B <= B, C <= C, D <= K + D] eval3.4 ~> eval4.10 [A <= A, B <= B, C <= C, D <= K + D] eval3.5 ~> eval3.3 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.4 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.5 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.6 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.7 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.8 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.3 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.4 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.5 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.6 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.7 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.8 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.7 ~> eval4.9 [A <= A, B <= B, C <= C, D <= D] eval3.7 ~> eval4.10 [A <= A, B <= B, C <= C, D <= D] eval3.8 ~> eval3.11 [A <= A, B <= B, C <= D, D <= B + D] eval4.9 ~> eval2.2 [A <= A, B <= B, C <= C, D <= D] eval4.10 ~> eval2.2 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] eval3.11 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= A + B] eval2.2 ~> eval3.3 [A <= A, B <= B, C <= A, D <= 2*A] eval4.9 ~> eval2.2 [A <= A, B <= B, C <= C, D <= D] eval3.3 ~> eval4.9 [A <= A, B <= B, C <= C, D <= D] eval3.5 ~> eval3.3 [A <= A, B <= B, C <= D, D <= B + D] eval2.2 ~> eval3.5 [A <= A, B <= B, C <= A, D <= 2*A] eval4.10 ~> eval2.2 [A <= A, B <= B, C <= C, D <= D] eval3.3 ~> eval4.10 [A <= A, B <= B, C <= C, D <= D] eval3.6 ~> eval3.3 [A <= A, B <= B, C <= B, D <= K + B + D] eval2.2 ~> eval3.6 [A <= A, B <= B, C <= A, D <= 2*A] eval3.5 ~> eval3.6 [A <= A, B <= B, C <= D, D <= B + D] eval3.5 ~> eval3.5 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.5 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.6 ~> eval3.6 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.4 ~> eval4.10 [A <= A, B <= B, C <= C, D <= K + D] eval2.2 ~> eval3.4 [A <= A, B <= B, C <= A, D <= 2*A] eval3.5 ~> eval3.4 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.4 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.7 ~> eval4.10 [A <= A, B <= B, C <= C, D <= D] eval2.2 ~> eval3.7 [A <= A, B <= B, C <= A, D <= 2*A] eval3.5 ~> eval3.7 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.7 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.4 ~> eval4.9 [A <= A, B <= B, C <= C, D <= K + D] eval3.7 ~> eval4.9 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= 3*K + 2*B + 2*D] eval3.5 ~> eval3.5 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.5 [A <= A, B <= B, C <= B, D <= K + B + D] eval3.5 ~> eval3.6 [A <= A, B <= B, C <= D, D <= B + D] eval3.6 ~> eval3.6 [A <= A, B <= B, C <= B, D <= K + B + D] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] eval1.0 ~> eval2.2 [] eval1.1 ~> eval2.2 [B ~+> B,K ~+> B] eval2.2 ~> eval3.3 [A ~=> C,A ~*> D] eval2.2 ~> eval3.4 [A ~=> C,A ~*> D] eval2.2 ~> eval3.5 [A ~=> C,A ~*> D] eval2.2 ~> eval3.6 [A ~=> C,A ~*> D] eval2.2 ~> eval3.7 [A ~=> C,A ~*> D] eval2.2 ~> eval3.8 [A ~=> C,A ~*> D] eval3.3 ~> eval4.9 [] eval3.3 ~> eval4.10 [] eval3.4 ~> eval4.9 [D ~+> D,K ~+> D] eval3.4 ~> eval4.10 [D ~+> D,K ~+> D] eval3.5 ~> eval3.3 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.4 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.5 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.6 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.7 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.8 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.4 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.5 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.6 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.7 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.8 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.7 ~> eval4.9 [] eval3.7 ~> eval4.10 [] eval3.8 ~> eval3.11 [D ~=> C,B ~+> D,D ~+> D] eval4.9 ~> eval2.2 [] eval4.10 ~> eval2.2 [] eval3.11 ~> exitus616 [] eval3.11 ~> exitus616 [] eval3.11 ~> exitus616 [] eval3.11 ~> exitus616 [] eval3.11 ~> exitus616 [] eval3.11 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] eval2.2 ~> eval3.3 [A ~=> C,A ~*> D] eval4.9 ~> eval2.2 [] eval3.3 ~> eval4.9 [] eval3.5 ~> eval3.3 [D ~=> C,B ~+> D,D ~+> D] eval2.2 ~> eval3.5 [A ~=> C,A ~*> D] eval4.10 ~> eval2.2 [] eval3.3 ~> eval4.10 [] eval3.6 ~> eval3.3 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval2.2 ~> eval3.6 [A ~=> C,A ~*> D] eval3.5 ~> eval3.6 [D ~=> C,B ~+> D,D ~+> D] eval3.5 ~> eval3.5 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.5 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.6 ~> eval3.6 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.4 ~> eval4.10 [D ~+> D,K ~+> D] eval2.2 ~> eval3.4 [A ~=> C,A ~*> D] eval3.5 ~> eval3.4 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.4 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.7 ~> eval4.10 [] eval2.2 ~> eval3.7 [A ~=> C,A ~*> D] eval3.5 ~> eval3.7 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.7 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.4 ~> eval4.9 [D ~+> D,K ~+> D] eval3.7 ~> eval4.9 [] + Loop: [B ~*> 0.0.0,D ~*> 0.0.0,K ~*> 0.0.0] eval3.5 ~> eval3.5 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.5 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] eval3.5 ~> eval3.6 [D ~=> C,B ~+> D,D ~+> D] eval3.6 ~> eval3.6 [B ~=> C,B ~+> D,D ~+> D,K ~+> D] + Applied Processor: Lare + Details: eval1.1 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> tick ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,K ~^> C ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] eval1.0 ~> exitus616 [A ~+> 0.0 ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick] + eval2.2> [A ~=> C ,B ~=> C ,D ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick] eval3.6> [A ~=> C ,B ~=> C ,D ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick] eval3.5> [A ~=> C ,B ~=> C ,D ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> tick ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick] + eval3.5> [B ~=> C ,D ~=> C ,B ~+> D ,D ~+> D ,tick ~+> tick ,K ~+> D ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] eval3.6> [B ~=> C ,D ~=> C ,B ~+> C ,B ~+> D ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] eval3.5> [B ~=> C ,D ~=> C ,B ~+> C ,B ~+> D ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] eval3.6> [B ~=> C ,D ~=> C ,B ~+> C ,B ~+> D ,D ~+> C ,D ~+> D ,tick ~+> tick ,K ~+> C ,K ~+> D ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)