YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0 (?,1) && -1 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && D >= 1 + A] 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && A >= D] 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0 (?,1) && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -1 + -1*B + D >= 0 && -1 + A + D >= 0 && -1 + -1*A + D >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (1,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (1,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0 (?,1) && -1 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && D >= 1 + A] 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [B + -1*C >= 0 (1,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && A >= D] 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0 (?,1) && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -1 + -1*B + D >= 0 && -1 + A + D >= 0 && -1 + -1*A + D >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (1,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4} ,11->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0 (?,1) && -1 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && D >= 1 + A] 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && A >= D] 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0 (?,1) && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -1 + -1*B + D >= 0 && -1 + A + D >= 0 && -1 + -1*A + D >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 12. evalSimpleSingle2returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11,12},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11,12},10->{2,3,4} ,11->{},12->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,7,5,3,10,8,6] c: [10] | `- p:[2,7,5,3] c: [7] * Step 4: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. evalSimpleSingle2start(A,B,C,D) -> evalSimpleSingle2entryin(A,B,C,D) True (1,1) 1. evalSimpleSingle2entryin(A,B,C,D) -> evalSimpleSingle2bb4in(0,0,C,D) True (?,1) 2. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1) 3. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2bbin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1] (?,1) 4. evalSimpleSingle2bb4in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 5. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb1in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 6. evalSimpleSingle2bbin(A,B,C,D) -> evalSimpleSingle2bb2in(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 7. evalSimpleSingle2bb1in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0 (?,1) && -1 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 8. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2bb3in(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && D >= 1 + A] 9. evalSimpleSingle2bb2in(A,B,C,D) -> evalSimpleSingle2returnin(A,B,C,D) [B + -1*C >= 0 (?,1) && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && A >= D] 10. evalSimpleSingle2bb3in(A,B,C,D) -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0 (?,1) && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -1 + -1*B + D >= 0 && -1 + A + D >= 0 && -1 + -1*A + D >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D) [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 12. evalSimpleSingle2returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalSimpleSingle2bb1in,4) ;(evalSimpleSingle2bb2in,4) ;(evalSimpleSingle2bb3in,4) ;(evalSimpleSingle2bb4in,4) ;(evalSimpleSingle2bbin,4) ;(evalSimpleSingle2entryin,4) ;(evalSimpleSingle2returnin,4) ;(evalSimpleSingle2start,4) ;(evalSimpleSingle2stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11,12},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11,12},10->{2,3,4} ,11->{},12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[2,7,5,3,10,8,6] c: [10] | `- p:[2,7,5,3] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalSimpleSingle2start ~> evalSimpleSingle2entryin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2entryin ~> evalSimpleSingle2bb4in [A <= 0*K, B <= 0*K, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2returnin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= C, B <= C, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2returnin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A <= D, B <= D, C <= C, D <= D] evalSimpleSingle2returnin ~> evalSimpleSingle2stop [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2returnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B + D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= C, B <= C, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [A <= D, B <= D, C <= C, D <= D] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= B + C] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [A <= C, B <= C, C <= C, D <= D] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [A <= A, B <= B, C <= C, D <= D] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [A <= A, B <= B, C <= C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalSimpleSingle2start ~> evalSimpleSingle2entryin [] evalSimpleSingle2entryin ~> evalSimpleSingle2bb4in [K ~=> A,K ~=> B] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb4in ~> evalSimpleSingle2returnin [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [C ~=> A,C ~=> B] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [] evalSimpleSingle2bb2in ~> evalSimpleSingle2returnin [] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [D ~=> A,D ~=> B] evalSimpleSingle2returnin ~> evalSimpleSingle2stop [] evalSimpleSingle2returnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,D ~+> 0.0,K ~+> 0.0] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [C ~=> A,C ~=> B] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb3in ~> evalSimpleSingle2bb4in [D ~=> A,D ~=> B] evalSimpleSingle2bb2in ~> evalSimpleSingle2bb3in [] evalSimpleSingle2bbin ~> evalSimpleSingle2bb2in [] + Loop: [B ~+> 0.0.0,C ~+> 0.0.0] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] evalSimpleSingle2bb1in ~> evalSimpleSingle2bb4in [C ~=> A,C ~=> B] evalSimpleSingle2bbin ~> evalSimpleSingle2bb1in [] evalSimpleSingle2bb4in ~> evalSimpleSingle2bbin [] + Applied Processor: LareProcessor + Details: evalSimpleSingle2start ~> exitus616 [C ~=> A ,C ~=> B ,D ~=> A ,D ~=> B ,K ~=> A ,K ~=> B ,C ~+> 0.0 ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0 ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> 0.0 ,D ~*> tick ,K ~*> 0.0 ,K ~*> tick] evalSimpleSingle2start ~> evalSimpleSingle2stop [C ~=> A ,C ~=> B ,D ~=> A ,D ~=> B ,K ~=> A ,K ~=> B ,C ~+> 0.0 ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0 ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> 0.0 ,D ~*> tick ,K ~*> 0.0 ,K ~*> tick] + evalSimpleSingle2bb4in> [C ~=> A ,C ~=> B ,D ~=> A ,D ~=> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> tick ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> tick ,K ~*> tick] evalSimpleSingle2bb2in> [C ~=> A ,C ~=> B ,D ~=> A ,D ~=> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> 0.0 ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> tick ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> tick ,D ~*> tick ,K ~*> tick] + evalSimpleSingle2bbin> [C ~=> A ,C ~=> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick] evalSimpleSingle2bb4in> [C ~=> A ,C ~=> B ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick] YES(?,POLY)