NO Initial ITS Start location: l14 0: l0 -> l1 : __const_5^0'=__const_5^post0, WItemsNum^0'=WItemsNum^post0, tmp1^0'=tmp1^post0, (1+__const_5^0-WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0 /\ __const_5^0-__const_5^post0 == 0), cost: 1 1: l0 -> l2 : __const_5^0'=__const_5^post1, WItemsNum^0'=WItemsNum^post1, tmp1^0'=tmp1^post1, (0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0), cost: 1 11: l1 -> l5 : __const_5^0'=__const_5^post11, WItemsNum^0'=WItemsNum^post11, tmp1^0'=tmp1^post11, (__const_5^0-__const_5^post11 == 0 /\ WItemsNum^0-WItemsNum^post11 == 0 /\ -tmp1^post11+tmp1^0 == 0), cost: 1 14: l2 -> l1 : __const_5^0'=__const_5^post14, WItemsNum^0'=WItemsNum^post14, tmp1^0'=tmp1^post14, (-tmp1^0 <= 0 /\ tmp1^0-tmp1^post14 == 0 /\ __const_5^0-__const_5^post14 == 0 /\ tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post14 == 0), cost: 1 15: l2 -> l12 : __const_5^0'=__const_5^post15, WItemsNum^0'=WItemsNum^post15, tmp1^0'=tmp1^post15, (tmp1^0-tmp1^post15 == 0 /\ 1-tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post15 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 16: l2 -> l12 : __const_5^0'=__const_5^post16, WItemsNum^0'=WItemsNum^post16, tmp1^0'=tmp1^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -tmp1^post16+tmp1^0 == 0 /\ 1+tmp1^0 <= 0 /\ -__const_5^post16+__const_5^0 == 0), cost: 1 2: l3 -> l4 : __const_5^0'=__const_5^post2, WItemsNum^0'=WItemsNum^post2, tmp1^0'=tmp1^post2, (tmp1^0-tmp1^post2 == 0 /\ __const_5^0-__const_5^post2 == 0 /\ -WItemsNum^post2+WItemsNum^0 == 0), cost: 1 3: l4 -> l0 : __const_5^0'=__const_5^post3, WItemsNum^0'=WItemsNum^post3, tmp1^0'=tmp1^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ -tmp1^post3+tmp1^0 == 0), cost: 1 4: l5 -> l6 : __const_5^0'=__const_5^post4, WItemsNum^0'=WItemsNum^post4, tmp1^0'=tmp1^post4, (-WItemsNum^post4+WItemsNum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 7: l6 -> l3 : __const_5^0'=__const_5^post7, WItemsNum^0'=WItemsNum^post7, tmp1^0'=tmp1^post7, (-2+WItemsNum^0 <= 0 /\ -tmp1^post7+tmp1^0 == 0 /\ -WItemsNum^post7+WItemsNum^0 == 0 /\ __const_5^0-__const_5^post7 == 0), cost: 1 8: l6 -> l5 : __const_5^0'=__const_5^post8, WItemsNum^0'=WItemsNum^post8, tmp1^0'=tmp1^post8, (1-WItemsNum^0+WItemsNum^post8 == 0 /\ -tmp1^post8+tmp1^0 == 0 /\ __const_5^0-__const_5^post8 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1 5: l7 -> l8 : __const_5^0'=__const_5^post5, WItemsNum^0'=WItemsNum^post5, tmp1^0'=tmp1^post5, (-WItemsNum^post5+WItemsNum^0 == 0 /\ -tmp1^post5+tmp1^0 == 0 /\ -__const_5^post5+__const_5^0 == 0), cost: 1 6: l9 -> l10 : __const_5^0'=__const_5^post6, WItemsNum^0'=WItemsNum^post6, tmp1^0'=tmp1^post6, (-WItemsNum^post6+WItemsNum^0 == 0 /\ __const_5^0-__const_5^post6 == 0 /\ -tmp1^post6+tmp1^0 == 0), cost: 1 9: l10 -> l11 : __const_5^0'=__const_5^post9, WItemsNum^0'=WItemsNum^post9, tmp1^0'=tmp1^post9, (__const_5^0-__const_5^post9 == 0 /\ WItemsNum^0-WItemsNum^post9 == 0 /\ -tmp1^post9+tmp1^0 == 0), cost: 1 10: l11 -> l10 : __const_5^0'=__const_5^post10, WItemsNum^0'=WItemsNum^post10, tmp1^0'=tmp1^post10, (WItemsNum^0-WItemsNum^post10 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -tmp1^post10+tmp1^0 == 0), cost: 1 12: l12 -> l4 : __const_5^0'=__const_5^post12, WItemsNum^0'=WItemsNum^post12, tmp1^0'=tmp1^post12, (-tmp1^post12+tmp1^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post12 == 0), cost: 1 13: l12 -> l4 : __const_5^0'=__const_5^post13, WItemsNum^0'=WItemsNum^post13, tmp1^0'=tmp1^post13, (-1-WItemsNum^0+WItemsNum^post13 == 0 /\ -tmp1^post13+tmp1^0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0), cost: 1 17: l13 -> l3 : __const_5^0'=__const_5^post17, WItemsNum^0'=WItemsNum^post17, tmp1^0'=tmp1^post17, (0 == 0 /\ -tmp1^post17+tmp1^0 == 0 /\ __const_5^0-__const_5^post17 == 0), cost: 1 18: l14 -> l13 : __const_5^0'=__const_5^post18, WItemsNum^0'=WItemsNum^post18, tmp1^0'=tmp1^post18, (-WItemsNum^post18+WItemsNum^0 == 0 /\ -tmp1^post18+tmp1^0 == 0 /\ __const_5^0-__const_5^post18 == 0), cost: 1 Removed unreachable rules and leafs Start location: l14 0: l0 -> l1 : __const_5^0'=__const_5^post0, WItemsNum^0'=WItemsNum^post0, tmp1^0'=tmp1^post0, (1+__const_5^0-WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0 /\ __const_5^0-__const_5^post0 == 0), cost: 1 1: l0 -> l2 : __const_5^0'=__const_5^post1, WItemsNum^0'=WItemsNum^post1, tmp1^0'=tmp1^post1, (0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0), cost: 1 11: l1 -> l5 : __const_5^0'=__const_5^post11, WItemsNum^0'=WItemsNum^post11, tmp1^0'=tmp1^post11, (__const_5^0-__const_5^post11 == 0 /\ WItemsNum^0-WItemsNum^post11 == 0 /\ -tmp1^post11+tmp1^0 == 0), cost: 1 14: l2 -> l1 : __const_5^0'=__const_5^post14, WItemsNum^0'=WItemsNum^post14, tmp1^0'=tmp1^post14, (-tmp1^0 <= 0 /\ tmp1^0-tmp1^post14 == 0 /\ __const_5^0-__const_5^post14 == 0 /\ tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post14 == 0), cost: 1 15: l2 -> l12 : __const_5^0'=__const_5^post15, WItemsNum^0'=WItemsNum^post15, tmp1^0'=tmp1^post15, (tmp1^0-tmp1^post15 == 0 /\ 1-tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post15 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 16: l2 -> l12 : __const_5^0'=__const_5^post16, WItemsNum^0'=WItemsNum^post16, tmp1^0'=tmp1^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -tmp1^post16+tmp1^0 == 0 /\ 1+tmp1^0 <= 0 /\ -__const_5^post16+__const_5^0 == 0), cost: 1 2: l3 -> l4 : __const_5^0'=__const_5^post2, WItemsNum^0'=WItemsNum^post2, tmp1^0'=tmp1^post2, (tmp1^0-tmp1^post2 == 0 /\ __const_5^0-__const_5^post2 == 0 /\ -WItemsNum^post2+WItemsNum^0 == 0), cost: 1 3: l4 -> l0 : __const_5^0'=__const_5^post3, WItemsNum^0'=WItemsNum^post3, tmp1^0'=tmp1^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ -tmp1^post3+tmp1^0 == 0), cost: 1 4: l5 -> l6 : __const_5^0'=__const_5^post4, WItemsNum^0'=WItemsNum^post4, tmp1^0'=tmp1^post4, (-WItemsNum^post4+WItemsNum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 7: l6 -> l3 : __const_5^0'=__const_5^post7, WItemsNum^0'=WItemsNum^post7, tmp1^0'=tmp1^post7, (-2+WItemsNum^0 <= 0 /\ -tmp1^post7+tmp1^0 == 0 /\ -WItemsNum^post7+WItemsNum^0 == 0 /\ __const_5^0-__const_5^post7 == 0), cost: 1 8: l6 -> l5 : __const_5^0'=__const_5^post8, WItemsNum^0'=WItemsNum^post8, tmp1^0'=tmp1^post8, (1-WItemsNum^0+WItemsNum^post8 == 0 /\ -tmp1^post8+tmp1^0 == 0 /\ __const_5^0-__const_5^post8 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1 12: l12 -> l4 : __const_5^0'=__const_5^post12, WItemsNum^0'=WItemsNum^post12, tmp1^0'=tmp1^post12, (-tmp1^post12+tmp1^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post12 == 0), cost: 1 13: l12 -> l4 : __const_5^0'=__const_5^post13, WItemsNum^0'=WItemsNum^post13, tmp1^0'=tmp1^post13, (-1-WItemsNum^0+WItemsNum^post13 == 0 /\ -tmp1^post13+tmp1^0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0), cost: 1 17: l13 -> l3 : __const_5^0'=__const_5^post17, WItemsNum^0'=WItemsNum^post17, tmp1^0'=tmp1^post17, (0 == 0 /\ -tmp1^post17+tmp1^0 == 0 /\ __const_5^0-__const_5^post17 == 0), cost: 1 18: l14 -> l13 : __const_5^0'=__const_5^post18, WItemsNum^0'=WItemsNum^post18, tmp1^0'=tmp1^post18, (-WItemsNum^post18+WItemsNum^0 == 0 /\ -tmp1^post18+tmp1^0 == 0 /\ __const_5^0-__const_5^post18 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : __const_5^0'=__const_5^post0, WItemsNum^0'=WItemsNum^post0, tmp1^0'=tmp1^post0, (1+__const_5^0-WItemsNum^0 <= 0 /\ tmp1^0-tmp1^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0 /\ __const_5^0-__const_5^post0 == 0), cost: 1 New rule: l0 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 Applied preprocessing Original rule: l0 -> l2 : __const_5^0'=__const_5^post1, WItemsNum^0'=WItemsNum^post1, tmp1^0'=tmp1^post1, (0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0), cost: 1 New rule: l0 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l4 : __const_5^0'=__const_5^post2, WItemsNum^0'=WItemsNum^post2, tmp1^0'=tmp1^post2, (tmp1^0-tmp1^post2 == 0 /\ __const_5^0-__const_5^post2 == 0 /\ -WItemsNum^post2+WItemsNum^0 == 0), cost: 1 New rule: l3 -> l4 : TRUE, cost: 1 Applied preprocessing Original rule: l4 -> l0 : __const_5^0'=__const_5^post3, WItemsNum^0'=WItemsNum^post3, tmp1^0'=tmp1^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__const_5^post3+__const_5^0 == 0 /\ -tmp1^post3+tmp1^0 == 0), cost: 1 New rule: l4 -> l0 : TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l6 : __const_5^0'=__const_5^post4, WItemsNum^0'=WItemsNum^post4, tmp1^0'=tmp1^post4, (-WItemsNum^post4+WItemsNum^0 == 0 /\ -tmp1^post4+tmp1^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1 New rule: l5 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l6 -> l3 : __const_5^0'=__const_5^post7, WItemsNum^0'=WItemsNum^post7, tmp1^0'=tmp1^post7, (-2+WItemsNum^0 <= 0 /\ -tmp1^post7+tmp1^0 == 0 /\ -WItemsNum^post7+WItemsNum^0 == 0 /\ __const_5^0-__const_5^post7 == 0), cost: 1 New rule: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l5 : __const_5^0'=__const_5^post8, WItemsNum^0'=WItemsNum^post8, tmp1^0'=tmp1^post8, (1-WItemsNum^0+WItemsNum^post8 == 0 /\ -tmp1^post8+tmp1^0 == 0 /\ __const_5^0-__const_5^post8 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1 New rule: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1 Applied preprocessing Original rule: l1 -> l5 : __const_5^0'=__const_5^post11, WItemsNum^0'=WItemsNum^post11, tmp1^0'=tmp1^post11, (__const_5^0-__const_5^post11 == 0 /\ WItemsNum^0-WItemsNum^post11 == 0 /\ -tmp1^post11+tmp1^0 == 0), cost: 1 New rule: l1 -> l5 : TRUE, cost: 1 Applied preprocessing Original rule: l12 -> l4 : __const_5^0'=__const_5^post12, WItemsNum^0'=WItemsNum^post12, tmp1^0'=tmp1^post12, (-tmp1^post12+tmp1^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post12 == 0), cost: 1 New rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l4 : __const_5^0'=__const_5^post13, WItemsNum^0'=WItemsNum^post13, tmp1^0'=tmp1^post13, (-1-WItemsNum^0+WItemsNum^post13 == 0 /\ -tmp1^post13+tmp1^0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0), cost: 1 New rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1 Applied preprocessing Original rule: l2 -> l1 : __const_5^0'=__const_5^post14, WItemsNum^0'=WItemsNum^post14, tmp1^0'=tmp1^post14, (-tmp1^0 <= 0 /\ tmp1^0-tmp1^post14 == 0 /\ __const_5^0-__const_5^post14 == 0 /\ tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post14 == 0), cost: 1 New rule: l2 -> l1 : tmp1^0 == 0, cost: 1 Applied preprocessing Original rule: l2 -> l12 : __const_5^0'=__const_5^post15, WItemsNum^0'=WItemsNum^post15, tmp1^0'=tmp1^post15, (tmp1^0-tmp1^post15 == 0 /\ 1-tmp1^0 <= 0 /\ WItemsNum^0-WItemsNum^post15 == 0 /\ __const_5^0-__const_5^post15 == 0), cost: 1 New rule: l2 -> l12 : -1+tmp1^0 >= 0, cost: 1 Applied preprocessing Original rule: l2 -> l12 : __const_5^0'=__const_5^post16, WItemsNum^0'=WItemsNum^post16, tmp1^0'=tmp1^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -tmp1^post16+tmp1^0 == 0 /\ 1+tmp1^0 <= 0 /\ -__const_5^post16+__const_5^0 == 0), cost: 1 New rule: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1 Applied preprocessing Original rule: l13 -> l3 : __const_5^0'=__const_5^post17, WItemsNum^0'=WItemsNum^post17, tmp1^0'=tmp1^post17, (0 == 0 /\ -tmp1^post17+tmp1^0 == 0 /\ __const_5^0-__const_5^post17 == 0), cost: 1 New rule: l13 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 1 Applied preprocessing Original rule: l14 -> l13 : __const_5^0'=__const_5^post18, WItemsNum^0'=WItemsNum^post18, tmp1^0'=tmp1^post18, (-WItemsNum^post18+WItemsNum^0 == 0 /\ -tmp1^post18+tmp1^0 == 0 /\ __const_5^0-__const_5^post18 == 0), cost: 1 New rule: l14 -> l13 : TRUE, cost: 1 Simplified rules Start location: l14 19: l0 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 20: l0 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 1 26: l1 -> l5 : TRUE, cost: 1 29: l2 -> l1 : tmp1^0 == 0, cost: 1 30: l2 -> l12 : -1+tmp1^0 >= 0, cost: 1 31: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1 21: l3 -> l4 : TRUE, cost: 1 22: l4 -> l0 : TRUE, cost: 1 23: l5 -> l6 : TRUE, cost: 1 24: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1 25: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1 27: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 28: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1 32: l13 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 1 33: l14 -> l13 : TRUE, cost: 1 Eliminating location l13 by chaining: Applied chaining First rule: l14 -> l13 : TRUE, cost: 1 Second rule: l13 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 1 New rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied deletion Removed the following rules: 32 33 Eliminated locations on linear paths Start location: l14 19: l0 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 20: l0 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 1 26: l1 -> l5 : TRUE, cost: 1 29: l2 -> l1 : tmp1^0 == 0, cost: 1 30: l2 -> l12 : -1+tmp1^0 >= 0, cost: 1 31: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1 21: l3 -> l4 : TRUE, cost: 1 22: l4 -> l0 : TRUE, cost: 1 23: l5 -> l6 : TRUE, cost: 1 24: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1 25: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1 27: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 28: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Eliminating location l0 by chaining: Applied chaining First rule: l4 -> l0 : TRUE, cost: 1 Second rule: l0 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 New rule: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 Applied chaining First rule: l4 -> l0 : TRUE, cost: 1 Second rule: l0 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 1 New rule: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 Applied deletion Removed the following rules: 19 20 22 Eliminating location l6 by chaining: Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> l3 : -2+WItemsNum^0 <= 0, cost: 1 New rule: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1 New rule: l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2 Applied deletion Removed the following rules: 23 24 25 Eliminating location l12 by chaining: Applied chaining First rule: l2 -> l12 : -1+tmp1^0 >= 0, cost: 1 Second rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 New rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1+tmp1^0 >= 0), cost: 2 Applied chaining First rule: l2 -> l12 : -1+tmp1^0 >= 0, cost: 1 Second rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1 New rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-1+tmp1^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2 Applied chaining First rule: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1 Second rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1 New rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 Applied chaining First rule: l2 -> l12 : 1+tmp1^0 <= 0, cost: 1 Second rule: l12 -> l4 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1 New rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 Applied deletion Removed the following rules: 27 28 30 31 Eliminated locations on tree-shaped paths Start location: l14 26: l1 -> l5 : TRUE, cost: 1 29: l2 -> l1 : tmp1^0 == 0, cost: 1 39: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1+tmp1^0 >= 0), cost: 2 40: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-1+tmp1^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2 41: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 42: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 21: l3 -> l4 : TRUE, cost: 1 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 36: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 37: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 38: l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied acceleration Original rule: l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2 New rule: l5 -> l5 : WItemsNum^0'=WItemsNum^0-n, (-2+WItemsNum^0-n >= 0 /\ n >= 0), cost: 2*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_ocJgcc.txt Applied instantiation Original rule: l5 -> l5 : WItemsNum^0'=WItemsNum^0-n, (-2+WItemsNum^0-n >= 0 /\ n >= 0), cost: 2*n New rule: l5 -> l5 : WItemsNum^0'=2, (0 >= 0 /\ -2+WItemsNum^0 >= 0), cost: -4+2*WItemsNum^0 Applied simplification Original rule: l5 -> l5 : WItemsNum^0'=2, (0 >= 0 /\ -2+WItemsNum^0 >= 0), cost: -4+2*WItemsNum^0 New rule: l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0 Applied deletion Removed the following rules: 38 Accelerated simple loops Start location: l14 26: l1 -> l5 : TRUE, cost: 1 29: l2 -> l1 : tmp1^0 == 0, cost: 1 39: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1+tmp1^0 >= 0), cost: 2 40: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-1+tmp1^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2 41: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 42: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 21: l3 -> l4 : TRUE, cost: 1 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 36: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 37: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 44: l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied chaining First rule: l1 -> l5 : TRUE, cost: 1 Second rule: l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0 New rule: l1 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -3+2*WItemsNum^0 Applied deletion Removed the following rules: 44 Chained accelerated rules with incoming rules Start location: l14 26: l1 -> l5 : TRUE, cost: 1 45: l1 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -3+2*WItemsNum^0 29: l2 -> l1 : tmp1^0 == 0, cost: 1 39: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1+tmp1^0 >= 0), cost: 2 40: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-1+tmp1^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2 41: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (1+__const_5^0-WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 42: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 21: l3 -> l4 : TRUE, cost: 1 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 36: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 37: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Eliminating location l2 by chaining: Applied chaining First rule: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 Second rule: l2 -> l1 : tmp1^0 == 0, cost: 1 New rule: l4 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3 Applied chaining First rule: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 Second rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-1+tmp1^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2 New rule: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 4 Applied chaining First rule: l4 -> l2 : tmp1^0'=tmp1^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2 Second rule: l2 -> l4 : WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^0 <= 0), cost: 2 New rule: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^post1 <= 0), cost: 4 Applied deletion Removed the following rules: 29 36 39 40 41 42 Eliminating location l5 by chaining: Applied chaining First rule: l1 -> l5 : TRUE, cost: 1 Second rule: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 New rule: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 Applied chaining First rule: l1 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -3+2*WItemsNum^0 Second rule: l5 -> l3 : -2+WItemsNum^0 <= 0, cost: 2 New rule: l1 -> l3 : WItemsNum^0'=2, (0 <= 0 /\ -2+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0 Applied simplification Original rule: l1 -> l3 : WItemsNum^0'=2, (0 <= 0 /\ -2+WItemsNum^0 >= 0), cost: -1+2*WItemsNum^0 New rule: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 Applied deletion Removed the following rules: 26 37 45 Eliminated locations on tree-shaped paths Start location: l14 49: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 50: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 21: l3 -> l4 : TRUE, cost: 1 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 46: l4 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3 47: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 4 48: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^post1 <= 0), cost: 4 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied acceleration Original rule: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 4 New rule: l4 -> l4 : WItemsNum^0'=WItemsNum^0+n0, tmp1^0'=tmp1^post1, (-1+n0 >= 0 /\ -1+tmp1^post1 >= 0 /\ 1+__const_5^0-WItemsNum^0-n0 >= 0), cost: 4*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_PAbdpD.txt Applied instantiation Original rule: l4 -> l4 : WItemsNum^0'=WItemsNum^0+n0, tmp1^0'=tmp1^post1, (-1+n0 >= 0 /\ -1+tmp1^post1 >= 0 /\ 1+__const_5^0-WItemsNum^0-n0 >= 0), cost: 4*n0 New rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 Applied acceleration Original rule: l4 -> l4 : WItemsNum^0'=1+WItemsNum^0, tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ 1+tmp1^post1 <= 0), cost: 4 New rule: l4 -> l4 : WItemsNum^0'=n1+WItemsNum^0, tmp1^0'=tmp1^post1, (1+__const_5^0-n1-WItemsNum^0 >= 0 /\ -1+n1 >= 0 /\ -1-tmp1^post1 >= 0), cost: 4*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_OcbiCC.txt Applied instantiation Original rule: l4 -> l4 : WItemsNum^0'=n1+WItemsNum^0, tmp1^0'=tmp1^post1, (1+__const_5^0-n1-WItemsNum^0 >= 0 /\ -1+n1 >= 0 /\ -1-tmp1^post1 >= 0), cost: 4*n1 New rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1-tmp1^post1 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 Applied simplification Original rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 New rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 Applied simplification Original rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1-tmp1^post1 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 New rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 Applied deletion Removed the following rules: 47 48 Accelerated simple loops Start location: l14 49: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 50: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 21: l3 -> l4 : TRUE, cost: 1 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 46: l4 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3 53: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 54: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied chaining First rule: l3 -> l4 : TRUE, cost: 1 Second rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Applied chaining First rule: l3 -> l4 : TRUE, cost: 1 Second rule: l4 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Applied deletion Removed the following rules: 53 54 Chained accelerated rules with incoming rules Start location: l14 49: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 50: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 21: l3 -> l4 : TRUE, cost: 1 55: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 56: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 35: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 46: l4 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Eliminating location l4 by chaining: Applied chaining First rule: l3 -> l4 : TRUE, cost: 1 Second rule: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 New rule: l3 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 3 Applied chaining First rule: l3 -> l4 : TRUE, cost: 1 Second rule: l4 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3 New rule: l3 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 4 Applied chaining First rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Second rule: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 New rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 <= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Applied simplification Original rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 <= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Applied chaining First rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Second rule: l4 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 2 New rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 <= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Applied simplification Original rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (0 <= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Applied partial deletion Original rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> [17] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Applied partial deletion Original rule: l3 -> l4 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 New rule: l3 -> [17] : (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 Applied deletion Removed the following rules: 21 35 46 55 56 Eliminated locations on tree-shaped paths Start location: l14 49: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 50: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 57: l3 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 3 58: l3 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 4 59: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 60: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 61: l3 -> [17] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 62: l3 -> [17] : (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied pruning (of leafs and parallel rules): Start location: l14 49: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 50: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 57: l3 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 3 58: l3 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 4 59: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 60: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Eliminating location l1 by chaining: Applied chaining First rule: l3 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 3 Second rule: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 New rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 Applied chaining First rule: l3 -> l1 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 3 Second rule: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 Applied chaining First rule: l3 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 4 Second rule: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 New rule: l3 -> l3 : tmp1^0'=tmp1^post1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 7 Applied chaining First rule: l3 -> l1 : tmp1^0'=tmp1^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 4 Second rule: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3+2*WItemsNum^0 Applied chaining First rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Second rule: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 New rule: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 Applied chaining First rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Second rule: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 Applied chaining First rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Second rule: l1 -> l3 : -2+WItemsNum^0 <= 0, cost: 3 New rule: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ 1+tmp1^post1 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 Applied chaining First rule: l3 -> l1 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 7+4*__const_5^0-4*WItemsNum^0 Second rule: l1 -> l3 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -1+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 Applied deletion Removed the following rules: 49 50 57 58 59 60 Eliminated locations on tree-shaped paths Start location: l14 63: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 64: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 65: l3 -> l3 : tmp1^0'=tmp1^post1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 7 66: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3+2*WItemsNum^0 67: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 68: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 69: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ 1+tmp1^post1 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 70: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0 /\ 1+tmp1^post1 <= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied pruning (of leafs and parallel rules): Start location: l14 63: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 64: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 66: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3+2*WItemsNum^0 67: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 68: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied simplification Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ tmp1^post1 == 0), cost: 3+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 Simplified simple loops Start location: l14 63: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 64: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 67: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 68: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 71: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied nonterm Original rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 New rule: l3 -> [18] : (2-WItemsNum^0 >= 0 /\ n2 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_bEPdjm.txt Applied acceleration Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: 6*n3 Sub-proof via acceration calculus written to file:///tmp/tmpnam_mkLCee.txt Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_dklCee.txt Applied acceleration Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_PHFgBI.txt Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 New rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+__const_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_pBGdCO.txt Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_AOIkdd.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 Second rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+6*__const_5^0+2*WItemsNum^0 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+6*__const_5^0+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_MdENgJ.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM New rule: l3 -> [18] : (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0), cost: 8+6*__const_5^0-4*WItemsNum^0 Second rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0), cost: 15+6*__const_5^0-4*WItemsNum^0 Applied acceleration Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0), cost: 15+6*__const_5^0-4*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n8 >= 0), cost: 6*__const_5^0*n8+7*n8 Sub-proof via acceration calculus written to file:///tmp/tmpnam_dghjfP.txt Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0), cost: 15+6*__const_5^0-4*WItemsNum^0 New rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_FkpcMo.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 Second rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM New rule: l3 -> [18] : (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 Second rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 8+2*WItemsNum^0 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 8+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ 1-__const_5^0 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_HniCob.txt Applied chaining First rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ 1-__const_5^0 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ -1+n15 >= 0 /\ 1-__const_5^0 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 Second rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 8+2*WItemsNum^0 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 8+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_edGCeK.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2+2*WItemsNum^0 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM New rule: l3 -> [18] : (0 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ 1-__const_5^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 Second rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: 3+6*n5*__const_5^0+2*WItemsNum^0 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: 3+6*n5*__const_5^0+2*WItemsNum^0 New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_BcMgmg.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [18] : (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 Second rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 7+6*n5*__const_5^0 Applied acceleration Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 7+6*n5*__const_5^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n18 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0*n18+7*n18 Sub-proof via acceration calculus written to file:///tmp/tmpnam_boGpJN.txt Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 7+6*n5*__const_5^0 New rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_GaJoEa.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=0, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 3+2*WItemsNum^0 Second rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [18] : (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 Second rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: 6*n3 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 == 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6+6*n3 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 == 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6+6*n3 New rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_NOEFkJ.txt Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: 6*n3 Second rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (0 >= 0 /\ -1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: 6*n3 Second rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6+6*n3 Applied nonterm Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6+6*n3 New rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_bJnlGl.txt Applied chaining First rule: l3 -> l3 : (-2+WItemsNum^0 <= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 6 Second rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (2-WItemsNum^0 >= 0 /\ n2 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ n2 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: 6*n3 New rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6*n3 Applied simplification Original rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 New rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 Applied simplification Original rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+__const_5^0 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM New rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ 1-__const_5^0 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ -1+n15 >= 0 /\ 1-__const_5^0 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ 1-__const_5^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n16 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (0 >= 0 /\ -1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM Applied simplification Original rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ 1+__const_5^0-WItemsNum^0 <= 0 /\ 1-__const_5^0 >= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM Applied deletion Removed the following rules: 63 64 68 71 Accelerated simple loops Start location: l14 67: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 74: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM 77: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM 78: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM 86: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM 94: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ n2 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM 95: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6*n3 96: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 97: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM 98: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM 99: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM 100: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: NONTERM 101: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM 102: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM 103: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM 104: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n16 >= 0), cost: NONTERM 105: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM 106: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM 107: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM 108: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM 109: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM 110: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM 111: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0), cost: 10+4*__const_5^0-4*WItemsNum^0 New rule: l14 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -1+__const_5^0 <= 0 /\ __const_5^0-WItemsNum^post17 >= 0), cost: 12+4*__const_5^0-4*WItemsNum^post17 Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ n2 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> l3 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 6*n3 New rule: l14 -> l3 : WItemsNum^0'=2, (-1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 2+6*n3 Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 6*n5*__const_5^0 New rule: l14 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 2+6*n5*__const_5^0 Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n7 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+n15 >= 0 /\ -1+__const_5^0 <= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0 /\ -1+n16 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n16 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+tmp1^post1 >= 0 /\ -1+n17 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (__const_5^0-WItemsNum^0 >= 0 /\ 2-WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+n22 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied chaining First rule: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 Second rule: l3 -> [18] : (-1+n23 >= 0 /\ -2+WItemsNum^0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: NONTERM New rule: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM Applied deletion Removed the following rules: 67 74 77 78 86 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 Chained accelerated rules with incoming rules Start location: l14 34: l14 -> l3 : WItemsNum^0'=WItemsNum^post17, 0 == 0, cost: 2 112: l14 -> l3 : WItemsNum^0'=1+__const_5^0, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -1+__const_5^0 <= 0 /\ __const_5^0-WItemsNum^post17 >= 0), cost: 12+4*__const_5^0-4*WItemsNum^post17 113: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM 114: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM 115: l14 -> l3 : WItemsNum^0'=2, (-1+__const_5^0 <= 0 /\ -1+n3 >= 0), cost: 2+6*n3 116: l14 -> l3 : WItemsNum^0'=2, tmp1^0'=tmp1^post1, (-1+tmp1^post1 >= 0 /\ -2+__const_5^0 >= 0 /\ -1+n5 >= 0), cost: 2+6*n5*__const_5^0 Removed unreachable locations and irrelevant leafs Start location: l14 113: l14 -> [18] : -1+__const_5^0 <= 0, cost: NONTERM 114: l14 -> [18] : -2+__const_5^0 >= 0, cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 113 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: -1+__const_5^0 <= 0