NO

Initial ITS
Start location: l13
   0: l0 -> l1 : __const_5^0'=__const_5^post0, __rho_2_^0'=__rho_2_^post0, WItemsNum^0'=WItemsNum^post0, __rho_1_^0'=__rho_1_^post0, (__rho_2_^0-__rho_2_^post0 == 0 /\ __const_5^0-__const_5^post0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0), cost: 1
   1: l1 -> l2 : __const_5^0'=__const_5^post1, __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=WItemsNum^post1, __rho_1_^0'=__rho_1_^post1, (0 == 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0), cost: 1
  13: l2 -> l10 : __const_5^0'=__const_5^post13, __rho_2_^0'=__rho_2_^post13, WItemsNum^0'=WItemsNum^post13, __rho_1_^0'=__rho_1_^post13, (1+__const_5^0-WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ WItemsNum^0-WItemsNum^post13 == 0 /\ __rho_2_^0-__rho_2_^post13 == 0), cost: 1
  14: l2 -> l11 : __const_5^0'=__const_5^post14, __rho_2_^0'=__rho_2_^post14, WItemsNum^0'=WItemsNum^post14, __rho_1_^0'=__rho_1_^post14, (WItemsNum^0-WItemsNum^post14 == 0 /\ -__rho_1_^post14+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post14 == 0), cost: 1
   2: l3 -> l4 : __const_5^0'=__const_5^post2, __rho_2_^0'=__rho_2_^post2, WItemsNum^0'=WItemsNum^post2, __rho_1_^0'=__rho_1_^post2, (-__rho_2_^post2+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post2 == 0 /\ -WItemsNum^post2+WItemsNum^0 == 0 /\ -__rho_1_^post2+__rho_1_^0 == 0), cost: 1
   3: l5 -> l6 : __const_5^0'=__const_5^post3, __rho_2_^0'=__rho_2_^post3, WItemsNum^0'=WItemsNum^post3, __rho_1_^0'=__rho_1_^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post3 == 0), cost: 1
   5: l6 -> l5 : __const_5^0'=__const_5^post5, __rho_2_^0'=__rho_2_^post5, WItemsNum^0'=WItemsNum^post5, __rho_1_^0'=__rho_1_^post5, (__rho_2_^0-__rho_2_^post5 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ 1-WItemsNum^0+WItemsNum^post5 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1
   6: l6 -> l0 : __const_5^0'=__const_5^post6, __rho_2_^0'=__rho_2_^post6, WItemsNum^0'=WItemsNum^post6, __rho_1_^0'=__rho_1_^post6, (-2+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -1+WItemsNum^post6 == 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -__rho_1_^post6+__rho_1_^0 == 0), cost: 1
   4: l7 -> l8 : __const_5^0'=__const_5^post4, __rho_2_^0'=__rho_2_^post4, WItemsNum^0'=WItemsNum^post4, __rho_1_^0'=__rho_1_^post4, (-WItemsNum^post4+WItemsNum^0 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ -__const_5^post4+__const_5^0 == 0), cost: 1
   7: l8 -> l9 : __const_5^0'=__const_5^post7, __rho_2_^0'=__rho_2_^post7, WItemsNum^0'=WItemsNum^post7, __rho_1_^0'=__rho_1_^post7, (-__rho_1_^post7+__rho_1_^0 == 0 /\ -WItemsNum^post7+WItemsNum^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post7 == 0), cost: 1
   8: l9 -> l8 : __const_5^0'=__const_5^post8, __rho_2_^0'=__rho_2_^post8, WItemsNum^0'=WItemsNum^post8, __rho_1_^0'=__rho_1_^post8, (__rho_1_^0-__rho_1_^post8 == 0 /\ -WItemsNum^post8+WItemsNum^0 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ __rho_2_^0-__rho_2_^post8 == 0), cost: 1
   9: l10 -> l1 : __const_5^0'=__const_5^post9, __rho_2_^0'=__rho_2_^post9, WItemsNum^0'=WItemsNum^post9, __rho_1_^0'=__rho_1_^post9, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post9 == 0 /\ -__rho_1_^post9+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ __const_5^0-__const_5^post9 == 0), cost: 1
  10: l10 -> l1 : __const_5^0'=__const_5^post10, __rho_2_^0'=__rho_2_^post10, WItemsNum^0'=WItemsNum^post10, __rho_1_^0'=__rho_1_^post10, (__const_5^0-__const_5^post10 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -1-WItemsNum^0+WItemsNum^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0), cost: 1
  11: l11 -> l10 : __const_5^0'=__const_5^post11, __rho_2_^0'=__rho_2_^post11, WItemsNum^0'=WItemsNum^post11, __rho_1_^0'=__rho_1_^post11, (-__rho_2_^post11+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ __rho_2_^0 <= 0 /\ -WItemsNum^post11+WItemsNum^0 == 0 /\ -__rho_1_^post11+__rho_1_^0 == 0), cost: 1
  12: l11 -> l5 : __const_5^0'=__const_5^post12, __rho_2_^0'=__rho_2_^post12, WItemsNum^0'=WItemsNum^post12, __rho_1_^0'=__rho_1_^post12, (-__rho_2_^post12+__rho_2_^0 == 0 /\ 1-__rho_2_^0 <= 0 /\ -WItemsNum^post12+WItemsNum^0 == 0 /\ -__rho_1_^post12+__rho_1_^0 == 0 /\ __const_5^0-__const_5^post12 == 0), cost: 1
  15: l12 -> l0 : __const_5^0'=__const_5^post15, __rho_2_^0'=__rho_2_^post15, WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=__rho_1_^post15, (0 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post15 == 0 /\ -__rho_1_^post15+WItemsNum^post15 == 0), cost: 1
  16: l13 -> l12 : __const_5^0'=__const_5^post16, __rho_2_^0'=__rho_2_^post16, WItemsNum^0'=WItemsNum^post16, __rho_1_^0'=__rho_1_^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -__rho_1_^post16+__rho_1_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post16 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l13
   0: l0 -> l1 : __const_5^0'=__const_5^post0, __rho_2_^0'=__rho_2_^post0, WItemsNum^0'=WItemsNum^post0, __rho_1_^0'=__rho_1_^post0, (__rho_2_^0-__rho_2_^post0 == 0 /\ __const_5^0-__const_5^post0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0), cost: 1
   1: l1 -> l2 : __const_5^0'=__const_5^post1, __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=WItemsNum^post1, __rho_1_^0'=__rho_1_^post1, (0 == 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0), cost: 1
  13: l2 -> l10 : __const_5^0'=__const_5^post13, __rho_2_^0'=__rho_2_^post13, WItemsNum^0'=WItemsNum^post13, __rho_1_^0'=__rho_1_^post13, (1+__const_5^0-WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ WItemsNum^0-WItemsNum^post13 == 0 /\ __rho_2_^0-__rho_2_^post13 == 0), cost: 1
  14: l2 -> l11 : __const_5^0'=__const_5^post14, __rho_2_^0'=__rho_2_^post14, WItemsNum^0'=WItemsNum^post14, __rho_1_^0'=__rho_1_^post14, (WItemsNum^0-WItemsNum^post14 == 0 /\ -__rho_1_^post14+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post14 == 0), cost: 1
   3: l5 -> l6 : __const_5^0'=__const_5^post3, __rho_2_^0'=__rho_2_^post3, WItemsNum^0'=WItemsNum^post3, __rho_1_^0'=__rho_1_^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post3 == 0), cost: 1
   5: l6 -> l5 : __const_5^0'=__const_5^post5, __rho_2_^0'=__rho_2_^post5, WItemsNum^0'=WItemsNum^post5, __rho_1_^0'=__rho_1_^post5, (__rho_2_^0-__rho_2_^post5 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ 1-WItemsNum^0+WItemsNum^post5 == 0 /\ 3-WItemsNum^0 <= 0), cost: 1
   6: l6 -> l0 : __const_5^0'=__const_5^post6, __rho_2_^0'=__rho_2_^post6, WItemsNum^0'=WItemsNum^post6, __rho_1_^0'=__rho_1_^post6, (-2+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -1+WItemsNum^post6 == 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -__rho_1_^post6+__rho_1_^0 == 0), cost: 1
   9: l10 -> l1 : __const_5^0'=__const_5^post9, __rho_2_^0'=__rho_2_^post9, WItemsNum^0'=WItemsNum^post9, __rho_1_^0'=__rho_1_^post9, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post9 == 0 /\ -__rho_1_^post9+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ __const_5^0-__const_5^post9 == 0), cost: 1
  10: l10 -> l1 : __const_5^0'=__const_5^post10, __rho_2_^0'=__rho_2_^post10, WItemsNum^0'=WItemsNum^post10, __rho_1_^0'=__rho_1_^post10, (__const_5^0-__const_5^post10 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -1-WItemsNum^0+WItemsNum^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0), cost: 1
  11: l11 -> l10 : __const_5^0'=__const_5^post11, __rho_2_^0'=__rho_2_^post11, WItemsNum^0'=WItemsNum^post11, __rho_1_^0'=__rho_1_^post11, (-__rho_2_^post11+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ __rho_2_^0 <= 0 /\ -WItemsNum^post11+WItemsNum^0 == 0 /\ -__rho_1_^post11+__rho_1_^0 == 0), cost: 1
  12: l11 -> l5 : __const_5^0'=__const_5^post12, __rho_2_^0'=__rho_2_^post12, WItemsNum^0'=WItemsNum^post12, __rho_1_^0'=__rho_1_^post12, (-__rho_2_^post12+__rho_2_^0 == 0 /\ 1-__rho_2_^0 <= 0 /\ -WItemsNum^post12+WItemsNum^0 == 0 /\ -__rho_1_^post12+__rho_1_^0 == 0 /\ __const_5^0-__const_5^post12 == 0), cost: 1
  15: l12 -> l0 : __const_5^0'=__const_5^post15, __rho_2_^0'=__rho_2_^post15, WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=__rho_1_^post15, (0 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post15 == 0 /\ -__rho_1_^post15+WItemsNum^post15 == 0), cost: 1
  16: l13 -> l12 : __const_5^0'=__const_5^post16, __rho_2_^0'=__rho_2_^post16, WItemsNum^0'=WItemsNum^post16, __rho_1_^0'=__rho_1_^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -__rho_1_^post16+__rho_1_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post16 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : __const_5^0'=__const_5^post0, __rho_2_^0'=__rho_2_^post0, WItemsNum^0'=WItemsNum^post0, __rho_1_^0'=__rho_1_^post0, (__rho_2_^0-__rho_2_^post0 == 0 /\ __const_5^0-__const_5^post0 == 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ WItemsNum^0-WItemsNum^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : __const_5^0'=__const_5^post1, __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=WItemsNum^post1, __rho_1_^0'=__rho_1_^post1, (0 == 0 /\ WItemsNum^0-WItemsNum^post1 == 0 /\ __const_5^0-__const_5^post1 == 0 /\ -__rho_1_^post1+__rho_1_^0 == 0), cost: 1
New rule:
l1 -> l2 : __rho_2_^0'=__rho_2_^post1, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : __const_5^0'=__const_5^post3, __rho_2_^0'=__rho_2_^post3, WItemsNum^0'=WItemsNum^post3, __rho_1_^0'=__rho_1_^post3, (-WItemsNum^post3+WItemsNum^0 == 0 /\ -__rho_1_^post3+__rho_1_^0 == 0 /\ -__rho_2_^post3+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post3 == 0), cost: 1
New rule:
l5 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : __const_5^0'=__const_5^post5, __rho_2_^0'=__rho_2_^post5, WItemsNum^0'=WItemsNum^post5, __rho_1_^0'=__rho_1_^post5, (__rho_2_^0-__rho_2_^post5 == 0 /\ __rho_1_^0-__rho_1_^post5 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ 1-WItemsNum^0+WItemsNum^post5 == 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:
l6 -> l0 : __const_5^0'=__const_5^post6, __rho_2_^0'=__rho_2_^post6, WItemsNum^0'=WItemsNum^post6, __rho_1_^0'=__rho_1_^post6, (-2+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -1+WItemsNum^post6 == 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -__rho_1_^post6+__rho_1_^0 == 0), cost: 1
New rule:
l6 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l1 : __const_5^0'=__const_5^post9, __rho_2_^0'=__rho_2_^post9, WItemsNum^0'=WItemsNum^post9, __rho_1_^0'=__rho_1_^post9, (1+__const_5^0-WItemsNum^0 <= 0 /\ -1-WItemsNum^0+WItemsNum^post9 == 0 /\ -__rho_1_^post9+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ __const_5^0-__const_5^post9 == 0), cost: 1
New rule:
l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l1 : __const_5^0'=__const_5^post10, __rho_2_^0'=__rho_2_^post10, WItemsNum^0'=WItemsNum^post10, __rho_1_^0'=__rho_1_^post10, (__const_5^0-__const_5^post10 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -__rho_1_^post10+__rho_1_^0 == 0 /\ -1-WItemsNum^0+WItemsNum^post10 == 0 /\ __rho_2_^0-__rho_2_^post10 == 0), cost: 1
New rule:
l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : __const_5^0'=__const_5^post11, __rho_2_^0'=__rho_2_^post11, WItemsNum^0'=WItemsNum^post11, __rho_1_^0'=__rho_1_^post11, (-__rho_2_^post11+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ __rho_2_^0 <= 0 /\ -WItemsNum^post11+WItemsNum^0 == 0 /\ -__rho_1_^post11+__rho_1_^0 == 0), cost: 1
New rule:
l11 -> l10 : __rho_2_^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l5 : __const_5^0'=__const_5^post12, __rho_2_^0'=__rho_2_^post12, WItemsNum^0'=WItemsNum^post12, __rho_1_^0'=__rho_1_^post12, (-__rho_2_^post12+__rho_2_^0 == 0 /\ 1-__rho_2_^0 <= 0 /\ -WItemsNum^post12+WItemsNum^0 == 0 /\ -__rho_1_^post12+__rho_1_^0 == 0 /\ __const_5^0-__const_5^post12 == 0), cost: 1
New rule:
l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l10 : __const_5^0'=__const_5^post13, __rho_2_^0'=__rho_2_^post13, WItemsNum^0'=WItemsNum^post13, __rho_1_^0'=__rho_1_^post13, (1+__const_5^0-WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post13 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ WItemsNum^0-WItemsNum^post13 == 0 /\ __rho_2_^0-__rho_2_^post13 == 0), cost: 1
New rule:
l2 -> l10 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l11 : __const_5^0'=__const_5^post14, __rho_2_^0'=__rho_2_^post14, WItemsNum^0'=WItemsNum^post14, __rho_1_^0'=__rho_1_^post14, (WItemsNum^0-WItemsNum^post14 == 0 /\ -__rho_1_^post14+__rho_1_^0 == 0 /\ __rho_2_^0-__rho_2_^post14 == 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ __const_5^0-__const_5^post14 == 0), cost: 1
New rule:
l2 -> l11 : -__const_5^0+WItemsNum^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l0 : __const_5^0'=__const_5^post15, __rho_2_^0'=__rho_2_^post15, WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=__rho_1_^post15, (0 == 0 /\ -__rho_2_^post15+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post15 == 0 /\ -__rho_1_^post15+WItemsNum^post15 == 0), cost: 1
New rule:
l12 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : __const_5^0'=__const_5^post16, __rho_2_^0'=__rho_2_^post16, WItemsNum^0'=WItemsNum^post16, __rho_1_^0'=__rho_1_^post16, (-WItemsNum^post16+WItemsNum^0 == 0 /\ -__rho_1_^post16+__rho_1_^0 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ __const_5^0-__const_5^post16 == 0), cost: 1
New rule:
l13 -> l12 : TRUE, cost: 1

Simplified rules
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  18: l1 -> l2 : __rho_2_^0'=__rho_2_^post1, 0 == 0, cost: 1
  26: l2 -> l10 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  27: l2 -> l11 : -__const_5^0+WItemsNum^0 <= 0, cost: 1
  19: l5 -> l6 : TRUE, cost: 1
  20: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1
  21: l6 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 1
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  24: l11 -> l10 : __rho_2_^0 <= 0, cost: 1
  25: l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
  28: l12 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 1
  29: l13 -> l12 : TRUE, cost: 1


Eliminating location l12 by chaining:

Applied chaining
First rule:
l13 -> l12 : TRUE, cost: 1
Second rule:
l12 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 1
New rule:
l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 28 29

Eliminated locations on linear paths
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  18: l1 -> l2 : __rho_2_^0'=__rho_2_^post1, 0 == 0, cost: 1
  26: l2 -> l10 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  27: l2 -> l11 : -__const_5^0+WItemsNum^0 <= 0, cost: 1
  19: l5 -> l6 : TRUE, cost: 1
  20: l6 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 1
  21: l6 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 1
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  24: l11 -> l10 : __rho_2_^0 <= 0, cost: 1
  25: l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l1 -> l2 : __rho_2_^0'=__rho_2_^post1, 0 == 0, cost: 1
Second rule:
l2 -> l10 : 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
New rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, (0 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2

Applied simplification
Original rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, (0 == 0 /\ 1+__const_5^0-WItemsNum^0 <= 0), cost: 2
New rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2

Applied chaining
First rule:
l1 -> l2 : __rho_2_^0'=__rho_2_^post1, 0 == 0, cost: 1
Second rule:
l2 -> l11 : -__const_5^0+WItemsNum^0 <= 0, cost: 1
New rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, (0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2

Applied simplification
Original rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, (0 == 0 /\ -__const_5^0+WItemsNum^0 <= 0), cost: 2
New rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 18 26 27

Eliminating location l6 by chaining:

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 chaining
First rule:
l5 -> l6 : TRUE, cost: 1
Second rule:
l6 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 1
New rule:
l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 19 20 21

Eliminated locations on tree-shaped paths
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  31: l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2
  32: l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
  33: l5 -> l5 : WItemsNum^0'=-1+WItemsNum^0, -3+WItemsNum^0 >= 0, cost: 2
  34: l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  24: l11 -> l10 : __rho_2_^0 <= 0, cost: 1
  25: l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 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'=-n+WItemsNum^0, (n >= 0 /\ -2-n+WItemsNum^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NELgkD.txt

Applied instantiation
Original rule:
l5 -> l5 : WItemsNum^0'=-n+WItemsNum^0, (n >= 0 /\ -2-n+WItemsNum^0 >= 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: 33

Accelerated simple loops
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  31: l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2
  32: l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
  34: l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
  36: l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  24: l11 -> l10 : __rho_2_^0 <= 0, cost: 1
  25: l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied chaining
First rule:
l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
Second rule:
l5 -> l5 : WItemsNum^0'=2, -2+WItemsNum^0 >= 0, cost: -4+2*WItemsNum^0
New rule:
l11 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__rho_2_^0 >= 0), cost: -3+2*WItemsNum^0

Applied deletion
Removed the following rules: 36

Chained accelerated rules with incoming rules
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  31: l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2
  32: l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
  34: l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  24: l11 -> l10 : __rho_2_^0 <= 0, cost: 1
  25: l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
  37: l11 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__rho_2_^0 >= 0), cost: -3+2*WItemsNum^0
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Eliminating location l11 by chaining:

Applied chaining
First rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
Second rule:
l11 -> l10 : __rho_2_^0 <= 0, cost: 1
New rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 3

Applied chaining
First rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
Second rule:
l11 -> l5 : -1+__rho_2_^0 >= 0, cost: 1
New rule:
l1 -> l5 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 3

Applied chaining
First rule:
l1 -> l11 : __rho_2_^0'=__rho_2_^post1, -__const_5^0+WItemsNum^0 <= 0, cost: 2
Second rule:
l11 -> l5 : WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -1+__rho_2_^0 >= 0), cost: -3+2*WItemsNum^0
New rule:
l1 -> l5 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: -1+2*WItemsNum^0

Applied deletion
Removed the following rules: 24 25 32 37

Eliminated locations on tree-shaped paths
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  31: l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2
  38: l1 -> l10 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 3
  39: l1 -> l5 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 3
  40: l1 -> l5 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: -1+2*WItemsNum^0
  34: l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
  22: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
  23: l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Eliminating location l5 by chaining:

Applied chaining
First rule:
l1 -> l5 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 3
Second rule:
l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
New rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 5

Applied chaining
First rule:
l1 -> l5 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=2, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: -1+2*WItemsNum^0
Second rule:
l5 -> l0 : WItemsNum^0'=1, -2+WItemsNum^0 <= 0, cost: 2
New rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0

Applied simplification
Original rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (0 <= 0 /\ -2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0
New rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0

Applied deletion
Removed the following rules: 34 39 40

Eliminating location l10 by chaining:

Applied chaining
First rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, 1+__const_5^0-WItemsNum^0 <= 0, cost: 2
Second rule:
l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 1
New rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 3

Applied chaining
First rule:
l1 -> l10 : __rho_2_^0'=__rho_2_^post1, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 3
Second rule:
l10 -> l1 : WItemsNum^0'=1+WItemsNum^0, -__const_5^0+WItemsNum^0 <= 0, cost: 1
New rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 4

Applied deletion
Removed the following rules: 22 23 31 38

Eliminated locations on tree-shaped paths
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  41: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 5
  42: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0
  43: l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 3
  44: l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 4
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied nonterm
Original rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, 1+__const_5^0-WItemsNum^0 <= 0, cost: 3
New rule:
l1 -> [15] : (-1+n0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_HpHlmn.txt

Applied acceleration
Original rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+WItemsNum^0, (-__const_5^0+WItemsNum^0 <= 0 /\ __rho_2_^post1 <= 0), cost: 4
New rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=WItemsNum^0+n1, (-1+n1 >= 0 /\ -__rho_2_^post1 >= 0 /\ 1+__const_5^0-WItemsNum^0-n1 >= 0), cost: 4*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NMlamE.txt

Applied instantiation
Original rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=WItemsNum^0+n1, (-1+n1 >= 0 /\ -__rho_2_^post1 >= 0 /\ 1+__const_5^0-WItemsNum^0-n1 >= 0), cost: 4*n1
New rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -__rho_2_^post1 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0

Applied simplification
Original rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (0 >= 0 /\ __const_5^0-WItemsNum^0 >= 0 /\ -__rho_2_^post1 >= 0), cost: 4+4*__const_5^0-4*WItemsNum^0
New rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0

Applied deletion
Removed the following rules: 43 44

Accelerated simple loops
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  41: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 5
  42: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0
  45: l1 -> [15] : (-1+n0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM
  47: l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> [15] : (-1+n0 >= 0 /\ -1-__const_5^0+WItemsNum^0 >= 0), cost: NONTERM
New rule:
l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 4+4*__const_5^0-4*WItemsNum^0
New rule:
l0 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0

Applied deletion
Removed the following rules: 45 47

Chained accelerated rules with incoming rules
Start location: l13
  17: l0 -> l1 : TRUE, cost: 1
  48: l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
  49: l0 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0
  41: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 5
  42: l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 5
New rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 6

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 1+2*WItemsNum^0
New rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 2+2*WItemsNum^0

Applied partial deletion
Original rule:
l0 -> l1 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1+__const_5^0, (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0
New rule:
l0 -> [16] : (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0

Applied deletion
Removed the following rules: 17 41 42 49

Eliminated locations on tree-shaped paths
Start location: l13
  48: l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
  50: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 6
  51: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 2+2*WItemsNum^0
  52: l0 -> [16] : (__const_5^0-WItemsNum^0 >= 0 /\ __rho_2_^post1 <= 0), cost: 5+4*__const_5^0-4*WItemsNum^0
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied pruning (of leafs and parallel rules):
Start location: l13
  48: l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
  50: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 6
  51: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 2+2*WItemsNum^0
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 6
New rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0), cost: 6*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bFJDoi.txt

Applied nonterm
Original rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 <= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 6
New rule:
l0 -> [17] : (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-WItemsNum^0 <= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_DFgIBp.txt

Applied deletion
Removed the following rules: 50

Accelerated simple loops
Start location: l13
  48: l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
  51: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 2+2*WItemsNum^0
  53: l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0), cost: 6*n4
  54: l0 -> [17] : (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-WItemsNum^0 <= 0), cost: NONTERM
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2


Applied chaining
First rule:
l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2
Second rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (-2+WItemsNum^0 >= 0 /\ -__const_5^0+WItemsNum^0 <= 0 /\ -1+__rho_2_^post1 >= 0), cost: 2+2*WItemsNum^0
New rule:
l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 >= 0 /\ -__const_5^0+WItemsNum^post15 <= 0), cost: 4+2*WItemsNum^post15

Applied chaining
First rule:
l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2
Second rule:
l0 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0), cost: 6*n4
New rule:
l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 <= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0 /\ __const_5^0-WItemsNum^post15 >= 0), cost: 2+6*n4

Applied chaining
First rule:
l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2
Second rule:
l0 -> [17] : (__const_5^0-WItemsNum^0 >= 0 /\ -1+__rho_2_^post1 >= 0 /\ 2-WItemsNum^0 >= 0 /\ 1-WItemsNum^0 <= 0), cost: NONTERM
New rule:
l13 -> [17] : -1+__const_5^0 >= 0, cost: NONTERM

Applied deletion
Removed the following rules: 51 53 54

Chained accelerated rules with incoming rules
Start location: l13
  48: l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
  30: l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2
  55: l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 >= 0 /\ -__const_5^0+WItemsNum^post15 <= 0), cost: 4+2*WItemsNum^post15
  56: l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 <= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0 /\ __const_5^0-WItemsNum^post15 >= 0), cost: 2+6*n4
  57: l13 -> [17] : -1+__const_5^0 >= 0, cost: NONTERM


Eliminating location l0 by chaining:

Applied chaining
First rule:
l13 -> l0 : WItemsNum^0'=WItemsNum^post15, __rho_1_^0'=WItemsNum^post15, 0 == 0, cost: 2
Second rule:
l0 -> [15] : -1-__const_5^0+WItemsNum^0 >= 0, cost: NONTERM
New rule:
l13 -> [15] : (0 == 0 /\ -1-__const_5^0+WItemsNum^post15 >= 0), cost: NONTERM

Applied simplification
Original rule:
l13 -> [15] : (0 == 0 /\ -1-__const_5^0+WItemsNum^post15 >= 0), cost: NONTERM
New rule:
l13 -> [15] : -1-__const_5^0+WItemsNum^post15 >= 0, cost: NONTERM

Applied partial deletion
Original rule:
l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 >= 0 /\ -__const_5^0+WItemsNum^post15 <= 0), cost: 4+2*WItemsNum^post15
New rule:
l13 -> [18] : (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 >= 0 /\ -__const_5^0+WItemsNum^post15 <= 0), cost: 4+2*WItemsNum^post15

Applied partial deletion
Original rule:
l13 -> l0 : __rho_2_^0'=__rho_2_^post1, WItemsNum^0'=1, __rho_1_^0'=WItemsNum^post15, (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 <= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0 /\ __const_5^0-WItemsNum^post15 >= 0), cost: 2+6*n4
New rule:
l13 -> [18] : (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 <= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0 /\ __const_5^0-WItemsNum^post15 >= 0), cost: 2+6*n4

Applied deletion
Removed the following rules: 30 48 55 56

Eliminated locations on tree-shaped paths
Start location: l13
  57: l13 -> [17] : -1+__const_5^0 >= 0, cost: NONTERM
  58: l13 -> [15] : -1-__const_5^0+WItemsNum^post15 >= 0, cost: NONTERM
  59: l13 -> [18] : (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 >= 0 /\ -__const_5^0+WItemsNum^post15 <= 0), cost: 4+2*WItemsNum^post15
  60: l13 -> [18] : (-1+__rho_2_^post1 >= 0 /\ -2+WItemsNum^post15 <= 0 /\ -1+__const_5^0 >= 0 /\ -1+n4 >= 0 /\ __const_5^0-WItemsNum^post15 >= 0), cost: 2+6*n4


Computing asymptotic complexity
Proved nontermination of rule 57 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