WORST_CASE(Omega(0),?)

Initial ITS
Start location: l23
   0: l0 -> l1 : tmp^0'=tmp^post0, j^0'=j^post0, x^0'=x^post0, n^0'=n^post0, i^0'=i^post0, tmp___0^0'=tmp___0^post0, m^0'=m^post0, y^0'=y^post0, (-y^post0+y^0 == 0 /\ -m^post0+m^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -n^post0+n^0 == 0 /\ x^0-x^post0 == 0 /\ 1-j^0+n^0 <= 0 /\ -j^post0+j^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0), cost: 1
   1: l0 -> l2 : tmp^0'=tmp^post1, j^0'=j^post1, x^0'=x^post1, n^0'=n^post1, i^0'=i^post1, tmp___0^0'=tmp___0^post1, m^0'=m^post1, y^0'=y^post1, (0 == 0 /\ j^0-j^post1 == 0 /\ n^0-n^post1 == 0 /\ -m^post1+m^0 == 0 /\ -y^post1+y^0 == 0 /\ -i^post1+i^0 == 0 /\ j^0-n^0 <= 0 /\ -x^post1+x^0 == 0), cost: 1
  30: l1 -> l15 : tmp^0'=tmp^post30, j^0'=j^post30, x^0'=x^post30, n^0'=n^post30, i^0'=i^post30, tmp___0^0'=tmp___0^post30, m^0'=m^post30, y^0'=y^post30, (-x^post30+x^0 == 0 /\ i^0-m^0 <= 0 /\ i^0-i^post30 == 0 /\ m^0-m^post30 == 0 /\ -i^0+m^0 <= 0 /\ n^0-n^post30 == 0 /\ -y^post30+y^0 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ j^0-j^post30 == 0 /\ tmp^0-tmp^post30 == 0), cost: 1
  31: l1 -> l21 : tmp^0'=tmp^post31, j^0'=j^post31, x^0'=x^post31, n^0'=n^post31, i^0'=i^post31, tmp___0^0'=tmp___0^post31, m^0'=m^post31, y^0'=y^post31, (x^0-x^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ -n^post31+n^0 == 0 /\ 1-i^0+m^0 <= 0 /\ j^0-j^post31 == 0 /\ -i^post31+i^0 == 0 /\ -m^post31+m^0 == 0 /\ tmp^0-tmp^post31 == 0 /\ -y^post31+y^0 == 0), cost: 1
  32: l1 -> l21 : tmp^0'=tmp^post32, j^0'=j^post32, x^0'=x^post32, n^0'=n^post32, i^0'=i^post32, tmp___0^0'=tmp___0^post32, m^0'=m^post32, y^0'=y^post32, (-j^post32+j^0 == 0 /\ i^0-i^post32 == 0 /\ 1+i^0-m^0 <= 0 /\ -y^post32+y^0 == 0 /\ -m^post32+m^0 == 0 /\ tmp^0-tmp^post32 == 0 /\ x^0-x^post32 == 0 /\ n^0-n^post32 == 0 /\ -tmp___0^post32+tmp___0^0 == 0), cost: 1
  34: l2 -> l22 : tmp^0'=tmp^post34, j^0'=j^post34, x^0'=x^post34, n^0'=n^post34, i^0'=i^post34, tmp___0^0'=tmp___0^post34, m^0'=m^post34, y^0'=y^post34, (i^0-i^post34 == 0 /\ -tmp___0^post34+tmp___0^0 == 0 /\ n^0-n^post34 == 0 /\ j^0-j^post34 == 0 /\ -m^post34+m^0 == 0 /\ tmp^0-tmp^post34 == 0 /\ x^0-x^post34 == 0 /\ -y^post34+y^0 == 0 /\ tmp^0-tmp___0^0 <= 0), cost: 1
  35: l2 -> l22 : tmp^0'=tmp^post35, j^0'=j^post35, x^0'=x^post35, n^0'=n^post35, i^0'=i^post35, tmp___0^0'=tmp___0^post35, m^0'=m^post35, y^0'=y^post35, (0 == 0 /\ -j^0+i^post35 == 0 /\ -n^post35+n^0 == 0 /\ j^0-j^post35 == 0 /\ -y^post35+y^0 == 0 /\ tmp^0-tmp^post35 == 0 /\ -tmp___0^post35+tmp___0^0 == 0 /\ 1-tmp^0+tmp___0^0 <= 0 /\ -m^post35+m^0 == 0), cost: 1
   2: l3 -> l0 : tmp^0'=tmp^post2, j^0'=j^post2, x^0'=x^post2, n^0'=n^post2, i^0'=i^post2, tmp___0^0'=tmp___0^post2, m^0'=m^post2, y^0'=y^post2, (-y^post2+y^0 == 0 /\ x^0-x^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i^0-i^post2 == 0 /\ -j^post2+j^0 == 0 /\ -m^post2+m^0 == 0 /\ n^0-n^post2 == 0), cost: 1
   3: l4 -> l5 : tmp^0'=tmp^post3, j^0'=j^post3, x^0'=x^post3, n^0'=n^post3, i^0'=i^post3, tmp___0^0'=tmp___0^post3, m^0'=m^post3, y^0'=y^post3, (j^0-j^post3 == 0 /\ -x^post3+x^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i^post3+i^0 == 0 /\ -1+m^post3-m^0 == 0 /\ -y^post3+y^0 == 0 /\ n^0-n^post3 == 0), cost: 1
  26: l5 -> l16 : tmp^0'=tmp^post26, j^0'=j^post26, x^0'=x^post26, n^0'=n^post26, i^0'=i^post26, tmp___0^0'=tmp___0^post26, m^0'=m^post26, y^0'=y^post26, (-x^post26+x^0 == 0 /\ i^0-i^post26 == 0 /\ -y^post26+y^0 == 0 /\ n^0-n^post26 == 0 /\ m^0-m^post26 == 0 /\ j^0-j^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ tmp^0-tmp^post26 == 0), cost: 1
   4: l6 -> l7 : tmp^0'=tmp^post4, j^0'=j^post4, x^0'=x^post4, n^0'=n^post4, i^0'=i^post4, tmp___0^0'=tmp___0^post4, m^0'=m^post4, y^0'=y^post4, (tmp^0-tmp^post4 == 0 /\ -1-i^0+i^post4 == 0 /\ -n^post4+n^0 == 0 /\ x^0-x^post4 == 0 /\ -m^post4+m^0 == 0 /\ j^0-j^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -y^post4+y^0 == 0), cost: 1
  17: l7 -> l14 : tmp^0'=tmp^post17, j^0'=j^post17, x^0'=x^post17, n^0'=n^post17, i^0'=i^post17, tmp___0^0'=tmp___0^post17, m^0'=m^post17, y^0'=y^post17, (tmp^0-tmp^post17 == 0 /\ -n^post17+n^0 == 0 /\ x^0-x^post17 == 0 /\ -y^post17+y^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ j^0-j^post17 == 0 /\ i^0-i^post17 == 0 /\ -m^post17+m^0 == 0), cost: 1
   5: l8 -> l6 : tmp^0'=tmp^post5, j^0'=j^post5, x^0'=x^post5, n^0'=n^post5, i^0'=i^post5, tmp___0^0'=tmp___0^post5, m^0'=m^post5, y^0'=y^post5, (-m^post5+m^0 == 0 /\ -y^post5+y^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -i^post5+i^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ n^0-n^post5 == 0 /\ -x^post5+x^0 == 0 /\ 1-j^0+n^0 <= 0 /\ j^0-j^post5 == 0), cost: 1
   6: l8 -> l9 : tmp^0'=tmp^post6, j^0'=j^post6, x^0'=x^post6, n^0'=n^post6, i^0'=i^post6, tmp___0^0'=tmp___0^post6, m^0'=m^post6, y^0'=y^post6, (-1+j^post6-j^0 == 0 /\ -n^post6+n^0 == 0 /\ x^0-x^post6 == 0 /\ -m^post6+m^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -y^post6+y^0 == 0 /\ j^0-n^0 <= 0 /\ i^0-i^post6 == 0), cost: 1
   7: l9 -> l8 : tmp^0'=tmp^post7, j^0'=j^post7, x^0'=x^post7, n^0'=n^post7, i^0'=i^post7, tmp___0^0'=tmp___0^post7, m^0'=m^post7, y^0'=y^post7, (tmp^0-tmp^post7 == 0 /\ i^0-i^post7 == 0 /\ -y^post7+y^0 == 0 /\ m^0-m^post7 == 0 /\ -x^post7+x^0 == 0 /\ n^0-n^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ j^0-j^post7 == 0), cost: 1
   8: l10 -> l9 : tmp^0'=tmp^post8, j^0'=j^post8, x^0'=x^post8, n^0'=n^post8, i^0'=i^post8, tmp___0^0'=tmp___0^post8, m^0'=m^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ x^0-x^post8 == 0 /\ -y^post8+y^0 == 0 /\ -n^post8+n^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ j^0-j^post8 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post8 == 0 /\ -m^post8+m^0 == 0), cost: 1
   9: l10 -> l11 : tmp^0'=tmp^post9, j^0'=j^post9, x^0'=x^post9, n^0'=n^post9, i^0'=i^post9, tmp___0^0'=tmp___0^post9, m^0'=m^post9, y^0'=y^post9, (-x^post9+x^0 == 0 /\ -1-j^0+j^post9 == 0 /\ n^0-n^post9 == 0 /\ m^0-m^post9 == 0 /\ -y^post9+y^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ j^0-n^0 <= 0 /\ -i^post9+i^0 == 0), cost: 1
  10: l11 -> l10 : tmp^0'=tmp^post10, j^0'=j^post10, x^0'=x^post10, n^0'=n^post10, i^0'=i^post10, tmp___0^0'=tmp___0^post10, m^0'=m^post10, y^0'=y^post10, (x^0-x^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -m^post10+m^0 == 0 /\ -y^post10+y^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -n^post10+n^0 == 0 /\ -i^post10+i^0 == 0 /\ j^0-j^post10 == 0), cost: 1
  11: l12 -> l11 : tmp^0'=tmp^post11, j^0'=j^post11, x^0'=x^post11, n^0'=n^post11, i^0'=i^post11, tmp___0^0'=tmp___0^post11, m^0'=m^post11, y^0'=y^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ i^0-i^post11 == 0 /\ -x^post11+x^0 == 0 /\ n^0-n^post11 == 0 /\ j^0-j^post11 == 0 /\ -m^post11+m^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0), cost: 1
  12: l13 -> l6 : tmp^0'=tmp^post12, j^0'=j^post12, x^0'=x^post12, n^0'=n^post12, i^0'=i^post12, tmp___0^0'=tmp___0^post12, m^0'=m^post12, y^0'=y^post12, (j^0-j^post12 == 0 /\ -y^0 <= 0 /\ -i^post12+i^0 == 0 /\ -x^post12+x^0 == 0 /\ -y^post12+y^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ n^0-n^post12 == 0 /\ y^0 <= 0 /\ -m^post12+m^0 == 0), cost: 1
  13: l13 -> l12 : tmp^0'=tmp^post13, j^0'=j^post13, x^0'=x^post13, n^0'=n^post13, i^0'=i^post13, tmp___0^0'=tmp___0^post13, m^0'=m^post13, y^0'=y^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ 1-y^0 <= 0 /\ i^0-i^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -m^post13+m^0 == 0 /\ -n^post13+n^0 == 0 /\ x^0-x^post13 == 0 /\ -j^post13+j^0 == 0 /\ -y^post13+y^0 == 0), cost: 1
  14: l13 -> l12 : tmp^0'=tmp^post14, j^0'=j^post14, x^0'=x^post14, n^0'=n^post14, i^0'=i^post14, tmp___0^0'=tmp___0^post14, m^0'=m^post14, y^0'=y^post14, (j^0-j^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0 /\ -m^post14+m^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ 1+y^0 <= 0 /\ n^0-n^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -i^post14+i^0 == 0), cost: 1
  15: l14 -> l4 : tmp^0'=tmp^post15, j^0'=j^post15, x^0'=x^post15, n^0'=n^post15, i^0'=i^post15, tmp___0^0'=tmp___0^post15, m^0'=m^post15, y^0'=y^post15, (-j^post15+j^0 == 0 /\ -m^post15+m^0 == 0 /\ -y^post15+y^0 == 0 /\ 1+n^0-i^0 <= 0 /\ x^0-x^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ n^0-n^post15 == 0 /\ i^0-i^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
  16: l14 -> l13 : tmp^0'=tmp^post16, j^0'=j^post16, x^0'=x^post16, n^0'=n^post16, i^0'=i^post16, tmp___0^0'=tmp___0^post16, m^0'=m^post16, y^0'=y^post16, (0 == 0 /\ j^0-j^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i^post16+i^0 == 0 /\ -m^post16+m^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -n^0+i^0 <= 0 /\ n^0-n^post16 == 0 /\ -x^post16+x^0 == 0), cost: 1
  18: l15 -> l4 : tmp^0'=tmp^post18, j^0'=j^post18, x^0'=x^post18, n^0'=n^post18, i^0'=i^post18, tmp___0^0'=tmp___0^post18, m^0'=m^post18, y^0'=y^post18, (-y^post18+y^0 == 0 /\ -x^post18+x^0 == 0 /\ j^0-j^post18 == 0 /\ -x^0 <= 0 /\ -m^post18+m^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ x^0 <= 0 /\ -i^post18+i^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ n^0-n^post18 == 0), cost: 1
  19: l15 -> l7 : tmp^0'=tmp^post19, j^0'=j^post19, x^0'=x^post19, n^0'=n^post19, i^0'=i^post19, tmp___0^0'=tmp___0^post19, m^0'=m^post19, y^0'=y^post19, (1-x^0 <= 0 /\ x^0-x^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ -n^post19+n^0 == 0 /\ -y^post19+y^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -j^post19+j^0 == 0 /\ -m^post19+m^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
  20: l15 -> l7 : tmp^0'=tmp^post20, j^0'=j^post20, x^0'=x^post20, n^0'=n^post20, i^0'=i^post20, tmp___0^0'=tmp___0^post20, m^0'=m^post20, y^0'=y^post20, (tmp^0-tmp^post20 == 0 /\ n^0-n^post20 == 0 /\ m^0-m^post20 == 0 /\ -x^post20+x^0 == 0 /\ -y^post20+y^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -i^post20+i^0 == 0 /\ j^0-j^post20 == 0 /\ 1+x^0 <= 0), cost: 1
  21: l16 -> l17 : tmp^0'=tmp^post21, j^0'=j^post21, x^0'=x^post21, n^0'=n^post21, i^0'=i^post21, tmp___0^0'=tmp___0^post21, m^0'=m^post21, y^0'=y^post21, (tmp^0-tmp^post21 == 0 /\ x^0-x^post21 == 0 /\ -m^post21+m^0 == 0 /\ i^0-i^post21 == 0 /\ j^0-j^post21 == 0 /\ -n^post21+n^0 == 0 /\ n^0-m^0 <= 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -y^post21+y^0 == 0), cost: 1
  22: l16 -> l3 : tmp^0'=tmp^post22, j^0'=j^post22, x^0'=x^post22, n^0'=n^post22, i^0'=i^post22, tmp___0^0'=tmp___0^post22, m^0'=m^post22, y^0'=y^post22, (-tmp___0^post22+tmp___0^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ x^post22 == 0 /\ -m^post22+m^0 == 0 /\ i^post22-m^0 == 0 /\ n^0-n^post22 == 0 /\ j^0-j^post22 == 0 /\ 1-n^0+m^0 <= 0 /\ -y^post22+y^0 == 0), cost: 1
  23: l18 -> l15 : tmp^0'=tmp^post23, j^0'=j^post23, x^0'=x^post23, n^0'=n^post23, i^0'=i^post23, tmp___0^0'=tmp___0^post23, m^0'=m^post23, y^0'=y^post23, (-y^post23+y^0 == 0 /\ -m^post23+m^0 == 0 /\ tmp^0-tmp^post23 == 0 /\ x^0-x^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -i^post23+i^0 == 0 /\ 1-j^0+n^0 <= 0 /\ -n^post23+n^0 == 0 /\ j^0-j^post23 == 0), cost: 1
  24: l18 -> l19 : tmp^0'=tmp^post24, j^0'=j^post24, x^0'=x^post24, n^0'=n^post24, i^0'=i^post24, tmp___0^0'=tmp___0^post24, m^0'=m^post24, y^0'=y^post24, (0 == 0 /\ m^0-m^post24 == 0 /\ n^0-n^post24 == 0 /\ -1-j^0+j^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ i^0-i^post24 == 0 /\ j^0-n^0 <= 0 /\ x^0-x^post24 == 0 /\ tmp^0-tmp^post24 == 0), cost: 1
  25: l19 -> l18 : tmp^0'=tmp^post25, j^0'=j^post25, x^0'=x^post25, n^0'=n^post25, i^0'=i^post25, tmp___0^0'=tmp___0^post25, m^0'=m^post25, y^0'=y^post25, (-i^post25+i^0 == 0 /\ -n^post25+n^0 == 0 /\ -y^post25+y^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ j^0-j^post25 == 0 /\ x^0-x^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ -m^post25+m^0 == 0), cost: 1
  27: l20 -> l19 : tmp^0'=tmp^post27, j^0'=j^post27, x^0'=x^post27, n^0'=n^post27, i^0'=i^post27, tmp___0^0'=tmp___0^post27, m^0'=m^post27, y^0'=y^post27, (x^0-x^post27 == 0 /\ -y^post27+y^0 == 0 /\ -m^post27+m^0 == 0 /\ -i^post27+i^0 == 0 /\ tmp___0^0-tmp___0^post27 == 0 /\ j^0-j^post27 == 0 /\ -n^post27+n^0 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post27 == 0), cost: 1
  28: l20 -> l21 : tmp^0'=tmp^post28, j^0'=j^post28, x^0'=x^post28, n^0'=n^post28, i^0'=i^post28, tmp___0^0'=tmp___0^post28, m^0'=m^post28, y^0'=y^post28, (0 == 0 /\ m^0-m^post28 == 0 /\ n^0-n^post28 == 0 /\ -1-j^0+j^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0 /\ i^0-i^post28 == 0 /\ j^0-n^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ x^0-x^post28 == 0), cost: 1
  29: l21 -> l20 : tmp^0'=tmp^post29, j^0'=j^post29, x^0'=x^post29, n^0'=n^post29, i^0'=i^post29, tmp___0^0'=tmp___0^post29, m^0'=m^post29, y^0'=y^post29, (-i^post29+i^0 == 0 /\ -y^post29+y^0 == 0 /\ -n^post29+n^0 == 0 /\ tmp___0^0-tmp___0^post29 == 0 /\ j^0-j^post29 == 0 /\ x^0-x^post29 == 0 /\ tmp^0-tmp^post29 == 0 /\ -m^post29+m^0 == 0), cost: 1
  33: l22 -> l3 : tmp^0'=tmp^post33, j^0'=j^post33, x^0'=x^post33, n^0'=n^post33, i^0'=i^post33, tmp___0^0'=tmp___0^post33, m^0'=m^post33, y^0'=y^post33, (tmp___0^0-tmp___0^post33 == 0 /\ -i^post33+i^0 == 0 /\ -x^post33+x^0 == 0 /\ -m^post33+m^0 == 0 /\ -y^post33+y^0 == 0 /\ -tmp^post33+tmp^0 == 0 /\ n^0-n^post33 == 0 /\ -1-j^0+j^post33 == 0), cost: 1
  36: l23 -> l5 : tmp^0'=tmp^post36, j^0'=j^post36, x^0'=x^post36, n^0'=n^post36, i^0'=i^post36, tmp___0^0'=tmp___0^post36, m^0'=m^post36, y^0'=y^post36, (-y^post36+y^0 == 0 /\ -m^post36+m^0 == 0 /\ tmp^0-tmp^post36 == 0 /\ -n^post36+n^0 == 0 /\ x^0-x^post36 == 0 /\ -j^post36+j^0 == 0 /\ i^0-i^post36 == 0 /\ tmp___0^0-tmp___0^post36 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l23
   0: l0 -> l1 : tmp^0'=tmp^post0, j^0'=j^post0, x^0'=x^post0, n^0'=n^post0, i^0'=i^post0, tmp___0^0'=tmp___0^post0, m^0'=m^post0, y^0'=y^post0, (-y^post0+y^0 == 0 /\ -m^post0+m^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -n^post0+n^0 == 0 /\ x^0-x^post0 == 0 /\ 1-j^0+n^0 <= 0 /\ -j^post0+j^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0), cost: 1
   1: l0 -> l2 : tmp^0'=tmp^post1, j^0'=j^post1, x^0'=x^post1, n^0'=n^post1, i^0'=i^post1, tmp___0^0'=tmp___0^post1, m^0'=m^post1, y^0'=y^post1, (0 == 0 /\ j^0-j^post1 == 0 /\ n^0-n^post1 == 0 /\ -m^post1+m^0 == 0 /\ -y^post1+y^0 == 0 /\ -i^post1+i^0 == 0 /\ j^0-n^0 <= 0 /\ -x^post1+x^0 == 0), cost: 1
  30: l1 -> l15 : tmp^0'=tmp^post30, j^0'=j^post30, x^0'=x^post30, n^0'=n^post30, i^0'=i^post30, tmp___0^0'=tmp___0^post30, m^0'=m^post30, y^0'=y^post30, (-x^post30+x^0 == 0 /\ i^0-m^0 <= 0 /\ i^0-i^post30 == 0 /\ m^0-m^post30 == 0 /\ -i^0+m^0 <= 0 /\ n^0-n^post30 == 0 /\ -y^post30+y^0 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ j^0-j^post30 == 0 /\ tmp^0-tmp^post30 == 0), cost: 1
  31: l1 -> l21 : tmp^0'=tmp^post31, j^0'=j^post31, x^0'=x^post31, n^0'=n^post31, i^0'=i^post31, tmp___0^0'=tmp___0^post31, m^0'=m^post31, y^0'=y^post31, (x^0-x^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ -n^post31+n^0 == 0 /\ 1-i^0+m^0 <= 0 /\ j^0-j^post31 == 0 /\ -i^post31+i^0 == 0 /\ -m^post31+m^0 == 0 /\ tmp^0-tmp^post31 == 0 /\ -y^post31+y^0 == 0), cost: 1
  32: l1 -> l21 : tmp^0'=tmp^post32, j^0'=j^post32, x^0'=x^post32, n^0'=n^post32, i^0'=i^post32, tmp___0^0'=tmp___0^post32, m^0'=m^post32, y^0'=y^post32, (-j^post32+j^0 == 0 /\ i^0-i^post32 == 0 /\ 1+i^0-m^0 <= 0 /\ -y^post32+y^0 == 0 /\ -m^post32+m^0 == 0 /\ tmp^0-tmp^post32 == 0 /\ x^0-x^post32 == 0 /\ n^0-n^post32 == 0 /\ -tmp___0^post32+tmp___0^0 == 0), cost: 1
  34: l2 -> l22 : tmp^0'=tmp^post34, j^0'=j^post34, x^0'=x^post34, n^0'=n^post34, i^0'=i^post34, tmp___0^0'=tmp___0^post34, m^0'=m^post34, y^0'=y^post34, (i^0-i^post34 == 0 /\ -tmp___0^post34+tmp___0^0 == 0 /\ n^0-n^post34 == 0 /\ j^0-j^post34 == 0 /\ -m^post34+m^0 == 0 /\ tmp^0-tmp^post34 == 0 /\ x^0-x^post34 == 0 /\ -y^post34+y^0 == 0 /\ tmp^0-tmp___0^0 <= 0), cost: 1
  35: l2 -> l22 : tmp^0'=tmp^post35, j^0'=j^post35, x^0'=x^post35, n^0'=n^post35, i^0'=i^post35, tmp___0^0'=tmp___0^post35, m^0'=m^post35, y^0'=y^post35, (0 == 0 /\ -j^0+i^post35 == 0 /\ -n^post35+n^0 == 0 /\ j^0-j^post35 == 0 /\ -y^post35+y^0 == 0 /\ tmp^0-tmp^post35 == 0 /\ -tmp___0^post35+tmp___0^0 == 0 /\ 1-tmp^0+tmp___0^0 <= 0 /\ -m^post35+m^0 == 0), cost: 1
   2: l3 -> l0 : tmp^0'=tmp^post2, j^0'=j^post2, x^0'=x^post2, n^0'=n^post2, i^0'=i^post2, tmp___0^0'=tmp___0^post2, m^0'=m^post2, y^0'=y^post2, (-y^post2+y^0 == 0 /\ x^0-x^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i^0-i^post2 == 0 /\ -j^post2+j^0 == 0 /\ -m^post2+m^0 == 0 /\ n^0-n^post2 == 0), cost: 1
   3: l4 -> l5 : tmp^0'=tmp^post3, j^0'=j^post3, x^0'=x^post3, n^0'=n^post3, i^0'=i^post3, tmp___0^0'=tmp___0^post3, m^0'=m^post3, y^0'=y^post3, (j^0-j^post3 == 0 /\ -x^post3+x^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i^post3+i^0 == 0 /\ -1+m^post3-m^0 == 0 /\ -y^post3+y^0 == 0 /\ n^0-n^post3 == 0), cost: 1
  26: l5 -> l16 : tmp^0'=tmp^post26, j^0'=j^post26, x^0'=x^post26, n^0'=n^post26, i^0'=i^post26, tmp___0^0'=tmp___0^post26, m^0'=m^post26, y^0'=y^post26, (-x^post26+x^0 == 0 /\ i^0-i^post26 == 0 /\ -y^post26+y^0 == 0 /\ n^0-n^post26 == 0 /\ m^0-m^post26 == 0 /\ j^0-j^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ tmp^0-tmp^post26 == 0), cost: 1
   4: l6 -> l7 : tmp^0'=tmp^post4, j^0'=j^post4, x^0'=x^post4, n^0'=n^post4, i^0'=i^post4, tmp___0^0'=tmp___0^post4, m^0'=m^post4, y^0'=y^post4, (tmp^0-tmp^post4 == 0 /\ -1-i^0+i^post4 == 0 /\ -n^post4+n^0 == 0 /\ x^0-x^post4 == 0 /\ -m^post4+m^0 == 0 /\ j^0-j^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -y^post4+y^0 == 0), cost: 1
  17: l7 -> l14 : tmp^0'=tmp^post17, j^0'=j^post17, x^0'=x^post17, n^0'=n^post17, i^0'=i^post17, tmp___0^0'=tmp___0^post17, m^0'=m^post17, y^0'=y^post17, (tmp^0-tmp^post17 == 0 /\ -n^post17+n^0 == 0 /\ x^0-x^post17 == 0 /\ -y^post17+y^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ j^0-j^post17 == 0 /\ i^0-i^post17 == 0 /\ -m^post17+m^0 == 0), cost: 1
   5: l8 -> l6 : tmp^0'=tmp^post5, j^0'=j^post5, x^0'=x^post5, n^0'=n^post5, i^0'=i^post5, tmp___0^0'=tmp___0^post5, m^0'=m^post5, y^0'=y^post5, (-m^post5+m^0 == 0 /\ -y^post5+y^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -i^post5+i^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ n^0-n^post5 == 0 /\ -x^post5+x^0 == 0 /\ 1-j^0+n^0 <= 0 /\ j^0-j^post5 == 0), cost: 1
   6: l8 -> l9 : tmp^0'=tmp^post6, j^0'=j^post6, x^0'=x^post6, n^0'=n^post6, i^0'=i^post6, tmp___0^0'=tmp___0^post6, m^0'=m^post6, y^0'=y^post6, (-1+j^post6-j^0 == 0 /\ -n^post6+n^0 == 0 /\ x^0-x^post6 == 0 /\ -m^post6+m^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -y^post6+y^0 == 0 /\ j^0-n^0 <= 0 /\ i^0-i^post6 == 0), cost: 1
   7: l9 -> l8 : tmp^0'=tmp^post7, j^0'=j^post7, x^0'=x^post7, n^0'=n^post7, i^0'=i^post7, tmp___0^0'=tmp___0^post7, m^0'=m^post7, y^0'=y^post7, (tmp^0-tmp^post7 == 0 /\ i^0-i^post7 == 0 /\ -y^post7+y^0 == 0 /\ m^0-m^post7 == 0 /\ -x^post7+x^0 == 0 /\ n^0-n^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ j^0-j^post7 == 0), cost: 1
   8: l10 -> l9 : tmp^0'=tmp^post8, j^0'=j^post8, x^0'=x^post8, n^0'=n^post8, i^0'=i^post8, tmp___0^0'=tmp___0^post8, m^0'=m^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ x^0-x^post8 == 0 /\ -y^post8+y^0 == 0 /\ -n^post8+n^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ j^0-j^post8 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post8 == 0 /\ -m^post8+m^0 == 0), cost: 1
   9: l10 -> l11 : tmp^0'=tmp^post9, j^0'=j^post9, x^0'=x^post9, n^0'=n^post9, i^0'=i^post9, tmp___0^0'=tmp___0^post9, m^0'=m^post9, y^0'=y^post9, (-x^post9+x^0 == 0 /\ -1-j^0+j^post9 == 0 /\ n^0-n^post9 == 0 /\ m^0-m^post9 == 0 /\ -y^post9+y^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ j^0-n^0 <= 0 /\ -i^post9+i^0 == 0), cost: 1
  10: l11 -> l10 : tmp^0'=tmp^post10, j^0'=j^post10, x^0'=x^post10, n^0'=n^post10, i^0'=i^post10, tmp___0^0'=tmp___0^post10, m^0'=m^post10, y^0'=y^post10, (x^0-x^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -m^post10+m^0 == 0 /\ -y^post10+y^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -n^post10+n^0 == 0 /\ -i^post10+i^0 == 0 /\ j^0-j^post10 == 0), cost: 1
  11: l12 -> l11 : tmp^0'=tmp^post11, j^0'=j^post11, x^0'=x^post11, n^0'=n^post11, i^0'=i^post11, tmp___0^0'=tmp___0^post11, m^0'=m^post11, y^0'=y^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ i^0-i^post11 == 0 /\ -x^post11+x^0 == 0 /\ n^0-n^post11 == 0 /\ j^0-j^post11 == 0 /\ -m^post11+m^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0), cost: 1
  12: l13 -> l6 : tmp^0'=tmp^post12, j^0'=j^post12, x^0'=x^post12, n^0'=n^post12, i^0'=i^post12, tmp___0^0'=tmp___0^post12, m^0'=m^post12, y^0'=y^post12, (j^0-j^post12 == 0 /\ -y^0 <= 0 /\ -i^post12+i^0 == 0 /\ -x^post12+x^0 == 0 /\ -y^post12+y^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ n^0-n^post12 == 0 /\ y^0 <= 0 /\ -m^post12+m^0 == 0), cost: 1
  13: l13 -> l12 : tmp^0'=tmp^post13, j^0'=j^post13, x^0'=x^post13, n^0'=n^post13, i^0'=i^post13, tmp___0^0'=tmp___0^post13, m^0'=m^post13, y^0'=y^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ 1-y^0 <= 0 /\ i^0-i^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -m^post13+m^0 == 0 /\ -n^post13+n^0 == 0 /\ x^0-x^post13 == 0 /\ -j^post13+j^0 == 0 /\ -y^post13+y^0 == 0), cost: 1
  14: l13 -> l12 : tmp^0'=tmp^post14, j^0'=j^post14, x^0'=x^post14, n^0'=n^post14, i^0'=i^post14, tmp___0^0'=tmp___0^post14, m^0'=m^post14, y^0'=y^post14, (j^0-j^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0 /\ -m^post14+m^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ 1+y^0 <= 0 /\ n^0-n^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -i^post14+i^0 == 0), cost: 1
  15: l14 -> l4 : tmp^0'=tmp^post15, j^0'=j^post15, x^0'=x^post15, n^0'=n^post15, i^0'=i^post15, tmp___0^0'=tmp___0^post15, m^0'=m^post15, y^0'=y^post15, (-j^post15+j^0 == 0 /\ -m^post15+m^0 == 0 /\ -y^post15+y^0 == 0 /\ 1+n^0-i^0 <= 0 /\ x^0-x^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ n^0-n^post15 == 0 /\ i^0-i^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
  16: l14 -> l13 : tmp^0'=tmp^post16, j^0'=j^post16, x^0'=x^post16, n^0'=n^post16, i^0'=i^post16, tmp___0^0'=tmp___0^post16, m^0'=m^post16, y^0'=y^post16, (0 == 0 /\ j^0-j^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i^post16+i^0 == 0 /\ -m^post16+m^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -n^0+i^0 <= 0 /\ n^0-n^post16 == 0 /\ -x^post16+x^0 == 0), cost: 1
  18: l15 -> l4 : tmp^0'=tmp^post18, j^0'=j^post18, x^0'=x^post18, n^0'=n^post18, i^0'=i^post18, tmp___0^0'=tmp___0^post18, m^0'=m^post18, y^0'=y^post18, (-y^post18+y^0 == 0 /\ -x^post18+x^0 == 0 /\ j^0-j^post18 == 0 /\ -x^0 <= 0 /\ -m^post18+m^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ x^0 <= 0 /\ -i^post18+i^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ n^0-n^post18 == 0), cost: 1
  19: l15 -> l7 : tmp^0'=tmp^post19, j^0'=j^post19, x^0'=x^post19, n^0'=n^post19, i^0'=i^post19, tmp___0^0'=tmp___0^post19, m^0'=m^post19, y^0'=y^post19, (1-x^0 <= 0 /\ x^0-x^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ -n^post19+n^0 == 0 /\ -y^post19+y^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -j^post19+j^0 == 0 /\ -m^post19+m^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
  20: l15 -> l7 : tmp^0'=tmp^post20, j^0'=j^post20, x^0'=x^post20, n^0'=n^post20, i^0'=i^post20, tmp___0^0'=tmp___0^post20, m^0'=m^post20, y^0'=y^post20, (tmp^0-tmp^post20 == 0 /\ n^0-n^post20 == 0 /\ m^0-m^post20 == 0 /\ -x^post20+x^0 == 0 /\ -y^post20+y^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -i^post20+i^0 == 0 /\ j^0-j^post20 == 0 /\ 1+x^0 <= 0), cost: 1
  22: l16 -> l3 : tmp^0'=tmp^post22, j^0'=j^post22, x^0'=x^post22, n^0'=n^post22, i^0'=i^post22, tmp___0^0'=tmp___0^post22, m^0'=m^post22, y^0'=y^post22, (-tmp___0^post22+tmp___0^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ x^post22 == 0 /\ -m^post22+m^0 == 0 /\ i^post22-m^0 == 0 /\ n^0-n^post22 == 0 /\ j^0-j^post22 == 0 /\ 1-n^0+m^0 <= 0 /\ -y^post22+y^0 == 0), cost: 1
  23: l18 -> l15 : tmp^0'=tmp^post23, j^0'=j^post23, x^0'=x^post23, n^0'=n^post23, i^0'=i^post23, tmp___0^0'=tmp___0^post23, m^0'=m^post23, y^0'=y^post23, (-y^post23+y^0 == 0 /\ -m^post23+m^0 == 0 /\ tmp^0-tmp^post23 == 0 /\ x^0-x^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -i^post23+i^0 == 0 /\ 1-j^0+n^0 <= 0 /\ -n^post23+n^0 == 0 /\ j^0-j^post23 == 0), cost: 1
  24: l18 -> l19 : tmp^0'=tmp^post24, j^0'=j^post24, x^0'=x^post24, n^0'=n^post24, i^0'=i^post24, tmp___0^0'=tmp___0^post24, m^0'=m^post24, y^0'=y^post24, (0 == 0 /\ m^0-m^post24 == 0 /\ n^0-n^post24 == 0 /\ -1-j^0+j^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ i^0-i^post24 == 0 /\ j^0-n^0 <= 0 /\ x^0-x^post24 == 0 /\ tmp^0-tmp^post24 == 0), cost: 1
  25: l19 -> l18 : tmp^0'=tmp^post25, j^0'=j^post25, x^0'=x^post25, n^0'=n^post25, i^0'=i^post25, tmp___0^0'=tmp___0^post25, m^0'=m^post25, y^0'=y^post25, (-i^post25+i^0 == 0 /\ -n^post25+n^0 == 0 /\ -y^post25+y^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ j^0-j^post25 == 0 /\ x^0-x^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ -m^post25+m^0 == 0), cost: 1
  27: l20 -> l19 : tmp^0'=tmp^post27, j^0'=j^post27, x^0'=x^post27, n^0'=n^post27, i^0'=i^post27, tmp___0^0'=tmp___0^post27, m^0'=m^post27, y^0'=y^post27, (x^0-x^post27 == 0 /\ -y^post27+y^0 == 0 /\ -m^post27+m^0 == 0 /\ -i^post27+i^0 == 0 /\ tmp___0^0-tmp___0^post27 == 0 /\ j^0-j^post27 == 0 /\ -n^post27+n^0 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post27 == 0), cost: 1
  28: l20 -> l21 : tmp^0'=tmp^post28, j^0'=j^post28, x^0'=x^post28, n^0'=n^post28, i^0'=i^post28, tmp___0^0'=tmp___0^post28, m^0'=m^post28, y^0'=y^post28, (0 == 0 /\ m^0-m^post28 == 0 /\ n^0-n^post28 == 0 /\ -1-j^0+j^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0 /\ i^0-i^post28 == 0 /\ j^0-n^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ x^0-x^post28 == 0), cost: 1
  29: l21 -> l20 : tmp^0'=tmp^post29, j^0'=j^post29, x^0'=x^post29, n^0'=n^post29, i^0'=i^post29, tmp___0^0'=tmp___0^post29, m^0'=m^post29, y^0'=y^post29, (-i^post29+i^0 == 0 /\ -y^post29+y^0 == 0 /\ -n^post29+n^0 == 0 /\ tmp___0^0-tmp___0^post29 == 0 /\ j^0-j^post29 == 0 /\ x^0-x^post29 == 0 /\ tmp^0-tmp^post29 == 0 /\ -m^post29+m^0 == 0), cost: 1
  33: l22 -> l3 : tmp^0'=tmp^post33, j^0'=j^post33, x^0'=x^post33, n^0'=n^post33, i^0'=i^post33, tmp___0^0'=tmp___0^post33, m^0'=m^post33, y^0'=y^post33, (tmp___0^0-tmp___0^post33 == 0 /\ -i^post33+i^0 == 0 /\ -x^post33+x^0 == 0 /\ -m^post33+m^0 == 0 /\ -y^post33+y^0 == 0 /\ -tmp^post33+tmp^0 == 0 /\ n^0-n^post33 == 0 /\ -1-j^0+j^post33 == 0), cost: 1
  36: l23 -> l5 : tmp^0'=tmp^post36, j^0'=j^post36, x^0'=x^post36, n^0'=n^post36, i^0'=i^post36, tmp___0^0'=tmp___0^post36, m^0'=m^post36, y^0'=y^post36, (-y^post36+y^0 == 0 /\ -m^post36+m^0 == 0 /\ tmp^0-tmp^post36 == 0 /\ -n^post36+n^0 == 0 /\ x^0-x^post36 == 0 /\ -j^post36+j^0 == 0 /\ i^0-i^post36 == 0 /\ tmp___0^0-tmp___0^post36 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : tmp^0'=tmp^post0, j^0'=j^post0, x^0'=x^post0, n^0'=n^post0, i^0'=i^post0, tmp___0^0'=tmp___0^post0, m^0'=m^post0, y^0'=y^post0, (-y^post0+y^0 == 0 /\ -m^post0+m^0 == 0 /\ tmp^0-tmp^post0 == 0 /\ -n^post0+n^0 == 0 /\ x^0-x^post0 == 0 /\ 1-j^0+n^0 <= 0 /\ -j^post0+j^0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ i^0-i^post0 == 0), cost: 1
New rule:
l0 -> l1 : 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : tmp^0'=tmp^post1, j^0'=j^post1, x^0'=x^post1, n^0'=n^post1, i^0'=i^post1, tmp___0^0'=tmp___0^post1, m^0'=m^post1, y^0'=y^post1, (0 == 0 /\ j^0-j^post1 == 0 /\ n^0-n^post1 == 0 /\ -m^post1+m^0 == 0 /\ -y^post1+y^0 == 0 /\ -i^post1+i^0 == 0 /\ j^0-n^0 <= 0 /\ -x^post1+x^0 == 0), cost: 1
New rule:
l0 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : tmp^0'=tmp^post2, j^0'=j^post2, x^0'=x^post2, n^0'=n^post2, i^0'=i^post2, tmp___0^0'=tmp___0^post2, m^0'=m^post2, y^0'=y^post2, (-y^post2+y^0 == 0 /\ x^0-x^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ i^0-i^post2 == 0 /\ -j^post2+j^0 == 0 /\ -m^post2+m^0 == 0 /\ n^0-n^post2 == 0), cost: 1
New rule:
l3 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : tmp^0'=tmp^post3, j^0'=j^post3, x^0'=x^post3, n^0'=n^post3, i^0'=i^post3, tmp___0^0'=tmp___0^post3, m^0'=m^post3, y^0'=y^post3, (j^0-j^post3 == 0 /\ -x^post3+x^0 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ -i^post3+i^0 == 0 /\ -1+m^post3-m^0 == 0 /\ -y^post3+y^0 == 0 /\ n^0-n^post3 == 0), cost: 1
New rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : tmp^0'=tmp^post4, j^0'=j^post4, x^0'=x^post4, n^0'=n^post4, i^0'=i^post4, tmp___0^0'=tmp___0^post4, m^0'=m^post4, y^0'=y^post4, (tmp^0-tmp^post4 == 0 /\ -1-i^0+i^post4 == 0 /\ -n^post4+n^0 == 0 /\ x^0-x^post4 == 0 /\ -m^post4+m^0 == 0 /\ j^0-j^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ -y^post4+y^0 == 0), cost: 1
New rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : tmp^0'=tmp^post5, j^0'=j^post5, x^0'=x^post5, n^0'=n^post5, i^0'=i^post5, tmp___0^0'=tmp___0^post5, m^0'=m^post5, y^0'=y^post5, (-m^post5+m^0 == 0 /\ -y^post5+y^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -i^post5+i^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ n^0-n^post5 == 0 /\ -x^post5+x^0 == 0 /\ 1-j^0+n^0 <= 0 /\ j^0-j^post5 == 0), cost: 1
New rule:
l8 -> l6 : 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l9 : tmp^0'=tmp^post6, j^0'=j^post6, x^0'=x^post6, n^0'=n^post6, i^0'=i^post6, tmp___0^0'=tmp___0^post6, m^0'=m^post6, y^0'=y^post6, (-1+j^post6-j^0 == 0 /\ -n^post6+n^0 == 0 /\ x^0-x^post6 == 0 /\ -m^post6+m^0 == 0 /\ tmp^0-tmp^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -y^post6+y^0 == 0 /\ j^0-n^0 <= 0 /\ i^0-i^post6 == 0), cost: 1
New rule:
l8 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : tmp^0'=tmp^post7, j^0'=j^post7, x^0'=x^post7, n^0'=n^post7, i^0'=i^post7, tmp___0^0'=tmp___0^post7, m^0'=m^post7, y^0'=y^post7, (tmp^0-tmp^post7 == 0 /\ i^0-i^post7 == 0 /\ -y^post7+y^0 == 0 /\ m^0-m^post7 == 0 /\ -x^post7+x^0 == 0 /\ n^0-n^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ j^0-j^post7 == 0), cost: 1
New rule:
l9 -> l8 : TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l9 : tmp^0'=tmp^post8, j^0'=j^post8, x^0'=x^post8, n^0'=n^post8, i^0'=i^post8, tmp___0^0'=tmp___0^post8, m^0'=m^post8, y^0'=y^post8, (-i^post8+i^0 == 0 /\ x^0-x^post8 == 0 /\ -y^post8+y^0 == 0 /\ -n^post8+n^0 == 0 /\ tmp___0^0-tmp___0^post8 == 0 /\ j^0-j^post8 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post8 == 0 /\ -m^post8+m^0 == 0), cost: 1
New rule:
l10 -> l9 : 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : tmp^0'=tmp^post9, j^0'=j^post9, x^0'=x^post9, n^0'=n^post9, i^0'=i^post9, tmp___0^0'=tmp___0^post9, m^0'=m^post9, y^0'=y^post9, (-x^post9+x^0 == 0 /\ -1-j^0+j^post9 == 0 /\ n^0-n^post9 == 0 /\ m^0-m^post9 == 0 /\ -y^post9+y^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ j^0-n^0 <= 0 /\ -i^post9+i^0 == 0), cost: 1
New rule:
l10 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : tmp^0'=tmp^post10, j^0'=j^post10, x^0'=x^post10, n^0'=n^post10, i^0'=i^post10, tmp___0^0'=tmp___0^post10, m^0'=m^post10, y^0'=y^post10, (x^0-x^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ -m^post10+m^0 == 0 /\ -y^post10+y^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -n^post10+n^0 == 0 /\ -i^post10+i^0 == 0 /\ j^0-j^post10 == 0), cost: 1
New rule:
l11 -> l10 : TRUE, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : tmp^0'=tmp^post11, j^0'=j^post11, x^0'=x^post11, n^0'=n^post11, i^0'=i^post11, tmp___0^0'=tmp___0^post11, m^0'=m^post11, y^0'=y^post11, (0 == 0 /\ tmp^0-tmp^post11 == 0 /\ i^0-i^post11 == 0 /\ -x^post11+x^0 == 0 /\ n^0-n^post11 == 0 /\ j^0-j^post11 == 0 /\ -m^post11+m^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0), cost: 1
New rule:
l12 -> l11 : y^0'=y^post11, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l6 : tmp^0'=tmp^post12, j^0'=j^post12, x^0'=x^post12, n^0'=n^post12, i^0'=i^post12, tmp___0^0'=tmp___0^post12, m^0'=m^post12, y^0'=y^post12, (j^0-j^post12 == 0 /\ -y^0 <= 0 /\ -i^post12+i^0 == 0 /\ -x^post12+x^0 == 0 /\ -y^post12+y^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ n^0-n^post12 == 0 /\ y^0 <= 0 /\ -m^post12+m^0 == 0), cost: 1
New rule:
l13 -> l6 : y^0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : tmp^0'=tmp^post13, j^0'=j^post13, x^0'=x^post13, n^0'=n^post13, i^0'=i^post13, tmp___0^0'=tmp___0^post13, m^0'=m^post13, y^0'=y^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ 1-y^0 <= 0 /\ i^0-i^post13 == 0 /\ tmp^0-tmp^post13 == 0 /\ -m^post13+m^0 == 0 /\ -n^post13+n^0 == 0 /\ x^0-x^post13 == 0 /\ -j^post13+j^0 == 0 /\ -y^post13+y^0 == 0), cost: 1
New rule:
l13 -> l12 : -1+y^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : tmp^0'=tmp^post14, j^0'=j^post14, x^0'=x^post14, n^0'=n^post14, i^0'=i^post14, tmp___0^0'=tmp___0^post14, m^0'=m^post14, y^0'=y^post14, (j^0-j^post14 == 0 /\ -x^post14+x^0 == 0 /\ -y^post14+y^0 == 0 /\ -m^post14+m^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ 1+y^0 <= 0 /\ n^0-n^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -i^post14+i^0 == 0), cost: 1
New rule:
l13 -> l12 : 1+y^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l4 : tmp^0'=tmp^post15, j^0'=j^post15, x^0'=x^post15, n^0'=n^post15, i^0'=i^post15, tmp___0^0'=tmp___0^post15, m^0'=m^post15, y^0'=y^post15, (-j^post15+j^0 == 0 /\ -m^post15+m^0 == 0 /\ -y^post15+y^0 == 0 /\ 1+n^0-i^0 <= 0 /\ x^0-x^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ n^0-n^post15 == 0 /\ i^0-i^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0), cost: 1
New rule:
l14 -> l4 : 1+n^0-i^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l14 -> l13 : tmp^0'=tmp^post16, j^0'=j^post16, x^0'=x^post16, n^0'=n^post16, i^0'=i^post16, tmp___0^0'=tmp___0^post16, m^0'=m^post16, y^0'=y^post16, (0 == 0 /\ j^0-j^post16 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ -i^post16+i^0 == 0 /\ -m^post16+m^0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -n^0+i^0 <= 0 /\ n^0-n^post16 == 0 /\ -x^post16+x^0 == 0), cost: 1
New rule:
l14 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l14 : tmp^0'=tmp^post17, j^0'=j^post17, x^0'=x^post17, n^0'=n^post17, i^0'=i^post17, tmp___0^0'=tmp___0^post17, m^0'=m^post17, y^0'=y^post17, (tmp^0-tmp^post17 == 0 /\ -n^post17+n^0 == 0 /\ x^0-x^post17 == 0 /\ -y^post17+y^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ j^0-j^post17 == 0 /\ i^0-i^post17 == 0 /\ -m^post17+m^0 == 0), cost: 1
New rule:
l7 -> l14 : TRUE, cost: 1

Applied preprocessing
Original rule:
l15 -> l4 : tmp^0'=tmp^post18, j^0'=j^post18, x^0'=x^post18, n^0'=n^post18, i^0'=i^post18, tmp___0^0'=tmp___0^post18, m^0'=m^post18, y^0'=y^post18, (-y^post18+y^0 == 0 /\ -x^post18+x^0 == 0 /\ j^0-j^post18 == 0 /\ -x^0 <= 0 /\ -m^post18+m^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ x^0 <= 0 /\ -i^post18+i^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ n^0-n^post18 == 0), cost: 1
New rule:
l15 -> l4 : x^0 == 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l7 : tmp^0'=tmp^post19, j^0'=j^post19, x^0'=x^post19, n^0'=n^post19, i^0'=i^post19, tmp___0^0'=tmp___0^post19, m^0'=m^post19, y^0'=y^post19, (1-x^0 <= 0 /\ x^0-x^post19 == 0 /\ tmp^0-tmp^post19 == 0 /\ -n^post19+n^0 == 0 /\ -y^post19+y^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -j^post19+j^0 == 0 /\ -m^post19+m^0 == 0 /\ -i^post19+i^0 == 0), cost: 1
New rule:
l15 -> l7 : -1+x^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l7 : tmp^0'=tmp^post20, j^0'=j^post20, x^0'=x^post20, n^0'=n^post20, i^0'=i^post20, tmp___0^0'=tmp___0^post20, m^0'=m^post20, y^0'=y^post20, (tmp^0-tmp^post20 == 0 /\ n^0-n^post20 == 0 /\ m^0-m^post20 == 0 /\ -x^post20+x^0 == 0 /\ -y^post20+y^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -i^post20+i^0 == 0 /\ j^0-j^post20 == 0 /\ 1+x^0 <= 0), cost: 1
New rule:
l15 -> l7 : 1+x^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l3 : tmp^0'=tmp^post22, j^0'=j^post22, x^0'=x^post22, n^0'=n^post22, i^0'=i^post22, tmp___0^0'=tmp___0^post22, m^0'=m^post22, y^0'=y^post22, (-tmp___0^post22+tmp___0^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ x^post22 == 0 /\ -m^post22+m^0 == 0 /\ i^post22-m^0 == 0 /\ n^0-n^post22 == 0 /\ j^0-j^post22 == 0 /\ 1-n^0+m^0 <= 0 /\ -y^post22+y^0 == 0), cost: 1
New rule:
l16 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l18 -> l15 : tmp^0'=tmp^post23, j^0'=j^post23, x^0'=x^post23, n^0'=n^post23, i^0'=i^post23, tmp___0^0'=tmp___0^post23, m^0'=m^post23, y^0'=y^post23, (-y^post23+y^0 == 0 /\ -m^post23+m^0 == 0 /\ tmp^0-tmp^post23 == 0 /\ x^0-x^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -i^post23+i^0 == 0 /\ 1-j^0+n^0 <= 0 /\ -n^post23+n^0 == 0 /\ j^0-j^post23 == 0), cost: 1
New rule:
l18 -> l15 : 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l18 -> l19 : tmp^0'=tmp^post24, j^0'=j^post24, x^0'=x^post24, n^0'=n^post24, i^0'=i^post24, tmp___0^0'=tmp___0^post24, m^0'=m^post24, y^0'=y^post24, (0 == 0 /\ m^0-m^post24 == 0 /\ n^0-n^post24 == 0 /\ -1-j^0+j^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ i^0-i^post24 == 0 /\ j^0-n^0 <= 0 /\ x^0-x^post24 == 0 /\ tmp^0-tmp^post24 == 0), cost: 1
New rule:
l18 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l19 -> l18 : tmp^0'=tmp^post25, j^0'=j^post25, x^0'=x^post25, n^0'=n^post25, i^0'=i^post25, tmp___0^0'=tmp___0^post25, m^0'=m^post25, y^0'=y^post25, (-i^post25+i^0 == 0 /\ -n^post25+n^0 == 0 /\ -y^post25+y^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ j^0-j^post25 == 0 /\ x^0-x^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ -m^post25+m^0 == 0), cost: 1
New rule:
l19 -> l18 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l16 : tmp^0'=tmp^post26, j^0'=j^post26, x^0'=x^post26, n^0'=n^post26, i^0'=i^post26, tmp___0^0'=tmp___0^post26, m^0'=m^post26, y^0'=y^post26, (-x^post26+x^0 == 0 /\ i^0-i^post26 == 0 /\ -y^post26+y^0 == 0 /\ n^0-n^post26 == 0 /\ m^0-m^post26 == 0 /\ j^0-j^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ tmp^0-tmp^post26 == 0), cost: 1
New rule:
l5 -> l16 : TRUE, cost: 1

Applied preprocessing
Original rule:
l20 -> l19 : tmp^0'=tmp^post27, j^0'=j^post27, x^0'=x^post27, n^0'=n^post27, i^0'=i^post27, tmp___0^0'=tmp___0^post27, m^0'=m^post27, y^0'=y^post27, (x^0-x^post27 == 0 /\ -y^post27+y^0 == 0 /\ -m^post27+m^0 == 0 /\ -i^post27+i^0 == 0 /\ tmp___0^0-tmp___0^post27 == 0 /\ j^0-j^post27 == 0 /\ -n^post27+n^0 == 0 /\ 1-j^0+n^0 <= 0 /\ tmp^0-tmp^post27 == 0), cost: 1
New rule:
l20 -> l19 : 1-j^0+n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l20 -> l21 : tmp^0'=tmp^post28, j^0'=j^post28, x^0'=x^post28, n^0'=n^post28, i^0'=i^post28, tmp___0^0'=tmp___0^post28, m^0'=m^post28, y^0'=y^post28, (0 == 0 /\ m^0-m^post28 == 0 /\ n^0-n^post28 == 0 /\ -1-j^0+j^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0 /\ i^0-i^post28 == 0 /\ j^0-n^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ x^0-x^post28 == 0), cost: 1
New rule:
l20 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l21 -> l20 : tmp^0'=tmp^post29, j^0'=j^post29, x^0'=x^post29, n^0'=n^post29, i^0'=i^post29, tmp___0^0'=tmp___0^post29, m^0'=m^post29, y^0'=y^post29, (-i^post29+i^0 == 0 /\ -y^post29+y^0 == 0 /\ -n^post29+n^0 == 0 /\ tmp___0^0-tmp___0^post29 == 0 /\ j^0-j^post29 == 0 /\ x^0-x^post29 == 0 /\ tmp^0-tmp^post29 == 0 /\ -m^post29+m^0 == 0), cost: 1
New rule:
l21 -> l20 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l15 : tmp^0'=tmp^post30, j^0'=j^post30, x^0'=x^post30, n^0'=n^post30, i^0'=i^post30, tmp___0^0'=tmp___0^post30, m^0'=m^post30, y^0'=y^post30, (-x^post30+x^0 == 0 /\ i^0-m^0 <= 0 /\ i^0-i^post30 == 0 /\ m^0-m^post30 == 0 /\ -i^0+m^0 <= 0 /\ n^0-n^post30 == 0 /\ -y^post30+y^0 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ j^0-j^post30 == 0 /\ tmp^0-tmp^post30 == 0), cost: 1
New rule:
l1 -> l15 : i^0-m^0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l21 : tmp^0'=tmp^post31, j^0'=j^post31, x^0'=x^post31, n^0'=n^post31, i^0'=i^post31, tmp___0^0'=tmp___0^post31, m^0'=m^post31, y^0'=y^post31, (x^0-x^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ -n^post31+n^0 == 0 /\ 1-i^0+m^0 <= 0 /\ j^0-j^post31 == 0 /\ -i^post31+i^0 == 0 /\ -m^post31+m^0 == 0 /\ tmp^0-tmp^post31 == 0 /\ -y^post31+y^0 == 0), cost: 1
New rule:
l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l21 : tmp^0'=tmp^post32, j^0'=j^post32, x^0'=x^post32, n^0'=n^post32, i^0'=i^post32, tmp___0^0'=tmp___0^post32, m^0'=m^post32, y^0'=y^post32, (-j^post32+j^0 == 0 /\ i^0-i^post32 == 0 /\ 1+i^0-m^0 <= 0 /\ -y^post32+y^0 == 0 /\ -m^post32+m^0 == 0 /\ tmp^0-tmp^post32 == 0 /\ x^0-x^post32 == 0 /\ n^0-n^post32 == 0 /\ -tmp___0^post32+tmp___0^0 == 0), cost: 1
New rule:
l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l22 -> l3 : tmp^0'=tmp^post33, j^0'=j^post33, x^0'=x^post33, n^0'=n^post33, i^0'=i^post33, tmp___0^0'=tmp___0^post33, m^0'=m^post33, y^0'=y^post33, (tmp___0^0-tmp___0^post33 == 0 /\ -i^post33+i^0 == 0 /\ -x^post33+x^0 == 0 /\ -m^post33+m^0 == 0 /\ -y^post33+y^0 == 0 /\ -tmp^post33+tmp^0 == 0 /\ n^0-n^post33 == 0 /\ -1-j^0+j^post33 == 0), cost: 1
New rule:
l22 -> l3 : j^0'=1+j^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l22 : tmp^0'=tmp^post34, j^0'=j^post34, x^0'=x^post34, n^0'=n^post34, i^0'=i^post34, tmp___0^0'=tmp___0^post34, m^0'=m^post34, y^0'=y^post34, (i^0-i^post34 == 0 /\ -tmp___0^post34+tmp___0^0 == 0 /\ n^0-n^post34 == 0 /\ j^0-j^post34 == 0 /\ -m^post34+m^0 == 0 /\ tmp^0-tmp^post34 == 0 /\ x^0-x^post34 == 0 /\ -y^post34+y^0 == 0 /\ tmp^0-tmp___0^0 <= 0), cost: 1
New rule:
l2 -> l22 : tmp^0-tmp___0^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l22 : tmp^0'=tmp^post35, j^0'=j^post35, x^0'=x^post35, n^0'=n^post35, i^0'=i^post35, tmp___0^0'=tmp___0^post35, m^0'=m^post35, y^0'=y^post35, (0 == 0 /\ -j^0+i^post35 == 0 /\ -n^post35+n^0 == 0 /\ j^0-j^post35 == 0 /\ -y^post35+y^0 == 0 /\ tmp^0-tmp^post35 == 0 /\ -tmp___0^post35+tmp___0^0 == 0 /\ 1-tmp^0+tmp___0^0 <= 0 /\ -m^post35+m^0 == 0), cost: 1
New rule:
l2 -> l22 : x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l23 -> l5 : tmp^0'=tmp^post36, j^0'=j^post36, x^0'=x^post36, n^0'=n^post36, i^0'=i^post36, tmp___0^0'=tmp___0^post36, m^0'=m^post36, y^0'=y^post36, (-y^post36+y^0 == 0 /\ -m^post36+m^0 == 0 /\ tmp^0-tmp^post36 == 0 /\ -n^post36+n^0 == 0 /\ x^0-x^post36 == 0 /\ -j^post36+j^0 == 0 /\ i^0-i^post36 == 0 /\ tmp___0^0-tmp___0^post36 == 0), cost: 1
New rule:
l23 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l23
  37: l0 -> l1 : 1-j^0+n^0 <= 0, cost: 1
  38: l0 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 1
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
  70: l2 -> l22 : tmp^0-tmp___0^0 <= 0, cost: 1
  71: l2 -> l22 : x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 1
  39: l3 -> l0 : TRUE, cost: 1
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  62: l5 -> l16 : TRUE, cost: 1
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  54: l7 -> l14 : TRUE, cost: 1
  42: l8 -> l6 : 1-j^0+n^0 <= 0, cost: 1
  43: l8 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
  44: l9 -> l8 : TRUE, cost: 1
  45: l10 -> l9 : 1-j^0+n^0 <= 0, cost: 1
  46: l10 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
  47: l11 -> l10 : TRUE, cost: 1
  48: l12 -> l11 : y^0'=y^post11, 0 == 0, cost: 1
  49: l13 -> l6 : y^0 == 0, cost: 1
  50: l13 -> l12 : -1+y^0 >= 0, cost: 1
  51: l13 -> l12 : 1+y^0 <= 0, cost: 1
  52: l14 -> l4 : 1+n^0-i^0 <= 0, cost: 1
  53: l14 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 1
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  58: l16 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 1
  59: l18 -> l15 : 1-j^0+n^0 <= 0, cost: 1
  60: l18 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 1
  61: l19 -> l18 : TRUE, cost: 1
  63: l20 -> l19 : 1-j^0+n^0 <= 0, cost: 1
  64: l20 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 1
  65: l21 -> l20 : TRUE, cost: 1
  69: l22 -> l3 : j^0'=1+j^0, TRUE, cost: 1
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l16 by chaining:

Applied chaining
First rule:
l5 -> l16 : TRUE, cost: 1
Second rule:
l16 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 1
New rule:
l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 58 62

Eliminated locations on linear paths
Start location: l23
  37: l0 -> l1 : 1-j^0+n^0 <= 0, cost: 1
  38: l0 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 1
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
  70: l2 -> l22 : tmp^0-tmp___0^0 <= 0, cost: 1
  71: l2 -> l22 : x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 1
  39: l3 -> l0 : TRUE, cost: 1
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  54: l7 -> l14 : TRUE, cost: 1
  42: l8 -> l6 : 1-j^0+n^0 <= 0, cost: 1
  43: l8 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
  44: l9 -> l8 : TRUE, cost: 1
  45: l10 -> l9 : 1-j^0+n^0 <= 0, cost: 1
  46: l10 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
  47: l11 -> l10 : TRUE, cost: 1
  48: l12 -> l11 : y^0'=y^post11, 0 == 0, cost: 1
  49: l13 -> l6 : y^0 == 0, cost: 1
  50: l13 -> l12 : -1+y^0 >= 0, cost: 1
  51: l13 -> l12 : 1+y^0 <= 0, cost: 1
  52: l14 -> l4 : 1+n^0-i^0 <= 0, cost: 1
  53: l14 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 1
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  59: l18 -> l15 : 1-j^0+n^0 <= 0, cost: 1
  60: l18 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 1
  61: l19 -> l18 : TRUE, cost: 1
  63: l20 -> l19 : 1-j^0+n^0 <= 0, cost: 1
  64: l20 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 1
  65: l21 -> l20 : TRUE, cost: 1
  69: l22 -> l3 : j^0'=1+j^0, TRUE, cost: 1
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l0 by chaining:

Applied chaining
First rule:
l3 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : 1-j^0+n^0 <= 0, cost: 1
New rule:
l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l3 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 1
New rule:
l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 37 38 39

Eliminating location l14 by chaining:

Applied chaining
First rule:
l7 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l4 : 1+n^0-i^0 <= 0, cost: 1
New rule:
l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2

Applied chaining
First rule:
l7 -> l14 : TRUE, cost: 1
Second rule:
l14 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 1
New rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 52 53 54

Eliminating location l12 by chaining:

Applied chaining
First rule:
l13 -> l12 : -1+y^0 >= 0, cost: 1
Second rule:
l12 -> l11 : y^0'=y^post11, 0 == 0, cost: 1
New rule:
l13 -> l11 : y^0'=y^post11, (0 == 0 /\ -1+y^0 >= 0), cost: 2

Applied simplification
Original rule:
l13 -> l11 : y^0'=y^post11, (0 == 0 /\ -1+y^0 >= 0), cost: 2
New rule:
l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2

Applied chaining
First rule:
l13 -> l12 : 1+y^0 <= 0, cost: 1
Second rule:
l12 -> l11 : y^0'=y^post11, 0 == 0, cost: 1
New rule:
l13 -> l11 : y^0'=y^post11, (0 == 0 /\ 1+y^0 <= 0), cost: 2

Applied simplification
Original rule:
l13 -> l11 : y^0'=y^post11, (0 == 0 /\ 1+y^0 <= 0), cost: 2
New rule:
l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 48 50 51

Eliminating location l10 by chaining:

Applied chaining
First rule:
l11 -> l10 : TRUE, cost: 1
Second rule:
l10 -> l9 : 1-j^0+n^0 <= 0, cost: 1
New rule:
l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l11 -> l10 : TRUE, cost: 1
Second rule:
l10 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
New rule:
l11 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 45 46 47

Eliminating location l8 by chaining:

Applied chaining
First rule:
l9 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l6 : 1-j^0+n^0 <= 0, cost: 1
New rule:
l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l9 -> l8 : TRUE, cost: 1
Second rule:
l8 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 1
New rule:
l9 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 42 43 44

Eliminating location l20 by chaining:

Applied chaining
First rule:
l21 -> l20 : TRUE, cost: 1
Second rule:
l20 -> l19 : 1-j^0+n^0 <= 0, cost: 1
New rule:
l21 -> l19 : 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l21 -> l20 : TRUE, cost: 1
Second rule:
l20 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 1
New rule:
l21 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 63 64 65

Eliminating location l18 by chaining:

Applied chaining
First rule:
l19 -> l18 : TRUE, cost: 1
Second rule:
l18 -> l15 : 1-j^0+n^0 <= 0, cost: 1
New rule:
l19 -> l15 : 1-j^0+n^0 <= 0, cost: 2

Applied chaining
First rule:
l19 -> l18 : TRUE, cost: 1
Second rule:
l18 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 1
New rule:
l19 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 59 60 61

Eliminating location l22 by chaining:

Applied chaining
First rule:
l2 -> l22 : tmp^0-tmp___0^0 <= 0, cost: 1
Second rule:
l22 -> l3 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2

Applied chaining
First rule:
l2 -> l22 : x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 1
Second rule:
l22 -> l3 : j^0'=1+j^0, TRUE, cost: 1
New rule:
l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 69 70 71

Eliminated locations on tree-shaped paths
Start location: l23
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
  88: l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2
  89: l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2
  74: l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
  75: l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
  77: l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
  82: l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
  83: l9 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2
  80: l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
  81: l11 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2
  49: l13 -> l6 : y^0 == 0, cost: 1
  78: l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
  79: l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  86: l19 -> l15 : 1-j^0+n^0 <= 0, cost: 2
  87: l19 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 2
  84: l21 -> l19 : 1-j^0+n^0 <= 0, cost: 2
  85: l21 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 2
  72: l23 -> l5 : TRUE, cost: 1


Applied acceleration
Original rule:
l9 -> l9 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2
New rule:
l9 -> l9 : j^0'=j^0+n, (1-j^0+n^0-n >= 0 /\ n >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ADMeBd.txt

Applied instantiation
Original rule:
l9 -> l9 : j^0'=j^0+n, (1-j^0+n^0-n >= 0 /\ n >= 0), cost: 2*n
New rule:
l9 -> l9 : j^0'=1+n^0, (0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0

Applied simplification
Original rule:
l9 -> l9 : j^0'=1+n^0, (0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0
New rule:
l9 -> l9 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0

Applied deletion
Removed the following rules: 83

Applied acceleration
Original rule:
l11 -> l11 : j^0'=1+j^0, j^0-n^0 <= 0, cost: 2
New rule:
l11 -> l11 : j^0'=j^0+n0, (1-j^0+n^0-n0 >= 0 /\ n0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gHLilj.txt

Applied instantiation
Original rule:
l11 -> l11 : j^0'=j^0+n0, (1-j^0+n^0-n0 >= 0 /\ n0 >= 0), cost: 2*n0
New rule:
l11 -> l11 : j^0'=1+n^0, (0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0

Applied simplification
Original rule:
l11 -> l11 : j^0'=1+n^0, (0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0
New rule:
l11 -> l11 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0

Applied deletion
Removed the following rules: 81

Applied acceleration
Original rule:
l19 -> l19 : j^0'=1+j^0, y^0'=y^post24, j^0-n^0 <= 0, cost: 2
New rule:
l19 -> l19 : j^0'=j^0+n1, y^0'=y^post24, (-1+n1 >= 0 /\ 1-j^0+n^0-n1 >= 0), cost: 2*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bNIFKl.txt

Applied instantiation
Original rule:
l19 -> l19 : j^0'=j^0+n1, y^0'=y^post24, (-1+n1 >= 0 /\ 1-j^0+n^0-n1 >= 0), cost: 2*n1
New rule:
l19 -> l19 : j^0'=1+n^0, y^0'=y^post24, (0 >= 0 /\ -j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0

Applied simplification
Original rule:
l19 -> l19 : j^0'=1+n^0, y^0'=y^post24, (0 >= 0 /\ -j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0
New rule:
l19 -> l19 : j^0'=1+n^0, y^0'=y^post24, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0

Applied deletion
Removed the following rules: 87

Applied acceleration
Original rule:
l21 -> l21 : j^0'=1+j^0, y^0'=y^post28, j^0-n^0 <= 0, cost: 2
New rule:
l21 -> l21 : j^0'=n2+j^0, y^0'=y^post28, (1-n2-j^0+n^0 >= 0 /\ -1+n2 >= 0), cost: 2*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EHPnHb.txt

Applied instantiation
Original rule:
l21 -> l21 : j^0'=n2+j^0, y^0'=y^post28, (1-n2-j^0+n^0 >= 0 /\ -1+n2 >= 0), cost: 2*n2
New rule:
l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, (0 >= 0 /\ -j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0

Applied simplification
Original rule:
l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, (0 >= 0 /\ -j^0+n^0 >= 0), cost: 2-2*j^0+2*n^0
New rule:
l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0

Applied deletion
Removed the following rules: 85

Accelerated simple loops
Start location: l23
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
  88: l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2
  89: l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2
  74: l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
  75: l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
  77: l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
  82: l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
  91: l9 -> l9 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
  80: l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
  93: l11 -> l11 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
  49: l13 -> l6 : y^0 == 0, cost: 1
  78: l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
  79: l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  86: l19 -> l15 : 1-j^0+n^0 <= 0, cost: 2
  95: l19 -> l19 : j^0'=1+n^0, y^0'=y^post24, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
  84: l21 -> l19 : 1-j^0+n^0 <= 0, cost: 2
  97: l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied chaining
First rule:
l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l9 -> l9 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
New rule:
l11 -> l9 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 4-2*j^0+2*n^0

Applied deletion
Removed the following rules: 91

Applied chaining
First rule:
l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
Second rule:
l11 -> l11 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
New rule:
l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-1+y^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 4-2*j^0+2*n^0

Applied chaining
First rule:
l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
Second rule:
l11 -> l11 : j^0'=1+n^0, 1-j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
New rule:
l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1-j^0+n^0 >= 0 /\ 1+y^0 <= 0), cost: 4-2*j^0+2*n^0

Applied deletion
Removed the following rules: 93

Applied deletion
Removed the following rules: 95

Applied chaining
First rule:
l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
Second rule:
l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
New rule:
l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1-i^0+m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0

Applied chaining
First rule:
l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
Second rule:
l21 -> l21 : j^0'=1+n^0, y^0'=y^post28, -j^0+n^0 >= 0, cost: 2-2*j^0+2*n^0
New rule:
l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1+i^0-m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0

Applied deletion
Removed the following rules: 97

Chained accelerated rules with incoming rules
Start location: l23
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
 101: l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1-i^0+m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0
 102: l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1+i^0-m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0
  88: l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2
  89: l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2
  74: l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
  75: l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
  77: l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
  82: l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
  80: l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
  98: l11 -> l9 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 4-2*j^0+2*n^0
  49: l13 -> l6 : y^0 == 0, cost: 1
  78: l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
  79: l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
  99: l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-1+y^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 4-2*j^0+2*n^0
 100: l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1-j^0+n^0 >= 0 /\ 1+y^0 <= 0), cost: 4-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  86: l19 -> l15 : 1-j^0+n^0 <= 0, cost: 2
  84: l21 -> l19 : 1-j^0+n^0 <= 0, cost: 2
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l19 by chaining:

Applied chaining
First rule:
l21 -> l19 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l19 -> l15 : 1-j^0+n^0 <= 0, cost: 2
New rule:
l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 84 86

Eliminated locations on linear paths
Start location: l23
  66: l1 -> l15 : i^0-m^0 == 0, cost: 1
  67: l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
  68: l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
 101: l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1-i^0+m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0
 102: l1 -> l21 : j^0'=1+n^0, y^0'=y^post28, (1+i^0-m^0 <= 0 /\ -j^0+n^0 >= 0), cost: 3-2*j^0+2*n^0
  88: l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2
  89: l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2
  74: l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
  75: l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
  77: l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
  82: l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
  80: l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
  98: l11 -> l9 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 4-2*j^0+2*n^0
  49: l13 -> l6 : y^0 == 0, cost: 1
  78: l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
  79: l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
  99: l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-1+y^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 4-2*j^0+2*n^0
 100: l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1-j^0+n^0 >= 0 /\ 1+y^0 <= 0), cost: 4-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l1 by chaining:

Applied chaining
First rule:
l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l1 -> l15 : i^0-m^0 == 0, cost: 1
New rule:
l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3

Applied chaining
First rule:
l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l1 -> l21 : 1-i^0+m^0 <= 0, cost: 1
New rule:
l3 -> l21 : (1-i^0+m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3

Applied chaining
First rule:
l3 -> l1 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l1 -> l21 : 1+i^0-m^0 <= 0, cost: 1
New rule:
l3 -> l21 : (1+i^0-m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3

Applied deletion
Removed the following rules: 66 67 68 74 101 102

Eliminating location l2 by chaining:

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
Second rule:
l2 -> l3 : j^0'=1+j^0, tmp^0-tmp___0^0 <= 0, cost: 2
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, tmp___0^0'=tmp___0^post1, (-tmp___0^post1+tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4

Applied chaining
First rule:
l3 -> l2 : tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, j^0-n^0 <= 0, cost: 2
Second rule:
l2 -> l3 : j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, 1-tmp^0+tmp___0^0 <= 0, cost: 2
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, tmp___0^0'=tmp___0^post1, (1+tmp___0^post1-tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4

Applied deletion
Removed the following rules: 75 88 89

Eliminating location l13 by chaining:

Applied chaining
First rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
Second rule:
l13 -> l6 : y^0 == 0, cost: 1
New rule:
l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3

Applied chaining
First rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
Second rule:
l13 -> l11 : y^0'=y^post11, -1+y^0 >= 0, cost: 2
New rule:
l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4

Applied chaining
First rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
Second rule:
l13 -> l11 : y^0'=y^post11, 1+y^0 <= 0, cost: 2
New rule:
l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4

Applied chaining
First rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
Second rule:
l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-1+y^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 4-2*j^0+2*n^0
New rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l13 : y^0'=y^post16, -n^0+i^0 <= 0, cost: 2
Second rule:
l13 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1-j^0+n^0 >= 0 /\ 1+y^0 <= 0), cost: 4-2*j^0+2*n^0
New rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0

Applied deletion
Removed the following rules: 49 77 78 79 99 100

Eliminating location l9 by chaining:

Applied chaining
First rule:
l11 -> l9 : 1-j^0+n^0 <= 0, cost: 2
Second rule:
l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
New rule:
l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4

Applied chaining
First rule:
l11 -> l9 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 4-2*j^0+2*n^0
Second rule:
l9 -> l6 : 1-j^0+n^0 <= 0, cost: 2
New rule:
l11 -> l6 : j^0'=1+n^0, (0 <= 0 /\ 1-j^0+n^0 == 0), cost: 6-2*j^0+2*n^0

Applied simplification
Original rule:
l11 -> l6 : j^0'=1+n^0, (0 <= 0 /\ 1-j^0+n^0 == 0), cost: 6-2*j^0+2*n^0
New rule:
l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0

Applied deletion
Removed the following rules: 80 82 98

Eliminated locations on tree-shaped paths
Start location: l23
 104: l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3
 105: l3 -> l21 : (1-i^0+m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
 106: l3 -> l21 : (1+i^0-m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
 107: l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, tmp___0^0'=tmp___0^post1, (-tmp___0^post1+tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4
 108: l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, tmp___0^0'=tmp___0^post1, (1+tmp___0^post1-tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 110: l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4
 111: l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4
 112: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 113: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 114: l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
 115: l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Applied acceleration
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, tmp___0^0'=tmp___0^post1, (-tmp___0^post1+tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=j^0+n3, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ 1-j^0+n^0-n3 >= 0 /\ -1+n3 >= 0), cost: 4*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nKkNIF.txt

Applied instantiation
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=j^0+n3, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ 1-j^0+n^0-n3 >= 0 /\ -1+n3 >= 0), cost: 4*n3
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, tmp___0^0'=tmp___0^post1, (0 >= 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied acceleration
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+j^0, x^0'=x^post35, i^0'=j^0, tmp___0^0'=tmp___0^post1, (1+tmp___0^post1-tmp^post1 <= 0 /\ j^0-n^0 <= 0), cost: 4
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=j^0+n4, x^0'=x^post35, i^0'=-1+j^0+n4, tmp___0^0'=tmp___0^post1, (1-j^0+n^0-n4 >= 0 /\ -1+n4 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0), cost: 4*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_kCBDkL.txt

Applied instantiation
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=j^0+n4, x^0'=x^post35, i^0'=-1+j^0+n4, tmp___0^0'=tmp___0^post1, (1-j^0+n^0-n4 >= 0 /\ -1+n4 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0), cost: 4*n4
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied simplification
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, tmp___0^0'=tmp___0^post1, (0 >= 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied simplification
Original rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0

Applied deletion
Removed the following rules: 107 108

Accelerated simple loops
Start location: l23
 104: l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3
 105: l3 -> l21 : (1-i^0+m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
 106: l3 -> l21 : (1+i^0-m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
 118: l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
 119: l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 110: l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4
 111: l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4
 112: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 113: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 114: l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
 115: l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Applied chaining
First rule:
l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
Second rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
Second rule:
l3 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0), cost: 4-4*j^0+4*n^0
New rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0

Applied deletion
Removed the following rules: 118 119

Chained accelerated rules with incoming rules
Start location: l23
 104: l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3
 105: l3 -> l21 : (1-i^0+m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
 106: l3 -> l21 : (1+i^0-m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
  73: l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
 120: l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
 121: l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 110: l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4
 111: l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4
 112: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 113: l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
 114: l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
 115: l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l3 by chaining:

Applied chaining
First rule:
l5 -> l3 : x^0'=0, i^0'=m^0, 1-n^0+m^0 <= 0, cost: 2
Second rule:
l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3
New rule:
l5 -> l15 : x^0'=0, i^0'=m^0, (0 == 0 /\ 1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5

Applied simplification
Original rule:
l5 -> l15 : x^0'=0, i^0'=m^0, (0 == 0 /\ 1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5
New rule:
l5 -> l15 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5

Applied chaining
First rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
Second rule:
l3 -> l15 : (i^0-m^0 == 0 /\ 1-j^0+n^0 <= 0), cost: 3
New rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ 0 == 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ 0 == 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
New rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
Second rule:
l3 -> l21 : (1-i^0+m^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 3
New rule:
l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
New rule:
l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0

Applied partial deletion
Original rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
New rule:
l5 -> [29] : (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0

Applied partial deletion
Original rule:
l5 -> l3 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
New rule:
l5 -> [29] : (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0

Applied deletion
Removed the following rules: 73 104 105 106 120 121

Eliminating location l11 by chaining:

Applied chaining
First rule:
l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4
Second rule:
l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
New rule:
l7 -> l6 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 8

Applied chaining
First rule:
l7 -> l11 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0), cost: 4
Second rule:
l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4
Second rule:
l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
New rule:
l7 -> l6 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 8

Applied chaining
First rule:
l7 -> l11 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0), cost: 4
Second rule:
l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
Second rule:
l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 <= 0 /\ -n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied simplification
Original rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 <= 0 /\ -n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
Second rule:
l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 == 0 /\ -n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied simplification
Original rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 == 0 /\ -n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
Second rule:
l11 -> l6 : 1-j^0+n^0 <= 0, cost: 4
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 <= 0 /\ 1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied simplification
Original rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 <= 0 /\ 1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l11 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 6-2*j^0+2*n^0
Second rule:
l11 -> l6 : j^0'=1+n^0, 1-j^0+n^0 == 0, cost: 6-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 == 0 /\ 1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied simplification
Original rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (0 == 0 /\ 1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
New rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0

Applied deletion
Removed the following rules: 110 111 112 113 114 115

Eliminated locations on tree-shaped paths
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 122: l5 -> l15 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5
 123: l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
 124: l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
 125: l5 -> [29] : (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
 126: l5 -> [29] : (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 6-4*j^0+4*n^0
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 127: l7 -> l6 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 128: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
 129: l7 -> l6 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 130: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
 131: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
 132: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 >= 0), cost: 10-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Applied pruning (of leafs and parallel rules):
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 122: l5 -> l15 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5
 123: l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
 124: l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 127: l7 -> l6 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 128: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
 129: l7 -> l6 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 130: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
 103: l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l21 by chaining:

Applied chaining
First rule:
l5 -> l21 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
Second rule:
l21 -> l15 : 1-j^0+n^0 <= 0, cost: 4
New rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0
New rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0

Applied deletion
Removed the following rules: 103 124

Eliminated locations on linear paths
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 122: l5 -> l15 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5
 123: l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
 133: l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0
  41: l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 109: l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
 127: l7 -> l6 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 128: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
 129: l7 -> l6 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 8
 130: l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
  55: l15 -> l4 : x^0 == 0, cost: 1
  56: l15 -> l7 : -1+x^0 >= 0, cost: 1
  57: l15 -> l7 : 1+x^0 <= 0, cost: 1
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l15 by chaining:

Applied chaining
First rule:
l5 -> l15 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 5
Second rule:
l15 -> l4 : x^0 == 0, cost: 1
New rule:
l5 -> l4 : x^0'=0, i^0'=m^0, (0 == 0 /\ 1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6

Applied simplification
Original rule:
l5 -> l4 : x^0'=0, i^0'=m^0, (0 == 0 /\ 1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
New rule:
l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6

Applied chaining
First rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
Second rule:
l15 -> l4 : x^0 == 0, cost: 1
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0
Second rule:
l15 -> l4 : x^0 == 0, cost: 1
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0
Second rule:
l15 -> l7 : -1+x^0 >= 0, cost: 1
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 13-4*j^0+4*n^0
Second rule:
l15 -> l7 : 1+x^0 <= 0, cost: 1
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0

Applied partial deletion
Original rule:
l5 -> l15 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
New rule:
l5 -> [30] : (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0

Applied deletion
Removed the following rules: 55 56 57 122 123 133

Eliminating location l6 by chaining:

Applied chaining
First rule:
l7 -> l6 : y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 3
Second rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 4

Applied chaining
First rule:
l7 -> l6 : y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 8
Second rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 9

Applied chaining
First rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
Second rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0

Applied chaining
First rule:
l7 -> l6 : y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 8
Second rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9

Applied chaining
First rule:
l7 -> l6 : j^0'=1+n^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 10-2*j^0+2*n^0
Second rule:
l6 -> l7 : i^0'=1+i^0, TRUE, cost: 1
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0

Applied deletion
Removed the following rules: 41 109 127 128 129 130

Eliminated locations on tree-shaped paths
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 137: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 138: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
 139: l5 -> [30] : (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 9-4*j^0+4*n^0
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 140: l7 -> l7 : i^0'=1+i^0, y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 4
 141: l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 9
 142: l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
 143: l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9
 144: l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied pruning (of leafs and parallel rules):
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 137: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 138: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 140: l7 -> l7 : i^0'=1+i^0, y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 4
 141: l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 9
 142: l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
 143: l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9
 144: l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied simplification
Original rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post16, (-n^0+i^0 <= 0 /\ y^post16 == 0), cost: 4
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=0, -n^0+i^0 <= 0, cost: 4

Applied simplification
Original rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 <= 0), cost: 9
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9

Applied simplification
Original rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ -1+y^post16 >= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0

Applied simplification
Original rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9
New rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9

Applied simplification
Original rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (1+y^post16 <= 0 /\ -n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0

Simplified simple loops
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 137: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 138: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 145: l7 -> l7 : i^0'=1+i^0, y^0'=0, -n^0+i^0 <= 0, cost: 4
 146: l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9
 147: l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied acceleration
Original rule:
l7 -> l7 : i^0'=1+i^0, y^0'=0, -n^0+i^0 <= 0, cost: 4
New rule:
l7 -> l7 : i^0'=n5+i^0, y^0'=0, (1-n5+n^0-i^0 >= 0 /\ -1+n5 >= 0), cost: 4*n5
Sub-proof via acceration calculus written to file:///tmp/tmpnam_imlFCG.txt

Applied instantiation
Original rule:
l7 -> l7 : i^0'=n5+i^0, y^0'=0, (1-n5+n^0-i^0 >= 0 /\ -1+n5 >= 0), cost: 4*n5
New rule:
l7 -> l7 : i^0'=1+n^0, y^0'=0, (0 >= 0 /\ n^0-i^0 >= 0), cost: 4+4*n^0-4*i^0

Applied acceleration
Original rule:
l7 -> l7 : i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 <= 0), cost: 9
New rule:
l7 -> l7 : i^0'=i^0+n6, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ -1+n6 >= 0 /\ 1+n^0-i^0-n6 >= 0), cost: 9*n6
Sub-proof via acceration calculus written to file:///tmp/tmpnam_FHAogh.txt

Applied instantiation
Original rule:
l7 -> l7 : i^0'=i^0+n6, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ -1+n6 >= 0 /\ 1+n^0-i^0-n6 >= 0), cost: 9*n6
New rule:
l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0

Applied acceleration
Original rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+i^0, y^0'=y^post11, (-n^0+i^0 <= 0 /\ 1-j^0+n^0 == 0), cost: 11-2*j^0+2*n^0
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=n7+i^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ 1-j^0+n^0 >= 0 /\ 1-n7+n^0-i^0 >= 0 /\ -1+n7 >= 0), cost: 9*n7
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gGlclF.txt

Applied instantiation
Original rule:
l7 -> l7 : j^0'=1+n^0, i^0'=n7+i^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ 1-j^0+n^0 >= 0 /\ 1-n7+n^0-i^0 >= 0 /\ -1+n7 >= 0), cost: 9*n7
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0

Applied simplification
Original rule:
l7 -> l7 : i^0'=1+n^0, y^0'=0, (0 >= 0 /\ n^0-i^0 >= 0), cost: 4+4*n^0-4*i^0
New rule:
l7 -> l7 : i^0'=1+n^0, y^0'=0, n^0-i^0 >= 0, cost: 4+4*n^0-4*i^0

Applied simplification
Original rule:
l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0

Applied simplification
Original rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0

Applied deletion
Removed the following rules: 145 146 147

Accelerated simple loops
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 137: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 138: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
 151: l7 -> l7 : i^0'=1+n^0, y^0'=0, n^0-i^0 >= 0, cost: 4+4*n^0-4*i^0
 152: l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0
 153: l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0
  72: l23 -> l5 : TRUE, cost: 1


Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : i^0'=1+n^0, y^0'=0, n^0-i^0 >= 0, cost: 4+4*n^0-4*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 18-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : i^0'=1+n^0, y^0'=0, n^0-i^0 >= 0, cost: 4+4*n^0-4*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 18-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 23-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 23-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 23-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l7 -> l7 : j^0'=1+n^0, i^0'=1+n^0, y^0'=y^post11, (-1+j^0-n^0 >= 0 /\ n^0-i^0 >= 0 /\ 1-j^0+n^0 >= 0), cost: 9+9*n^0-9*i^0
New rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 23-4*j^0+4*n^0

Applied deletion
Removed the following rules: 151 152 153

Chained accelerated rules with incoming rules
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 137: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 138: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
 154: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 18-4*j^0+4*n^0
 155: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 18-4*j^0+4*n^0
 156: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 23-4*j^0+4*n^0
 157: l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 23-4*j^0+4*n^0
  76: l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l7 by chaining:

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 18-4*j^0+4*n^0
Second rule:
l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (0 <= 0 /\ -1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (0 <= 0 /\ -1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 18-4*j^0+4*n^0
Second rule:
l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 23-4*j^0+4*n^0
Second rule:
l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (0 <= 0 /\ -1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 25-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (0 <= 0 /\ -1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 25-4*j^0+4*n^0
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 25-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 23-4*j^0+4*n^0
Second rule:
l7 -> l4 : 1+n^0-i^0 <= 0, cost: 2
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 25-4*j^0+4*n^0

Applied simplification
Original rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (0 <= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 25-4*j^0+4*n^0
New rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 25-4*j^0+4*n^0

Applied partial deletion
Original rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
New rule:
l5 -> [32] : (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0

Applied partial deletion
Original rule:
l5 -> l7 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
New rule:
l5 -> [32] : (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0

Applied deletion
Removed the following rules: 76 137 138 154 155 156 157

Eliminated locations on tree-shaped paths
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 158: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0
 159: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0
 160: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 25-4*j^0+4*n^0
 161: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=y^post11, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 25-4*j^0+4*n^0
 162: l5 -> [32] : (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 163: l5 -> [32] : (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 14-4*j^0+4*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied pruning (of leafs and parallel rules):
Start location: l23
  40: l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
 134: l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
 135: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
 136: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
 158: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0
 159: l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0
  72: l23 -> l5 : TRUE, cost: 1


Eliminating location l4 by chaining:

Applied chaining
First rule:
l5 -> l4 : x^0'=0, i^0'=m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 6
Second rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
New rule:
l5 -> l5 : x^0'=0, i^0'=m^0, m^0'=1+m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 7

Applied chaining
First rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 10-4*j^0+4*n^0
Second rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
New rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 11-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 14-4*j^0+4*n^0
Second rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
New rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 20-4*j^0+4*n^0
Second rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
New rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 21-4*j^0+4*n^0

Applied chaining
First rule:
l5 -> l4 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 20-4*j^0+4*n^0
Second rule:
l4 -> l5 : m^0'=1+m^0, TRUE, cost: 1
New rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 21-4*j^0+4*n^0

Applied deletion
Removed the following rules: 40 134 135 136 158 159

Eliminated locations on tree-shaped paths
Start location: l23
 164: l5 -> l5 : x^0'=0, i^0'=m^0, m^0'=1+m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 7
 165: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 11-4*j^0+4*n^0
 166: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0
 167: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 21-4*j^0+4*n^0
 168: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 21-4*j^0+4*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied simplification
Original rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (x^post35 == 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0
New rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0

Simplified simple loops
Start location: l23
 164: l5 -> l5 : x^0'=0, i^0'=m^0, m^0'=1+m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 7
 165: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 11-4*j^0+4*n^0
 167: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 21-4*j^0+4*n^0
 168: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 21-4*j^0+4*n^0
 169: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0
  72: l23 -> l5 : TRUE, cost: 1


Applied acceleration
Original rule:
l5 -> l5 : x^0'=0, i^0'=m^0, m^0'=1+m^0, (1-j^0+n^0 <= 0 /\ 1-n^0+m^0 <= 0), cost: 7
New rule:
l5 -> l5 : x^0'=0, i^0'=-1+n20+m^0, m^0'=n20+m^0, (-1+j^0-n^0 >= 0 /\ n^0-n20-m^0 >= 0 /\ -1+n20 >= 0), cost: 7*n20
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ahgpkJ.txt

Applied instantiation
Original rule:
l5 -> l5 : x^0'=0, i^0'=-1+n20+m^0, m^0'=n20+m^0, (-1+j^0-n^0 >= 0 /\ n^0-n20-m^0 >= 0 /\ -1+n20 >= 0), cost: 7*n20
New rule:
l5 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 7*n^0-7*m^0

Applied simplification
Original rule:
l5 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (0 >= 0 /\ -1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 7*n^0-7*m^0
New rule:
l5 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (-1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 7*n^0-7*m^0

Applied deletion
Removed the following rules: 164

Accelerated simple loops
Start location: l23
 165: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 11-4*j^0+4*n^0
 167: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 21-4*j^0+4*n^0
 168: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 21-4*j^0+4*n^0
 169: l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0
 171: l5 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (-1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 7*n^0-7*m^0
  72: l23 -> l5 : TRUE, cost: 1


Applied chaining
First rule:
l23 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 11-4*j^0+4*n^0
New rule:
l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 12-4*j^0+4*n^0

Applied chaining
First rule:
l23 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 21-4*j^0+4*n^0
New rule:
l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 22-4*j^0+4*n^0

Applied chaining
First rule:
l23 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 21-4*j^0+4*n^0
New rule:
l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 22-4*j^0+4*n^0

Applied chaining
First rule:
l23 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 15-4*j^0+4*n^0
New rule:
l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 16-4*j^0+4*n^0

Applied chaining
First rule:
l23 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (-1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 7*n^0-7*m^0
New rule:
l23 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (-1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 1+7*n^0-7*m^0

Applied deletion
Removed the following rules: 165 167 168 169 171

Chained accelerated rules with incoming rules
Start location: l23
  72: l23 -> l5 : TRUE, cost: 1
 172: l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=m^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (tmp___0^post1-tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 12-4*j^0+4*n^0
 173: l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1+x^post35 >= 0 /\ -1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 22-4*j^0+4*n^0
 174: l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=x^post35, i^0'=1+n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, y^0'=0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0 /\ 1+x^post35 <= 0), cost: 22-4*j^0+4*n^0
 175: l23 -> l5 : tmp^0'=tmp^post1, j^0'=1+n^0, x^0'=0, i^0'=n^0, tmp___0^0'=tmp___0^post1, m^0'=1+m^0, (-1-tmp___0^post1+tmp^post1 >= 0 /\ -j^0+n^0 >= 0 /\ 1-n^0+m^0 <= 0), cost: 16-4*j^0+4*n^0
 176: l23 -> l5 : x^0'=0, i^0'=-1+n^0, m^0'=n^0, (-1+j^0-n^0 >= 0 /\ -1+n^0-m^0 >= 0), cost: 1+7*n^0-7*m^0


Removed unreachable locations and irrelevant leafs
Start location: l23
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0