WORST_CASE(Omega(0),?)

Initial ITS
Start location: l16
   0: l0 -> l1 : pattern^0'=pattern^post0, c1^0'=c1^post0, xx^0'=xx^post0, it^0'=it^post0, buffer^0'=buffer^post0, z^0'=z^post0, seqlen^0'=seqlen^post0, c2^0'=c2^post0, yy^0'=yy^post0, (buffer^0-buffer^post0 == 0 /\ -yy^post0+yy^0 == 0 /\ z^0-z^post0 == 0 /\ xx^0-xx^post0 == 0 /\ pattern^0-pattern^post0 == 0 /\ c1^0-c1^post0 == 0 /\ -c2^post0+c2^0 == 0 /\ -seqlen^post0+seqlen^0 == 0 /\ it^0-it^post0 == 0), cost: 1
  23: l1 -> l13 : pattern^0'=pattern^post23, c1^0'=c1^post23, xx^0'=xx^post23, it^0'=it^post23, buffer^0'=buffer^post23, z^0'=z^post23, seqlen^0'=seqlen^post23, c2^0'=c2^post23, yy^0'=yy^post23, (-c1^post23+c1^0 == 0 /\ buffer^0-buffer^post23 == 0 /\ -c2^post23+c2^0 == 0 /\ -seqlen^post23+seqlen^0 == 0 /\ xx^0-xx^post23 == 0 /\ pattern^0-pattern^post23 == 0 /\ 1-xx^0+yy^0 <= 0 /\ -yy^post23+yy^0 == 0 /\ z^0-z^post23 == 0 /\ it^0-it^post23 == 0), cost: 1
  24: l1 -> l13 : pattern^0'=pattern^post24, c1^0'=c1^post24, xx^0'=xx^post24, it^0'=it^post24, buffer^0'=buffer^post24, z^0'=z^post24, seqlen^0'=seqlen^post24, c2^0'=c2^post24, yy^0'=yy^post24, (pattern^0-pattern^post24 == 0 /\ xx^0-xx^post24 == 0 /\ -z^post24+z^0 == 0 /\ it^0-it^post24 == 0 /\ c2^0-c2^post24 == 0 /\ -yy^post24+yy^0 == 0 /\ -buffer^post24+buffer^0 == 0 /\ -seqlen^post24+seqlen^0 == 0 /\ 1+xx^0-yy^0 <= 0 /\ c1^0-c1^post24 == 0), cost: 1
  25: l1 -> l15 : pattern^0'=pattern^post25, c1^0'=c1^post25, xx^0'=xx^post25, it^0'=it^post25, buffer^0'=buffer^post25, z^0'=z^post25, seqlen^0'=seqlen^post25, c2^0'=c2^post25, yy^0'=yy^post25, (-z^post25+z^0 == 0 /\ it^0-it^post25 == 0 /\ -c2^post25+c2^0 == 0 /\ -buffer^post25+buffer^0 == 0 /\ pattern^0-pattern^post25 == 0 /\ c1^0-c1^post25 == 0 /\ seqlen^0-seqlen^post25 == 0 /\ -xx^0+yy^0 <= 0 /\ -yy^post25+yy^0 == 0 /\ xx^0-yy^0 <= 0 /\ xx^0-xx^post25 == 0), cost: 1
   1: l2 -> l0 : pattern^0'=pattern^post1, c1^0'=c1^post1, xx^0'=xx^post1, it^0'=it^post1, buffer^0'=buffer^post1, z^0'=z^post1, seqlen^0'=seqlen^post1, c2^0'=c2^post1, yy^0'=yy^post1, (-c2^post1+c2^0 == 0 /\ -seqlen^post1+seqlen^0 == 0 /\ -1+yy^post1 == 0 /\ pattern^0-pattern^post1 == 0 /\ xx^0-xx^post1 == 0 /\ -c1^post1+c1^0 == 0 /\ -z^post1+z^0 == 0 /\ -buffer^post1+buffer^0 == 0 /\ it^0-it^post1 == 0), cost: 1
   2: l3 -> l4 : pattern^0'=pattern^post2, c1^0'=c1^post2, xx^0'=xx^post2, it^0'=it^post2, buffer^0'=buffer^post2, z^0'=z^post2, seqlen^0'=seqlen^post2, c2^0'=c2^post2, yy^0'=yy^post2, (-1+xx^post2 == 0 /\ c1^0-c1^post2 == 0 /\ c2^0-c2^post2 == 0 /\ -yy^post2+yy^0 == 0 /\ it^0-it^post2 == 0 /\ -z^post2+z^0 == 0 /\ pattern^0-pattern^post2 == 0 /\ seqlen^0-seqlen^post2 == 0 /\ -buffer^post2+buffer^0 == 0), cost: 1
   3: l4 -> l2 : pattern^0'=pattern^post3, c1^0'=c1^post3, xx^0'=xx^post3, it^0'=it^post3, buffer^0'=buffer^post3, z^0'=z^post3, seqlen^0'=seqlen^post3, c2^0'=c2^post3, yy^0'=yy^post3, (-c2^post3+c2^0 == 0 /\ -seqlen^post3+seqlen^0 == 0 /\ -yy^post3+yy^0 == 0 /\ -it^post3+it^0 == 0 /\ buffer^0-buffer^post3 == 0 /\ pattern^0-pattern^post3 == 0 /\ 1-c2^0 <= 0 /\ -xx^post3+xx^0 == 0 /\ c1^0-c1^post3 == 0 /\ -z^post3+z^0 == 0), cost: 1
   4: l4 -> l2 : pattern^0'=pattern^post4, c1^0'=c1^post4, xx^0'=xx^post4, it^0'=it^post4, buffer^0'=buffer^post4, z^0'=z^post4, seqlen^0'=seqlen^post4, c2^0'=c2^post4, yy^0'=yy^post4, (pattern^0-pattern^post4 == 0 /\ -seqlen^post4+seqlen^0 == 0 /\ -xx^post4+xx^0 == 0 /\ z^0-z^post4 == 0 /\ -it^post4+it^0 == 0 /\ -c2^post4+c2^0 == 0 /\ -yy^post4+yy^0 == 0 /\ 1+c2^0 <= 0 /\ buffer^0-buffer^post4 == 0 /\ c1^0-c1^post4 == 0), cost: 1
   5: l4 -> l0 : pattern^0'=pattern^post5, c1^0'=c1^post5, xx^0'=xx^post5, it^0'=it^post5, buffer^0'=buffer^post5, z^0'=z^post5, seqlen^0'=seqlen^post5, c2^0'=c2^post5, yy^0'=yy^post5, (-it^post5+it^0 == 0 /\ -c1^post5+c1^0 == 0 /\ -c2^0 <= 0 /\ z^0-z^post5 == 0 /\ -c2^post5+c2^0 == 0 /\ pattern^0-pattern^post5 == 0 /\ xx^0-xx^post5 == 0 /\ c2^0 <= 0 /\ -seqlen^post5+seqlen^0 == 0 /\ yy^post5 == 0 /\ buffer^0-buffer^post5 == 0), cost: 1
   6: l5 -> l6 : pattern^0'=pattern^post6, c1^0'=c1^post6, xx^0'=xx^post6, it^0'=it^post6, buffer^0'=buffer^post6, z^0'=z^post6, seqlen^0'=seqlen^post6, c2^0'=c2^post6, yy^0'=yy^post6, (0 == 0 /\ xx^0-xx^post6 == 0 /\ 1+z^post6-z^0 == 0 /\ -yy^post6+yy^0 == 0 /\ it^0-it^post6 == 0 /\ pattern^0-pattern^post6 == 0 /\ seqlen^0-seqlen^post6 == 0 /\ -buffer^post6+buffer^0 == 0), cost: 1
  10: l6 -> l3 : pattern^0'=pattern^post10, c1^0'=c1^post10, xx^0'=xx^post10, it^0'=it^post10, buffer^0'=buffer^post10, z^0'=z^post10, seqlen^0'=seqlen^post10, c2^0'=c2^post10, yy^0'=yy^post10, (xx^0-xx^post10 == 0 /\ -yy^post10+yy^0 == 0 /\ it^0-it^post10 == 0 /\ -z^post10+z^0 == 0 /\ c2^0-c2^post10 == 0 /\ c1^0-c1^post10 == 0 /\ -seqlen^post10+seqlen^0 == 0 /\ -buffer^post10+buffer^0 == 0 /\ 1-c1^0 <= 0 /\ pattern^0-pattern^post10 == 0), cost: 1
  11: l6 -> l3 : pattern^0'=pattern^post11, c1^0'=c1^post11, xx^0'=xx^post11, it^0'=it^post11, buffer^0'=buffer^post11, z^0'=z^post11, seqlen^0'=seqlen^post11, c2^0'=c2^post11, yy^0'=yy^post11, (c2^0-c2^post11 == 0 /\ -z^post11+z^0 == 0 /\ 1+c1^0 <= 0 /\ seqlen^0-seqlen^post11 == 0 /\ -yy^post11+yy^0 == 0 /\ c1^0-c1^post11 == 0 /\ -buffer^post11+buffer^0 == 0 /\ it^0-it^post11 == 0 /\ pattern^0-pattern^post11 == 0 /\ xx^0-xx^post11 == 0), cost: 1
  12: l6 -> l4 : pattern^0'=pattern^post12, c1^0'=c1^post12, xx^0'=xx^post12, it^0'=it^post12, buffer^0'=buffer^post12, z^0'=z^post12, seqlen^0'=seqlen^post12, c2^0'=c2^post12, yy^0'=yy^post12, (-yy^post12+yy^0 == 0 /\ c1^0-c1^post12 == 0 /\ c1^0 <= 0 /\ xx^post12 == 0 /\ -c2^post12+c2^0 == 0 /\ buffer^0-buffer^post12 == 0 /\ seqlen^0-seqlen^post12 == 0 /\ -it^post12+it^0 == 0 /\ pattern^0-pattern^post12 == 0 /\ -c1^0 <= 0 /\ -z^post12+z^0 == 0), cost: 1
   7: l7 -> l6 : pattern^0'=pattern^post7, c1^0'=c1^post7, xx^0'=xx^post7, it^0'=it^post7, buffer^0'=buffer^post7, z^0'=z^post7, seqlen^0'=seqlen^post7, c2^0'=c2^post7, yy^0'=yy^post7, (0 == 0 /\ -1-seqlen^0+seqlen^post7 == 0 /\ c1^0-c1^post7 == 0 /\ -xx^post7+xx^0 == 0 /\ -buffer^post7+buffer^0 == 0 /\ -c2^post7+c2^0 == 0 /\ 1-z^post7 <= 0 /\ -yy^post7+yy^0 == 0 /\ -pattern^post7+pattern^0 == 0 /\ it^post7-seqlen^post7 == 0), cost: 1
   8: l8 -> l7 : pattern^0'=pattern^post8, c1^0'=c1^post8, xx^0'=xx^post8, it^0'=it^post8, buffer^0'=buffer^post8, z^0'=z^post8, seqlen^0'=seqlen^post8, c2^0'=c2^post8, yy^0'=yy^post8, (-c2^post8+c2^0 == 0 /\ -2+pattern^0 <= 0 /\ -yy^post8+yy^0 == 0 /\ c1^0-c1^post8 == 0 /\ buffer^0-buffer^post8 == 0 /\ seqlen^0-seqlen^post8 == 0 /\ -it^post8+it^0 == 0 /\ -xx^post8+xx^0 == 0 /\ -z^post8+z^0 == 0 /\ -1-pattern^0+pattern^post8 == 0), cost: 1
   9: l8 -> l7 : pattern^0'=pattern^post9, c1^0'=c1^post9, xx^0'=xx^post9, it^0'=it^post9, buffer^0'=buffer^post9, z^0'=z^post9, seqlen^0'=seqlen^post9, c2^0'=c2^post9, yy^0'=yy^post9, (-yy^post9+yy^0 == 0 /\ -c2^post9+c2^0 == 0 /\ buffer^0-buffer^post9 == 0 /\ -seqlen^post9+seqlen^0 == 0 /\ z^0-z^post9 == 0 /\ xx^0-xx^post9 == 0 /\ -it^post9+it^0 == 0 /\ pattern^post9 == 0 /\ 3-pattern^0 <= 0 /\ -c1^post9+c1^0 == 0), cost: 1
  13: l9 -> l0 : pattern^0'=pattern^post13, c1^0'=c1^post13, xx^0'=xx^post13, it^0'=it^post13, buffer^0'=buffer^post13, z^0'=z^post13, seqlen^0'=seqlen^post13, c2^0'=c2^post13, yy^0'=yy^post13, (0 == 0 /\ -1+seqlen^post13 == 0 /\ -c2^post13+c2^0 == 0 /\ 1-z^post13 <= 0 /\ c1^0-c1^post13 == 0 /\ pattern^post13 == 0 /\ xx^post13 == 0 /\ buffer^0-buffer^post13 == 0 /\ it^post13-seqlen^post13 == 0 /\ yy^post13 == 0), cost: 1
  14: l10 -> l6 : pattern^0'=pattern^post14, c1^0'=c1^post14, xx^0'=xx^post14, it^0'=it^post14, buffer^0'=buffer^post14, z^0'=z^post14, seqlen^0'=seqlen^post14, c2^0'=c2^post14, yy^0'=yy^post14, (-seqlen^post14+seqlen^0 == 0 /\ -buffer^0+c1^post14 == 0 /\ -buffer^post14+buffer^0 == 0 /\ pattern^0-pattern^post14 == 0 /\ xx^0-xx^post14 == 0 /\ -c2^post14+c2^0 == 0 /\ it^0-it^post14 == 0 /\ -yy^post14+yy^0 == 0 /\ -z^post14+z^0 == 0), cost: 1
  15: l11 -> l10 : pattern^0'=pattern^post15, c1^0'=c1^post15, xx^0'=xx^post15, it^0'=it^post15, buffer^0'=buffer^post15, z^0'=z^post15, seqlen^0'=seqlen^post15, c2^0'=c2^post15, yy^0'=yy^post15, (-2+buffer^0 <= 0 /\ pattern^0-pattern^post15 == 0 /\ xx^0-xx^post15 == 0 /\ it^0-it^post15 == 0 /\ -buffer^post15+buffer^0 == 0 /\ -seqlen^post15+seqlen^0 == 0 /\ -yy^post15+yy^0 == 0 /\ -z^post15+z^0 == 0 /\ c1^0-c1^post15 == 0 /\ c2^post15 == 0), cost: 1
  16: l11 -> l10 : pattern^0'=pattern^post16, c1^0'=c1^post16, xx^0'=xx^post16, it^0'=it^post16, buffer^0'=buffer^post16, z^0'=z^post16, seqlen^0'=seqlen^post16, c2^0'=c2^post16, yy^0'=yy^post16, (c1^0-c1^post16 == 0 /\ -z^post16+z^0 == 0 /\ -xx^post16+xx^0 == 0 /\ seqlen^0-seqlen^post16 == 0 /\ -1+c2^post16 == 0 /\ 2+buffer^post16-buffer^0 == 0 /\ -yy^post16+yy^0 == 0 /\ pattern^0-pattern^post16 == 0 /\ 3-buffer^0 <= 0 /\ it^0-it^post16 == 0), cost: 1
  17: l12 -> l8 : pattern^0'=pattern^post17, c1^0'=c1^post17, xx^0'=xx^post17, it^0'=it^post17, buffer^0'=buffer^post17, z^0'=z^post17, seqlen^0'=seqlen^post17, c2^0'=c2^post17, yy^0'=yy^post17, (-xx^post17+xx^0 == 0 /\ buffer^0-buffer^post17 == 0 /\ z^0-z^post17 == 0 /\ -yy^post17+yy^0 == 0 /\ it^0 <= 0 /\ -seqlen^post17+seqlen^0 == 0 /\ c1^0-c1^post17 == 0 /\ -it^post17+it^0 == 0 /\ -c2^post17+c2^0 == 0 /\ pattern^0-pattern^post17 == 0), cost: 1
  18: l12 -> l11 : pattern^0'=pattern^post18, c1^0'=c1^post18, xx^0'=xx^post18, it^0'=it^post18, buffer^0'=buffer^post18, z^0'=z^post18, seqlen^0'=seqlen^post18, c2^0'=c2^post18, yy^0'=yy^post18, (1-it^0 <= 0 /\ c1^0-c1^post18 == 0 /\ -yy^post18+yy^0 == 0 /\ -seqlen^post18+seqlen^0 == 0 /\ pattern^0-pattern^post18 == 0 /\ 1-it^0+it^post18 == 0 /\ z^0-z^post18 == 0 /\ -pattern^0+buffer^post18 == 0 /\ xx^0-xx^post18 == 0 /\ -c2^post18+c2^0 == 0), cost: 1
  19: l13 -> l14 : pattern^0'=pattern^post19, c1^0'=c1^post19, xx^0'=xx^post19, it^0'=it^post19, buffer^0'=buffer^post19, z^0'=z^post19, seqlen^0'=seqlen^post19, c2^0'=c2^post19, yy^0'=yy^post19, (-buffer^post19+buffer^0 == 0 /\ -c2^post19+c2^0 == 0 /\ -seqlen^post19+seqlen^0 == 0 /\ -yy^post19+yy^0 == 0 /\ pattern^0-pattern^post19 == 0 /\ xx^0-xx^post19 == 0 /\ it^0-it^post19 == 0 /\ -c1^post19+c1^0 == 0 /\ -z^post19+z^0 == 0), cost: 1
  20: l15 -> l5 : pattern^0'=pattern^post20, c1^0'=c1^post20, xx^0'=xx^post20, it^0'=it^post20, buffer^0'=buffer^post20, z^0'=z^post20, seqlen^0'=seqlen^post20, c2^0'=c2^post20, yy^0'=yy^post20, (it^0-it^post20 == 0 /\ -buffer^post20+buffer^0 == 0 /\ c1^0-c1^post20 == 0 /\ -xx^post20+xx^0 == 0 /\ -yy^post20+yy^0 == 0 /\ -c2^post20+c2^0 == 0 /\ pattern^0-pattern^post20 == 0 /\ -z^post20+z^0 == 0 /\ 1-z^0 <= 0 /\ seqlen^0-seqlen^post20 == 0), cost: 1
  21: l15 -> l5 : pattern^0'=pattern^post21, c1^0'=c1^post21, xx^0'=xx^post21, it^0'=it^post21, buffer^0'=buffer^post21, z^0'=z^post21, seqlen^0'=seqlen^post21, c2^0'=c2^post21, yy^0'=yy^post21, (z^0-z^post21 == 0 /\ 1+z^0 <= 0 /\ pattern^0-pattern^post21 == 0 /\ -it^post21+it^0 == 0 /\ -c2^post21+c2^0 == 0 /\ buffer^0-buffer^post21 == 0 /\ -xx^post21+xx^0 == 0 /\ c1^0-c1^post21 == 0 /\ -yy^post21+yy^0 == 0 /\ -seqlen^post21+seqlen^0 == 0), cost: 1
  22: l15 -> l12 : pattern^0'=pattern^post22, c1^0'=c1^post22, xx^0'=xx^post22, it^0'=it^post22, buffer^0'=buffer^post22, z^0'=z^post22, seqlen^0'=seqlen^post22, c2^0'=c2^post22, yy^0'=yy^post22, (buffer^0-buffer^post22 == 0 /\ -xx^post22+xx^0 == 0 /\ -it^post22+it^0 == 0 /\ -yy^post22+yy^0 == 0 /\ z^0-z^post22 == 0 /\ -seqlen^post22+seqlen^0 == 0 /\ c1^0-c1^post22 == 0 /\ z^0 <= 0 /\ pattern^0-pattern^post22 == 0 /\ -z^0 <= 0 /\ -c2^post22+c2^0 == 0), cost: 1
  26: l16 -> l9 : pattern^0'=pattern^post26, c1^0'=c1^post26, xx^0'=xx^post26, it^0'=it^post26, buffer^0'=buffer^post26, z^0'=z^post26, seqlen^0'=seqlen^post26, c2^0'=c2^post26, yy^0'=yy^post26, (c1^0-c1^post26 == 0 /\ -xx^post26+xx^0 == 0 /\ pattern^0-pattern^post26 == 0 /\ -yy^post26+yy^0 == 0 /\ seqlen^0-seqlen^post26 == 0 /\ -z^post26+z^0 == 0 /\ -c2^post26+c2^0 == 0 /\ it^0-it^post26 == 0 /\ -buffer^post26+buffer^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l16
   0: l0 -> l1 : pattern^0'=pattern^post0, c1^0'=c1^post0, xx^0'=xx^post0, it^0'=it^post0, buffer^0'=buffer^post0, z^0'=z^post0, seqlen^0'=seqlen^post0, c2^0'=c2^post0, yy^0'=yy^post0, (buffer^0-buffer^post0 == 0 /\ -yy^post0+yy^0 == 0 /\ z^0-z^post0 == 0 /\ xx^0-xx^post0 == 0 /\ pattern^0-pattern^post0 == 0 /\ c1^0-c1^post0 == 0 /\ -c2^post0+c2^0 == 0 /\ -seqlen^post0+seqlen^0 == 0 /\ it^0-it^post0 == 0), cost: 1
  25: l1 -> l15 : pattern^0'=pattern^post25, c1^0'=c1^post25, xx^0'=xx^post25, it^0'=it^post25, buffer^0'=buffer^post25, z^0'=z^post25, seqlen^0'=seqlen^post25, c2^0'=c2^post25, yy^0'=yy^post25, (-z^post25+z^0 == 0 /\ it^0-it^post25 == 0 /\ -c2^post25+c2^0 == 0 /\ -buffer^post25+buffer^0 == 0 /\ pattern^0-pattern^post25 == 0 /\ c1^0-c1^post25 == 0 /\ seqlen^0-seqlen^post25 == 0 /\ -xx^0+yy^0 <= 0 /\ -yy^post25+yy^0 == 0 /\ xx^0-yy^0 <= 0 /\ xx^0-xx^post25 == 0), cost: 1
   1: l2 -> l0 : pattern^0'=pattern^post1, c1^0'=c1^post1, xx^0'=xx^post1, it^0'=it^post1, buffer^0'=buffer^post1, z^0'=z^post1, seqlen^0'=seqlen^post1, c2^0'=c2^post1, yy^0'=yy^post1, (-c2^post1+c2^0 == 0 /\ -seqlen^post1+seqlen^0 == 0 /\ -1+yy^post1 == 0 /\ pattern^0-pattern^post1 == 0 /\ xx^0-xx^post1 == 0 /\ -c1^post1+c1^0 == 0 /\ -z^post1+z^0 == 0 /\ -buffer^post1+buffer^0 == 0 /\ it^0-it^post1 == 0), cost: 1
   2: l3 -> l4 : pattern^0'=pattern^post2, c1^0'=c1^post2, xx^0'=xx^post2, it^0'=it^post2, buffer^0'=buffer^post2, z^0'=z^post2, seqlen^0'=seqlen^post2, c2^0'=c2^post2, yy^0'=yy^post2, (-1+xx^post2 == 0 /\ c1^0-c1^post2 == 0 /\ c2^0-c2^post2 == 0 /\ -yy^post2+yy^0 == 0 /\ it^0-it^post2 == 0 /\ -z^post2+z^0 == 0 /\ pattern^0-pattern^post2 == 0 /\ seqlen^0-seqlen^post2 == 0 /\ -buffer^post2+buffer^0 == 0), cost: 1
   3: l4 -> l2 : pattern^0'=pattern^post3, c1^0'=c1^post3, xx^0'=xx^post3, it^0'=it^post3, buffer^0'=buffer^post3, z^0'=z^post3, seqlen^0'=seqlen^post3, c2^0'=c2^post3, yy^0'=yy^post3, (-c2^post3+c2^0 == 0 /\ -seqlen^post3+seqlen^0 == 0 /\ -yy^post3+yy^0 == 0 /\ -it^post3+it^0 == 0 /\ buffer^0-buffer^post3 == 0 /\ pattern^0-pattern^post3 == 0 /\ 1-c2^0 <= 0 /\ -xx^post3+xx^0 == 0 /\ c1^0-c1^post3 == 0 /\ -z^post3+z^0 == 0), cost: 1
   4: l4 -> l2 : pattern^0'=pattern^post4, c1^0'=c1^post4, xx^0'=xx^post4, it^0'=it^post4, buffer^0'=buffer^post4, z^0'=z^post4, seqlen^0'=seqlen^post4, c2^0'=c2^post4, yy^0'=yy^post4, (pattern^0-pattern^post4 == 0 /\ -seqlen^post4+seqlen^0 == 0 /\ -xx^post4+xx^0 == 0 /\ z^0-z^post4 == 0 /\ -it^post4+it^0 == 0 /\ -c2^post4+c2^0 == 0 /\ -yy^post4+yy^0 == 0 /\ 1+c2^0 <= 0 /\ buffer^0-buffer^post4 == 0 /\ c1^0-c1^post4 == 0), cost: 1
   5: l4 -> l0 : pattern^0'=pattern^post5, c1^0'=c1^post5, xx^0'=xx^post5, it^0'=it^post5, buffer^0'=buffer^post5, z^0'=z^post5, seqlen^0'=seqlen^post5, c2^0'=c2^post5, yy^0'=yy^post5, (-it^post5+it^0 == 0 /\ -c1^post5+c1^0 == 0 /\ -c2^0 <= 0 /\ z^0-z^post5 == 0 /\ -c2^post5+c2^0 == 0 /\ pattern^0-pattern^post5 == 0 /\ xx^0-xx^post5 == 0 /\ c2^0 <= 0 /\ -seqlen^post5+seqlen^0 == 0 /\ yy^post5 == 0 /\ buffer^0-buffer^post5 == 0), cost: 1
   6: l5 -> l6 : pattern^0'=pattern^post6, c1^0'=c1^post6, xx^0'=xx^post6, it^0'=it^post6, buffer^0'=buffer^post6, z^0'=z^post6, seqlen^0'=seqlen^post6, c2^0'=c2^post6, yy^0'=yy^post6, (0 == 0 /\ xx^0-xx^post6 == 0 /\ 1+z^post6-z^0 == 0 /\ -yy^post6+yy^0 == 0 /\ it^0-it^post6 == 0 /\ pattern^0-pattern^post6 == 0 /\ seqlen^0-seqlen^post6 == 0 /\ -buffer^post6+buffer^0 == 0), cost: 1
  10: l6 -> l3 : pattern^0'=pattern^post10, c1^0'=c1^post10, xx^0'=xx^post10, it^0'=it^post10, buffer^0'=buffer^post10, z^0'=z^post10, seqlen^0'=seqlen^post10, c2^0'=c2^post10, yy^0'=yy^post10, (xx^0-xx^post10 == 0 /\ -yy^post10+yy^0 == 0 /\ it^0-it^post10 == 0 /\ -z^post10+z^0 == 0 /\ c2^0-c2^post10 == 0 /\ c1^0-c1^post10 == 0 /\ -seqlen^post10+seqlen^0 == 0 /\ -buffer^post10+buffer^0 == 0 /\ 1-c1^0 <= 0 /\ pattern^0-pattern^post10 == 0), cost: 1
  11: l6 -> l3 : pattern^0'=pattern^post11, c1^0'=c1^post11, xx^0'=xx^post11, it^0'=it^post11, buffer^0'=buffer^post11, z^0'=z^post11, seqlen^0'=seqlen^post11, c2^0'=c2^post11, yy^0'=yy^post11, (c2^0-c2^post11 == 0 /\ -z^post11+z^0 == 0 /\ 1+c1^0 <= 0 /\ seqlen^0-seqlen^post11 == 0 /\ -yy^post11+yy^0 == 0 /\ c1^0-c1^post11 == 0 /\ -buffer^post11+buffer^0 == 0 /\ it^0-it^post11 == 0 /\ pattern^0-pattern^post11 == 0 /\ xx^0-xx^post11 == 0), cost: 1
  12: l6 -> l4 : pattern^0'=pattern^post12, c1^0'=c1^post12, xx^0'=xx^post12, it^0'=it^post12, buffer^0'=buffer^post12, z^0'=z^post12, seqlen^0'=seqlen^post12, c2^0'=c2^post12, yy^0'=yy^post12, (-yy^post12+yy^0 == 0 /\ c1^0-c1^post12 == 0 /\ c1^0 <= 0 /\ xx^post12 == 0 /\ -c2^post12+c2^0 == 0 /\ buffer^0-buffer^post12 == 0 /\ seqlen^0-seqlen^post12 == 0 /\ -it^post12+it^0 == 0 /\ pattern^0-pattern^post12 == 0 /\ -c1^0 <= 0 /\ -z^post12+z^0 == 0), cost: 1
   7: l7 -> l6 : pattern^0'=pattern^post7, c1^0'=c1^post7, xx^0'=xx^post7, it^0'=it^post7, buffer^0'=buffer^post7, z^0'=z^post7, seqlen^0'=seqlen^post7, c2^0'=c2^post7, yy^0'=yy^post7, (0 == 0 /\ -1-seqlen^0+seqlen^post7 == 0 /\ c1^0-c1^post7 == 0 /\ -xx^post7+xx^0 == 0 /\ -buffer^post7+buffer^0 == 0 /\ -c2^post7+c2^0 == 0 /\ 1-z^post7 <= 0 /\ -yy^post7+yy^0 == 0 /\ -pattern^post7+pattern^0 == 0 /\ it^post7-seqlen^post7 == 0), cost: 1
   8: l8 -> l7 : pattern^0'=pattern^post8, c1^0'=c1^post8, xx^0'=xx^post8, it^0'=it^post8, buffer^0'=buffer^post8, z^0'=z^post8, seqlen^0'=seqlen^post8, c2^0'=c2^post8, yy^0'=yy^post8, (-c2^post8+c2^0 == 0 /\ -2+pattern^0 <= 0 /\ -yy^post8+yy^0 == 0 /\ c1^0-c1^post8 == 0 /\ buffer^0-buffer^post8 == 0 /\ seqlen^0-seqlen^post8 == 0 /\ -it^post8+it^0 == 0 /\ -xx^post8+xx^0 == 0 /\ -z^post8+z^0 == 0 /\ -1-pattern^0+pattern^post8 == 0), cost: 1
   9: l8 -> l7 : pattern^0'=pattern^post9, c1^0'=c1^post9, xx^0'=xx^post9, it^0'=it^post9, buffer^0'=buffer^post9, z^0'=z^post9, seqlen^0'=seqlen^post9, c2^0'=c2^post9, yy^0'=yy^post9, (-yy^post9+yy^0 == 0 /\ -c2^post9+c2^0 == 0 /\ buffer^0-buffer^post9 == 0 /\ -seqlen^post9+seqlen^0 == 0 /\ z^0-z^post9 == 0 /\ xx^0-xx^post9 == 0 /\ -it^post9+it^0 == 0 /\ pattern^post9 == 0 /\ 3-pattern^0 <= 0 /\ -c1^post9+c1^0 == 0), cost: 1
  13: l9 -> l0 : pattern^0'=pattern^post13, c1^0'=c1^post13, xx^0'=xx^post13, it^0'=it^post13, buffer^0'=buffer^post13, z^0'=z^post13, seqlen^0'=seqlen^post13, c2^0'=c2^post13, yy^0'=yy^post13, (0 == 0 /\ -1+seqlen^post13 == 0 /\ -c2^post13+c2^0 == 0 /\ 1-z^post13 <= 0 /\ c1^0-c1^post13 == 0 /\ pattern^post13 == 0 /\ xx^post13 == 0 /\ buffer^0-buffer^post13 == 0 /\ it^post13-seqlen^post13 == 0 /\ yy^post13 == 0), cost: 1
  14: l10 -> l6 : pattern^0'=pattern^post14, c1^0'=c1^post14, xx^0'=xx^post14, it^0'=it^post14, buffer^0'=buffer^post14, z^0'=z^post14, seqlen^0'=seqlen^post14, c2^0'=c2^post14, yy^0'=yy^post14, (-seqlen^post14+seqlen^0 == 0 /\ -buffer^0+c1^post14 == 0 /\ -buffer^post14+buffer^0 == 0 /\ pattern^0-pattern^post14 == 0 /\ xx^0-xx^post14 == 0 /\ -c2^post14+c2^0 == 0 /\ it^0-it^post14 == 0 /\ -yy^post14+yy^0 == 0 /\ -z^post14+z^0 == 0), cost: 1
  15: l11 -> l10 : pattern^0'=pattern^post15, c1^0'=c1^post15, xx^0'=xx^post15, it^0'=it^post15, buffer^0'=buffer^post15, z^0'=z^post15, seqlen^0'=seqlen^post15, c2^0'=c2^post15, yy^0'=yy^post15, (-2+buffer^0 <= 0 /\ pattern^0-pattern^post15 == 0 /\ xx^0-xx^post15 == 0 /\ it^0-it^post15 == 0 /\ -buffer^post15+buffer^0 == 0 /\ -seqlen^post15+seqlen^0 == 0 /\ -yy^post15+yy^0 == 0 /\ -z^post15+z^0 == 0 /\ c1^0-c1^post15 == 0 /\ c2^post15 == 0), cost: 1
  16: l11 -> l10 : pattern^0'=pattern^post16, c1^0'=c1^post16, xx^0'=xx^post16, it^0'=it^post16, buffer^0'=buffer^post16, z^0'=z^post16, seqlen^0'=seqlen^post16, c2^0'=c2^post16, yy^0'=yy^post16, (c1^0-c1^post16 == 0 /\ -z^post16+z^0 == 0 /\ -xx^post16+xx^0 == 0 /\ seqlen^0-seqlen^post16 == 0 /\ -1+c2^post16 == 0 /\ 2+buffer^post16-buffer^0 == 0 /\ -yy^post16+yy^0 == 0 /\ pattern^0-pattern^post16 == 0 /\ 3-buffer^0 <= 0 /\ it^0-it^post16 == 0), cost: 1
  17: l12 -> l8 : pattern^0'=pattern^post17, c1^0'=c1^post17, xx^0'=xx^post17, it^0'=it^post17, buffer^0'=buffer^post17, z^0'=z^post17, seqlen^0'=seqlen^post17, c2^0'=c2^post17, yy^0'=yy^post17, (-xx^post17+xx^0 == 0 /\ buffer^0-buffer^post17 == 0 /\ z^0-z^post17 == 0 /\ -yy^post17+yy^0 == 0 /\ it^0 <= 0 /\ -seqlen^post17+seqlen^0 == 0 /\ c1^0-c1^post17 == 0 /\ -it^post17+it^0 == 0 /\ -c2^post17+c2^0 == 0 /\ pattern^0-pattern^post17 == 0), cost: 1
  18: l12 -> l11 : pattern^0'=pattern^post18, c1^0'=c1^post18, xx^0'=xx^post18, it^0'=it^post18, buffer^0'=buffer^post18, z^0'=z^post18, seqlen^0'=seqlen^post18, c2^0'=c2^post18, yy^0'=yy^post18, (1-it^0 <= 0 /\ c1^0-c1^post18 == 0 /\ -yy^post18+yy^0 == 0 /\ -seqlen^post18+seqlen^0 == 0 /\ pattern^0-pattern^post18 == 0 /\ 1-it^0+it^post18 == 0 /\ z^0-z^post18 == 0 /\ -pattern^0+buffer^post18 == 0 /\ xx^0-xx^post18 == 0 /\ -c2^post18+c2^0 == 0), cost: 1
  20: l15 -> l5 : pattern^0'=pattern^post20, c1^0'=c1^post20, xx^0'=xx^post20, it^0'=it^post20, buffer^0'=buffer^post20, z^0'=z^post20, seqlen^0'=seqlen^post20, c2^0'=c2^post20, yy^0'=yy^post20, (it^0-it^post20 == 0 /\ -buffer^post20+buffer^0 == 0 /\ c1^0-c1^post20 == 0 /\ -xx^post20+xx^0 == 0 /\ -yy^post20+yy^0 == 0 /\ -c2^post20+c2^0 == 0 /\ pattern^0-pattern^post20 == 0 /\ -z^post20+z^0 == 0 /\ 1-z^0 <= 0 /\ seqlen^0-seqlen^post20 == 0), cost: 1
  21: l15 -> l5 : pattern^0'=pattern^post21, c1^0'=c1^post21, xx^0'=xx^post21, it^0'=it^post21, buffer^0'=buffer^post21, z^0'=z^post21, seqlen^0'=seqlen^post21, c2^0'=c2^post21, yy^0'=yy^post21, (z^0-z^post21 == 0 /\ 1+z^0 <= 0 /\ pattern^0-pattern^post21 == 0 /\ -it^post21+it^0 == 0 /\ -c2^post21+c2^0 == 0 /\ buffer^0-buffer^post21 == 0 /\ -xx^post21+xx^0 == 0 /\ c1^0-c1^post21 == 0 /\ -yy^post21+yy^0 == 0 /\ -seqlen^post21+seqlen^0 == 0), cost: 1
  22: l15 -> l12 : pattern^0'=pattern^post22, c1^0'=c1^post22, xx^0'=xx^post22, it^0'=it^post22, buffer^0'=buffer^post22, z^0'=z^post22, seqlen^0'=seqlen^post22, c2^0'=c2^post22, yy^0'=yy^post22, (buffer^0-buffer^post22 == 0 /\ -xx^post22+xx^0 == 0 /\ -it^post22+it^0 == 0 /\ -yy^post22+yy^0 == 0 /\ z^0-z^post22 == 0 /\ -seqlen^post22+seqlen^0 == 0 /\ c1^0-c1^post22 == 0 /\ z^0 <= 0 /\ pattern^0-pattern^post22 == 0 /\ -z^0 <= 0 /\ -c2^post22+c2^0 == 0), cost: 1
  26: l16 -> l9 : pattern^0'=pattern^post26, c1^0'=c1^post26, xx^0'=xx^post26, it^0'=it^post26, buffer^0'=buffer^post26, z^0'=z^post26, seqlen^0'=seqlen^post26, c2^0'=c2^post26, yy^0'=yy^post26, (c1^0-c1^post26 == 0 /\ -xx^post26+xx^0 == 0 /\ pattern^0-pattern^post26 == 0 /\ -yy^post26+yy^0 == 0 /\ seqlen^0-seqlen^post26 == 0 /\ -z^post26+z^0 == 0 /\ -c2^post26+c2^0 == 0 /\ it^0-it^post26 == 0 /\ -buffer^post26+buffer^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : pattern^0'=pattern^post0, c1^0'=c1^post0, xx^0'=xx^post0, it^0'=it^post0, buffer^0'=buffer^post0, z^0'=z^post0, seqlen^0'=seqlen^post0, c2^0'=c2^post0, yy^0'=yy^post0, (buffer^0-buffer^post0 == 0 /\ -yy^post0+yy^0 == 0 /\ z^0-z^post0 == 0 /\ xx^0-xx^post0 == 0 /\ pattern^0-pattern^post0 == 0 /\ c1^0-c1^post0 == 0 /\ -c2^post0+c2^0 == 0 /\ -seqlen^post0+seqlen^0 == 0 /\ it^0-it^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : pattern^0'=pattern^post1, c1^0'=c1^post1, xx^0'=xx^post1, it^0'=it^post1, buffer^0'=buffer^post1, z^0'=z^post1, seqlen^0'=seqlen^post1, c2^0'=c2^post1, yy^0'=yy^post1, (-c2^post1+c2^0 == 0 /\ -seqlen^post1+seqlen^0 == 0 /\ -1+yy^post1 == 0 /\ pattern^0-pattern^post1 == 0 /\ xx^0-xx^post1 == 0 /\ -c1^post1+c1^0 == 0 /\ -z^post1+z^0 == 0 /\ -buffer^post1+buffer^0 == 0 /\ it^0-it^post1 == 0), cost: 1
New rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : pattern^0'=pattern^post2, c1^0'=c1^post2, xx^0'=xx^post2, it^0'=it^post2, buffer^0'=buffer^post2, z^0'=z^post2, seqlen^0'=seqlen^post2, c2^0'=c2^post2, yy^0'=yy^post2, (-1+xx^post2 == 0 /\ c1^0-c1^post2 == 0 /\ c2^0-c2^post2 == 0 /\ -yy^post2+yy^0 == 0 /\ it^0-it^post2 == 0 /\ -z^post2+z^0 == 0 /\ pattern^0-pattern^post2 == 0 /\ seqlen^0-seqlen^post2 == 0 /\ -buffer^post2+buffer^0 == 0), cost: 1
New rule:
l3 -> l4 : xx^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : pattern^0'=pattern^post3, c1^0'=c1^post3, xx^0'=xx^post3, it^0'=it^post3, buffer^0'=buffer^post3, z^0'=z^post3, seqlen^0'=seqlen^post3, c2^0'=c2^post3, yy^0'=yy^post3, (-c2^post3+c2^0 == 0 /\ -seqlen^post3+seqlen^0 == 0 /\ -yy^post3+yy^0 == 0 /\ -it^post3+it^0 == 0 /\ buffer^0-buffer^post3 == 0 /\ pattern^0-pattern^post3 == 0 /\ 1-c2^0 <= 0 /\ -xx^post3+xx^0 == 0 /\ c1^0-c1^post3 == 0 /\ -z^post3+z^0 == 0), cost: 1
New rule:
l4 -> l2 : -1+c2^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : pattern^0'=pattern^post4, c1^0'=c1^post4, xx^0'=xx^post4, it^0'=it^post4, buffer^0'=buffer^post4, z^0'=z^post4, seqlen^0'=seqlen^post4, c2^0'=c2^post4, yy^0'=yy^post4, (pattern^0-pattern^post4 == 0 /\ -seqlen^post4+seqlen^0 == 0 /\ -xx^post4+xx^0 == 0 /\ z^0-z^post4 == 0 /\ -it^post4+it^0 == 0 /\ -c2^post4+c2^0 == 0 /\ -yy^post4+yy^0 == 0 /\ 1+c2^0 <= 0 /\ buffer^0-buffer^post4 == 0 /\ c1^0-c1^post4 == 0), cost: 1
New rule:
l4 -> l2 : 1+c2^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l0 : pattern^0'=pattern^post5, c1^0'=c1^post5, xx^0'=xx^post5, it^0'=it^post5, buffer^0'=buffer^post5, z^0'=z^post5, seqlen^0'=seqlen^post5, c2^0'=c2^post5, yy^0'=yy^post5, (-it^post5+it^0 == 0 /\ -c1^post5+c1^0 == 0 /\ -c2^0 <= 0 /\ z^0-z^post5 == 0 /\ -c2^post5+c2^0 == 0 /\ pattern^0-pattern^post5 == 0 /\ xx^0-xx^post5 == 0 /\ c2^0 <= 0 /\ -seqlen^post5+seqlen^0 == 0 /\ yy^post5 == 0 /\ buffer^0-buffer^post5 == 0), cost: 1
New rule:
l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : pattern^0'=pattern^post6, c1^0'=c1^post6, xx^0'=xx^post6, it^0'=it^post6, buffer^0'=buffer^post6, z^0'=z^post6, seqlen^0'=seqlen^post6, c2^0'=c2^post6, yy^0'=yy^post6, (0 == 0 /\ xx^0-xx^post6 == 0 /\ 1+z^post6-z^0 == 0 /\ -yy^post6+yy^0 == 0 /\ it^0-it^post6 == 0 /\ pattern^0-pattern^post6 == 0 /\ seqlen^0-seqlen^post6 == 0 /\ -buffer^post6+buffer^0 == 0), cost: 1
New rule:
l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l6 : pattern^0'=pattern^post7, c1^0'=c1^post7, xx^0'=xx^post7, it^0'=it^post7, buffer^0'=buffer^post7, z^0'=z^post7, seqlen^0'=seqlen^post7, c2^0'=c2^post7, yy^0'=yy^post7, (0 == 0 /\ -1-seqlen^0+seqlen^post7 == 0 /\ c1^0-c1^post7 == 0 /\ -xx^post7+xx^0 == 0 /\ -buffer^post7+buffer^0 == 0 /\ -c2^post7+c2^0 == 0 /\ 1-z^post7 <= 0 /\ -yy^post7+yy^0 == 0 /\ -pattern^post7+pattern^0 == 0 /\ it^post7-seqlen^post7 == 0), cost: 1
New rule:
l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : pattern^0'=pattern^post8, c1^0'=c1^post8, xx^0'=xx^post8, it^0'=it^post8, buffer^0'=buffer^post8, z^0'=z^post8, seqlen^0'=seqlen^post8, c2^0'=c2^post8, yy^0'=yy^post8, (-c2^post8+c2^0 == 0 /\ -2+pattern^0 <= 0 /\ -yy^post8+yy^0 == 0 /\ c1^0-c1^post8 == 0 /\ buffer^0-buffer^post8 == 0 /\ seqlen^0-seqlen^post8 == 0 /\ -it^post8+it^0 == 0 /\ -xx^post8+xx^0 == 0 /\ -z^post8+z^0 == 0 /\ -1-pattern^0+pattern^post8 == 0), cost: 1
New rule:
l8 -> l7 : pattern^0'=1+pattern^0, -2+pattern^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : pattern^0'=pattern^post9, c1^0'=c1^post9, xx^0'=xx^post9, it^0'=it^post9, buffer^0'=buffer^post9, z^0'=z^post9, seqlen^0'=seqlen^post9, c2^0'=c2^post9, yy^0'=yy^post9, (-yy^post9+yy^0 == 0 /\ -c2^post9+c2^0 == 0 /\ buffer^0-buffer^post9 == 0 /\ -seqlen^post9+seqlen^0 == 0 /\ z^0-z^post9 == 0 /\ xx^0-xx^post9 == 0 /\ -it^post9+it^0 == 0 /\ pattern^post9 == 0 /\ 3-pattern^0 <= 0 /\ -c1^post9+c1^0 == 0), cost: 1
New rule:
l8 -> l7 : pattern^0'=0, -3+pattern^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l3 : pattern^0'=pattern^post10, c1^0'=c1^post10, xx^0'=xx^post10, it^0'=it^post10, buffer^0'=buffer^post10, z^0'=z^post10, seqlen^0'=seqlen^post10, c2^0'=c2^post10, yy^0'=yy^post10, (xx^0-xx^post10 == 0 /\ -yy^post10+yy^0 == 0 /\ it^0-it^post10 == 0 /\ -z^post10+z^0 == 0 /\ c2^0-c2^post10 == 0 /\ c1^0-c1^post10 == 0 /\ -seqlen^post10+seqlen^0 == 0 /\ -buffer^post10+buffer^0 == 0 /\ 1-c1^0 <= 0 /\ pattern^0-pattern^post10 == 0), cost: 1
New rule:
l6 -> l3 : -1+c1^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l3 : pattern^0'=pattern^post11, c1^0'=c1^post11, xx^0'=xx^post11, it^0'=it^post11, buffer^0'=buffer^post11, z^0'=z^post11, seqlen^0'=seqlen^post11, c2^0'=c2^post11, yy^0'=yy^post11, (c2^0-c2^post11 == 0 /\ -z^post11+z^0 == 0 /\ 1+c1^0 <= 0 /\ seqlen^0-seqlen^post11 == 0 /\ -yy^post11+yy^0 == 0 /\ c1^0-c1^post11 == 0 /\ -buffer^post11+buffer^0 == 0 /\ it^0-it^post11 == 0 /\ pattern^0-pattern^post11 == 0 /\ xx^0-xx^post11 == 0), cost: 1
New rule:
l6 -> l3 : 1+c1^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l4 : pattern^0'=pattern^post12, c1^0'=c1^post12, xx^0'=xx^post12, it^0'=it^post12, buffer^0'=buffer^post12, z^0'=z^post12, seqlen^0'=seqlen^post12, c2^0'=c2^post12, yy^0'=yy^post12, (-yy^post12+yy^0 == 0 /\ c1^0-c1^post12 == 0 /\ c1^0 <= 0 /\ xx^post12 == 0 /\ -c2^post12+c2^0 == 0 /\ buffer^0-buffer^post12 == 0 /\ seqlen^0-seqlen^post12 == 0 /\ -it^post12+it^0 == 0 /\ pattern^0-pattern^post12 == 0 /\ -c1^0 <= 0 /\ -z^post12+z^0 == 0), cost: 1
New rule:
l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l0 : pattern^0'=pattern^post13, c1^0'=c1^post13, xx^0'=xx^post13, it^0'=it^post13, buffer^0'=buffer^post13, z^0'=z^post13, seqlen^0'=seqlen^post13, c2^0'=c2^post13, yy^0'=yy^post13, (0 == 0 /\ -1+seqlen^post13 == 0 /\ -c2^post13+c2^0 == 0 /\ 1-z^post13 <= 0 /\ c1^0-c1^post13 == 0 /\ pattern^post13 == 0 /\ xx^post13 == 0 /\ buffer^0-buffer^post13 == 0 /\ it^post13-seqlen^post13 == 0 /\ yy^post13 == 0), cost: 1
New rule:
l9 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l6 : pattern^0'=pattern^post14, c1^0'=c1^post14, xx^0'=xx^post14, it^0'=it^post14, buffer^0'=buffer^post14, z^0'=z^post14, seqlen^0'=seqlen^post14, c2^0'=c2^post14, yy^0'=yy^post14, (-seqlen^post14+seqlen^0 == 0 /\ -buffer^0+c1^post14 == 0 /\ -buffer^post14+buffer^0 == 0 /\ pattern^0-pattern^post14 == 0 /\ xx^0-xx^post14 == 0 /\ -c2^post14+c2^0 == 0 /\ it^0-it^post14 == 0 /\ -yy^post14+yy^0 == 0 /\ -z^post14+z^0 == 0), cost: 1
New rule:
l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : pattern^0'=pattern^post15, c1^0'=c1^post15, xx^0'=xx^post15, it^0'=it^post15, buffer^0'=buffer^post15, z^0'=z^post15, seqlen^0'=seqlen^post15, c2^0'=c2^post15, yy^0'=yy^post15, (-2+buffer^0 <= 0 /\ pattern^0-pattern^post15 == 0 /\ xx^0-xx^post15 == 0 /\ it^0-it^post15 == 0 /\ -buffer^post15+buffer^0 == 0 /\ -seqlen^post15+seqlen^0 == 0 /\ -yy^post15+yy^0 == 0 /\ -z^post15+z^0 == 0 /\ c1^0-c1^post15 == 0 /\ c2^post15 == 0), cost: 1
New rule:
l11 -> l10 : c2^0'=0, -2+buffer^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l10 : pattern^0'=pattern^post16, c1^0'=c1^post16, xx^0'=xx^post16, it^0'=it^post16, buffer^0'=buffer^post16, z^0'=z^post16, seqlen^0'=seqlen^post16, c2^0'=c2^post16, yy^0'=yy^post16, (c1^0-c1^post16 == 0 /\ -z^post16+z^0 == 0 /\ -xx^post16+xx^0 == 0 /\ seqlen^0-seqlen^post16 == 0 /\ -1+c2^post16 == 0 /\ 2+buffer^post16-buffer^0 == 0 /\ -yy^post16+yy^0 == 0 /\ pattern^0-pattern^post16 == 0 /\ 3-buffer^0 <= 0 /\ it^0-it^post16 == 0), cost: 1
New rule:
l11 -> l10 : buffer^0'=-2+buffer^0, c2^0'=1, -3+buffer^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l8 : pattern^0'=pattern^post17, c1^0'=c1^post17, xx^0'=xx^post17, it^0'=it^post17, buffer^0'=buffer^post17, z^0'=z^post17, seqlen^0'=seqlen^post17, c2^0'=c2^post17, yy^0'=yy^post17, (-xx^post17+xx^0 == 0 /\ buffer^0-buffer^post17 == 0 /\ z^0-z^post17 == 0 /\ -yy^post17+yy^0 == 0 /\ it^0 <= 0 /\ -seqlen^post17+seqlen^0 == 0 /\ c1^0-c1^post17 == 0 /\ -it^post17+it^0 == 0 /\ -c2^post17+c2^0 == 0 /\ pattern^0-pattern^post17 == 0), cost: 1
New rule:
l12 -> l8 : it^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : pattern^0'=pattern^post18, c1^0'=c1^post18, xx^0'=xx^post18, it^0'=it^post18, buffer^0'=buffer^post18, z^0'=z^post18, seqlen^0'=seqlen^post18, c2^0'=c2^post18, yy^0'=yy^post18, (1-it^0 <= 0 /\ c1^0-c1^post18 == 0 /\ -yy^post18+yy^0 == 0 /\ -seqlen^post18+seqlen^0 == 0 /\ pattern^0-pattern^post18 == 0 /\ 1-it^0+it^post18 == 0 /\ z^0-z^post18 == 0 /\ -pattern^0+buffer^post18 == 0 /\ xx^0-xx^post18 == 0 /\ -c2^post18+c2^0 == 0), cost: 1
New rule:
l12 -> l11 : it^0'=-1+it^0, buffer^0'=pattern^0, -1+it^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l5 : pattern^0'=pattern^post20, c1^0'=c1^post20, xx^0'=xx^post20, it^0'=it^post20, buffer^0'=buffer^post20, z^0'=z^post20, seqlen^0'=seqlen^post20, c2^0'=c2^post20, yy^0'=yy^post20, (it^0-it^post20 == 0 /\ -buffer^post20+buffer^0 == 0 /\ c1^0-c1^post20 == 0 /\ -xx^post20+xx^0 == 0 /\ -yy^post20+yy^0 == 0 /\ -c2^post20+c2^0 == 0 /\ pattern^0-pattern^post20 == 0 /\ -z^post20+z^0 == 0 /\ 1-z^0 <= 0 /\ seqlen^0-seqlen^post20 == 0), cost: 1
New rule:
l15 -> l5 : -1+z^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l5 : pattern^0'=pattern^post21, c1^0'=c1^post21, xx^0'=xx^post21, it^0'=it^post21, buffer^0'=buffer^post21, z^0'=z^post21, seqlen^0'=seqlen^post21, c2^0'=c2^post21, yy^0'=yy^post21, (z^0-z^post21 == 0 /\ 1+z^0 <= 0 /\ pattern^0-pattern^post21 == 0 /\ -it^post21+it^0 == 0 /\ -c2^post21+c2^0 == 0 /\ buffer^0-buffer^post21 == 0 /\ -xx^post21+xx^0 == 0 /\ c1^0-c1^post21 == 0 /\ -yy^post21+yy^0 == 0 /\ -seqlen^post21+seqlen^0 == 0), cost: 1
New rule:
l15 -> l5 : 1+z^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l15 -> l12 : pattern^0'=pattern^post22, c1^0'=c1^post22, xx^0'=xx^post22, it^0'=it^post22, buffer^0'=buffer^post22, z^0'=z^post22, seqlen^0'=seqlen^post22, c2^0'=c2^post22, yy^0'=yy^post22, (buffer^0-buffer^post22 == 0 /\ -xx^post22+xx^0 == 0 /\ -it^post22+it^0 == 0 /\ -yy^post22+yy^0 == 0 /\ z^0-z^post22 == 0 /\ -seqlen^post22+seqlen^0 == 0 /\ c1^0-c1^post22 == 0 /\ z^0 <= 0 /\ pattern^0-pattern^post22 == 0 /\ -z^0 <= 0 /\ -c2^post22+c2^0 == 0), cost: 1
New rule:
l15 -> l12 : z^0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l15 : pattern^0'=pattern^post25, c1^0'=c1^post25, xx^0'=xx^post25, it^0'=it^post25, buffer^0'=buffer^post25, z^0'=z^post25, seqlen^0'=seqlen^post25, c2^0'=c2^post25, yy^0'=yy^post25, (-z^post25+z^0 == 0 /\ it^0-it^post25 == 0 /\ -c2^post25+c2^0 == 0 /\ -buffer^post25+buffer^0 == 0 /\ pattern^0-pattern^post25 == 0 /\ c1^0-c1^post25 == 0 /\ seqlen^0-seqlen^post25 == 0 /\ -xx^0+yy^0 <= 0 /\ -yy^post25+yy^0 == 0 /\ xx^0-yy^0 <= 0 /\ xx^0-xx^post25 == 0), cost: 1
New rule:
l1 -> l15 : -xx^0+yy^0 == 0, cost: 1

Applied preprocessing
Original rule:
l16 -> l9 : pattern^0'=pattern^post26, c1^0'=c1^post26, xx^0'=xx^post26, it^0'=it^post26, buffer^0'=buffer^post26, z^0'=z^post26, seqlen^0'=seqlen^post26, c2^0'=c2^post26, yy^0'=yy^post26, (c1^0-c1^post26 == 0 /\ -xx^post26+xx^0 == 0 /\ pattern^0-pattern^post26 == 0 /\ -yy^post26+yy^0 == 0 /\ seqlen^0-seqlen^post26 == 0 /\ -z^post26+z^0 == 0 /\ -c2^post26+c2^0 == 0 /\ it^0-it^post26 == 0 /\ -buffer^post26+buffer^0 == 0), cost: 1
New rule:
l16 -> l9 : TRUE, cost: 1

Simplified rules
Start location: l16
  27: l0 -> l1 : TRUE, cost: 1
  49: l1 -> l15 : -xx^0+yy^0 == 0, cost: 1
  28: l2 -> l0 : yy^0'=1, TRUE, cost: 1
  29: l3 -> l4 : xx^0'=1, TRUE, cost: 1
  30: l4 -> l2 : -1+c2^0 >= 0, cost: 1
  31: l4 -> l2 : 1+c2^0 <= 0, cost: 1
  32: l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1
  33: l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1
  37: l6 -> l3 : -1+c1^0 >= 0, cost: 1
  38: l6 -> l3 : 1+c1^0 <= 0, cost: 1
  39: l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1
  34: l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
  35: l8 -> l7 : pattern^0'=1+pattern^0, -2+pattern^0 <= 0, cost: 1
  36: l8 -> l7 : pattern^0'=0, -3+pattern^0 >= 0, cost: 1
  40: l9 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 1
  41: l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
  42: l11 -> l10 : c2^0'=0, -2+buffer^0 <= 0, cost: 1
  43: l11 -> l10 : buffer^0'=-2+buffer^0, c2^0'=1, -3+buffer^0 >= 0, cost: 1
  44: l12 -> l8 : it^0 <= 0, cost: 1
  45: l12 -> l11 : it^0'=-1+it^0, buffer^0'=pattern^0, -1+it^0 >= 0, cost: 1
  46: l15 -> l5 : -1+z^0 >= 0, cost: 1
  47: l15 -> l5 : 1+z^0 <= 0, cost: 1
  48: l15 -> l12 : z^0 == 0, cost: 1
  50: l16 -> l9 : TRUE, cost: 1


Eliminating location l9 by chaining:

Applied chaining
First rule:
l16 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 1
New rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2

Applied deletion
Removed the following rules: 40 50

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l15 : -xx^0+yy^0 == 0, cost: 1
New rule:
l0 -> l15 : -xx^0+yy^0 == 0, cost: 2

Applied deletion
Removed the following rules: 27 49

Eliminated locations on linear paths
Start location: l16
  52: l0 -> l15 : -xx^0+yy^0 == 0, cost: 2
  28: l2 -> l0 : yy^0'=1, TRUE, cost: 1
  29: l3 -> l4 : xx^0'=1, TRUE, cost: 1
  30: l4 -> l2 : -1+c2^0 >= 0, cost: 1
  31: l4 -> l2 : 1+c2^0 <= 0, cost: 1
  32: l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1
  33: l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1
  37: l6 -> l3 : -1+c1^0 >= 0, cost: 1
  38: l6 -> l3 : 1+c1^0 <= 0, cost: 1
  39: l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1
  34: l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
  35: l8 -> l7 : pattern^0'=1+pattern^0, -2+pattern^0 <= 0, cost: 1
  36: l8 -> l7 : pattern^0'=0, -3+pattern^0 >= 0, cost: 1
  41: l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
  42: l11 -> l10 : c2^0'=0, -2+buffer^0 <= 0, cost: 1
  43: l11 -> l10 : buffer^0'=-2+buffer^0, c2^0'=1, -3+buffer^0 >= 0, cost: 1
  44: l12 -> l8 : it^0 <= 0, cost: 1
  45: l12 -> l11 : it^0'=-1+it^0, buffer^0'=pattern^0, -1+it^0 >= 0, cost: 1
  46: l15 -> l5 : -1+z^0 >= 0, cost: 1
  47: l15 -> l5 : 1+z^0 <= 0, cost: 1
  48: l15 -> l12 : z^0 == 0, cost: 1
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Eliminating location l15 by chaining:

Applied chaining
First rule:
l0 -> l15 : -xx^0+yy^0 == 0, cost: 2
Second rule:
l15 -> l5 : -1+z^0 >= 0, cost: 1
New rule:
l0 -> l5 : (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 3

Applied chaining
First rule:
l0 -> l15 : -xx^0+yy^0 == 0, cost: 2
Second rule:
l15 -> l5 : 1+z^0 <= 0, cost: 1
New rule:
l0 -> l5 : (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 3

Applied chaining
First rule:
l0 -> l15 : -xx^0+yy^0 == 0, cost: 2
Second rule:
l15 -> l12 : z^0 == 0, cost: 1
New rule:
l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3

Applied deletion
Removed the following rules: 46 47 48 52

Eliminating location l3 by chaining:

Applied chaining
First rule:
l6 -> l3 : -1+c1^0 >= 0, cost: 1
Second rule:
l3 -> l4 : xx^0'=1, TRUE, cost: 1
New rule:
l6 -> l4 : xx^0'=1, -1+c1^0 >= 0, cost: 2

Applied chaining
First rule:
l6 -> l3 : 1+c1^0 <= 0, cost: 1
Second rule:
l3 -> l4 : xx^0'=1, TRUE, cost: 1
New rule:
l6 -> l4 : xx^0'=1, 1+c1^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 29 37 38

Eliminating location l4 by chaining:

Applied chaining
First rule:
l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1
Second rule:
l4 -> l2 : -1+c2^0 >= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 2

Applied chaining
First rule:
l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1
Second rule:
l4 -> l2 : 1+c2^0 <= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 2

Applied chaining
First rule:
l6 -> l4 : xx^0'=0, c1^0 == 0, cost: 1
Second rule:
l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1
New rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, -1+c1^0 >= 0, cost: 2
Second rule:
l4 -> l2 : -1+c2^0 >= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 3

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, -1+c1^0 >= 0, cost: 2
Second rule:
l4 -> l2 : 1+c2^0 <= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 3

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, -1+c1^0 >= 0, cost: 2
Second rule:
l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, 1+c1^0 <= 0, cost: 2
Second rule:
l4 -> l2 : -1+c2^0 >= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 3

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, 1+c1^0 <= 0, cost: 2
Second rule:
l4 -> l2 : 1+c2^0 <= 0, cost: 1
New rule:
l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 3

Applied chaining
First rule:
l6 -> l4 : xx^0'=1, 1+c1^0 <= 0, cost: 2
Second rule:
l4 -> l0 : yy^0'=0, c2^0 == 0, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3

Applied deletion
Removed the following rules: 30 31 32 39 56 57

Eliminating location l8 by chaining:

Applied chaining
First rule:
l12 -> l8 : it^0 <= 0, cost: 1
Second rule:
l8 -> l7 : pattern^0'=1+pattern^0, -2+pattern^0 <= 0, cost: 1
New rule:
l12 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0), cost: 2

Applied chaining
First rule:
l12 -> l8 : it^0 <= 0, cost: 1
Second rule:
l8 -> l7 : pattern^0'=0, -3+pattern^0 >= 0, cost: 1
New rule:
l12 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 35 36 44

Eliminating location l11 by chaining:

Applied chaining
First rule:
l12 -> l11 : it^0'=-1+it^0, buffer^0'=pattern^0, -1+it^0 >= 0, cost: 1
Second rule:
l11 -> l10 : c2^0'=0, -2+buffer^0 <= 0, cost: 1
New rule:
l12 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0), cost: 2

Applied chaining
First rule:
l12 -> l11 : it^0'=-1+it^0, buffer^0'=pattern^0, -1+it^0 >= 0, cost: 1
Second rule:
l11 -> l10 : buffer^0'=-2+buffer^0, c2^0'=1, -3+buffer^0 >= 0, cost: 1
New rule:
l12 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 42 43 45

Eliminated locations on tree-shaped paths
Start location: l16
  53: l0 -> l5 : (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 3
  54: l0 -> l5 : (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 3
  55: l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3
  28: l2 -> l0 : yy^0'=1, TRUE, cost: 1
  33: l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1
  58: l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 2
  59: l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 2
  60: l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
  61: l6 -> l2 : xx^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 3
  62: l6 -> l2 : xx^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 3
  63: l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
  64: l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 3
  65: l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 3
  66: l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
  34: l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
  41: l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
  67: l12 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0), cost: 2
  68: l12 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0), cost: 2
  69: l12 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0), cost: 2
  70: l12 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0), cost: 2
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Eliminating location l5 by chaining:

Applied chaining
First rule:
l0 -> l5 : (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 3
Second rule:
l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1
New rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4

Applied simplification
Original rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
New rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4

Applied chaining
First rule:
l0 -> l5 : (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 3
Second rule:
l5 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, 0 == 0, cost: 1
New rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (0 == 0 /\ 1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4

Applied simplification
Original rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (0 == 0 /\ 1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
New rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4

Applied deletion
Removed the following rules: 33 53 54

Eliminating location l12 by chaining:

Applied chaining
First rule:
l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3
Second rule:
l12 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0), cost: 2
New rule:
l0 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5

Applied chaining
First rule:
l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3
Second rule:
l12 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0), cost: 2
New rule:
l0 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5

Applied chaining
First rule:
l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3
Second rule:
l12 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0), cost: 2
New rule:
l0 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5

Applied chaining
First rule:
l0 -> l12 : (z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 3
Second rule:
l12 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0), cost: 2
New rule:
l0 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5

Applied deletion
Removed the following rules: 55 67 68 69 70

Eliminating location l2 by chaining:

Applied chaining
First rule:
l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 2
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3

Applied chaining
First rule:
l6 -> l2 : xx^0'=0, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 2
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3

Applied chaining
First rule:
l6 -> l2 : xx^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 3
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4

Applied chaining
First rule:
l6 -> l2 : xx^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 3
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4

Applied chaining
First rule:
l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 3
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4

Applied chaining
First rule:
l6 -> l2 : xx^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 3
Second rule:
l2 -> l0 : yy^0'=1, TRUE, cost: 1
New rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4

Applied deletion
Removed the following rules: 28 58 59 61 62 64 65

Eliminated locations on tree-shaped paths
Start location: l16
  71: l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
  72: l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
  73: l0 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
  74: l0 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
  75: l0 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
  76: l0 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
  60: l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
  63: l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
  66: l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
  77: l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
  78: l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
  79: l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
  80: l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
  81: l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
  82: l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
  34: l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
  41: l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Eliminating location l7 by chaining:

Applied chaining
First rule:
l0 -> l7 : pattern^0'=1+pattern^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
Second rule:
l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
New rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6

Applied chaining
First rule:
l0 -> l7 : pattern^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
Second rule:
l7 -> l6 : it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, -1+z^post7 >= 0, cost: 1
New rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6

Applied deletion
Removed the following rules: 34 73 74

Eliminating location l10 by chaining:

Applied chaining
First rule:
l0 -> l10 : it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
Second rule:
l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
New rule:
l0 -> l6 : c1^0'=pattern^0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6

Applied chaining
First rule:
l0 -> l10 : it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 5
Second rule:
l10 -> l6 : c1^0'=buffer^0, TRUE, cost: 1
New rule:
l0 -> l6 : c1^0'=-2+pattern^0, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6

Applied deletion
Removed the following rules: 41 75 76

Eliminated locations on tree-shaped paths
Start location: l16
  71: l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
  72: l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
  83: l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
  84: l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
  85: l0 -> l6 : c1^0'=pattern^0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
  86: l0 -> l6 : c1^0'=-2+pattern^0, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
  60: l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
  63: l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
  66: l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
  77: l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
  78: l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
  79: l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
  80: l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
  81: l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
  82: l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Eliminating location l6 by chaining:

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=c1^post6, z^0'=-1+z^0, c2^0'=c2^post6, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 4
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=1+pattern^0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ -1+c2^0 >= 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=1, (c1^0 == 0 /\ 1+c2^0 <= 0), cost: 3
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c1^0 >= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ -1+c2^0 >= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : pattern^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (1+c1^0 <= 0 /\ 1+c2^0 <= 0), cost: 4
New rule:
l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied chaining
First rule:
l0 -> l6 : c1^0'=pattern^0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=0, yy^0'=0, (c1^0 == 0 /\ c2^0 == 0), cost: 2
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ pattern^0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8

Applied simplification
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ pattern^0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 == 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8

Applied chaining
First rule:
l0 -> l6 : c1^0'=pattern^0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (-1+c1^0 >= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9

Applied simplification
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : c1^0'=pattern^0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=0, (1+c1^0 <= 0 /\ c2^0 == 0), cost: 3
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied simplification
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 == 0 /\ -2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9

Applied chaining
First rule:
l0 -> l6 : c1^0'=-2+pattern^0, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l6 -> l0 : xx^0'=1, yy^0'=1, (-1+c2^0 >= 0 /\ -1+c1^0 >= 0), cost: 4
New rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (0 >= 0 /\ -1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied simplification
Original rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (0 >= 0 /\ -1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10
New rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10

Applied deletion
Removed the following rules: 60 63 66 71 72 77 78 79 80 81 82 83 84 85 86

Eliminated locations on tree-shaped paths
Start location: l16
  87: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6
  88: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7
  89: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7
  90: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0), cost: 7
  91: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7
  92: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
  93: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
  94: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
  95: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
  96: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6
  97: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7
  98: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7
  99: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0), cost: 7
 100: l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7
 101: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
 102: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
 103: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
 104: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
 105: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 106: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 107: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 108: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 109: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 110: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 111: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 112: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 113: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 114: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 115: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 116: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 117: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 118: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 119: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 120: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 121: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 122: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 123: l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 == 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8
 124: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9
 125: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9
 126: l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 6

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c2^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ c2^post6 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ c2^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0), cost: 7
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ c1^post6 == 0 /\ 1+c2^post6 <= 0), cost: 7
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 7

Simplified simple loops
Start location: l16
  92: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
  93: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
  94: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
  95: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
 101: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
 102: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
 103: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
 104: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
 105: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 106: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 107: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 108: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 109: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 110: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 111: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 112: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 113: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 114: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 115: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 116: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 117: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 118: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 119: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 120: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 121: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 122: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 123: l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 == 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8
 124: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9
 125: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9
 126: l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10
 127: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 6
 128: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 129: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 130: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 131: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 7
 132: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
 133: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7
 134: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 7
 135: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7
 136: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 7
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ z^0-n >= 0 /\ -1+n >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nEgOia.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ z^0-n >= 0 /\ -1+n >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ z^0-n0 >= 0 /\ -1+n0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bbaNAe.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ z^0-n0 >= 0 /\ -1+n0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n0
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n1, c2^0'=c2^post6, yy^0'=1, (z^0-n1 >= 0 /\ -1+n1 >= 0 /\ -1+c2^post6 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NiBdkh.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n1, c2^0'=c2^post6, yy^0'=1, (z^0-n1 >= 0 /\ -1+n1 >= 0 /\ -1+c2^post6 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n1
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c2^post6 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n2, c2^0'=c2^post6, yy^0'=1, (z^0-n2 >= 0 /\ -1+n2 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ONEMcM.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=z^0-n2, c2^0'=c2^post6, yy^0'=1, (z^0-n2 >= 0 /\ -1+n2 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n2
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n3 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_GocGnj.txt

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n4 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_GEJKPF.txt

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n5 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_GFniPn.txt

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mFcjMh.txt

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 == 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-n25+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 >= 0 /\ -n25+it^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n25 >= 0 /\ -pattern^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n25
Sub-proof via acceration calculus written to file:///tmp/tmpnam_fKhHJO.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=-n25+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 >= 0 /\ -n25+it^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n25 >= 0 /\ -pattern^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*n25
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 >= 0 /\ pattern^0 >= 0 /\ -1+it^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -pattern^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*it^0

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 10
New rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-n28+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-n28+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n28 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*n28
Sub-proof via acceration calculus written to file:///tmp/tmpnam_Jibokd.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=-n28+it^0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-n28+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n28 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*n28
New rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (0 >= 0 /\ -1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*it^0

Applied acceleration
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=z^0-n29, c2^0'=0, yy^0'=0, (-1+n29 >= 0 /\ z^0-n29 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*n29
Sub-proof via acceration calculus written to file:///tmp/tmpnam_eaEbLI.txt

Applied instantiation
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=z^0-n29, c2^0'=0, yy^0'=0, (-1+n29 >= 0 /\ z^0-n29 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*n29
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=0, c2^0'=0, yy^0'=0, (0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*z^0

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n34 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_AKcFbd.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n43 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cFHnmN.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n43 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ 1+c2^post6 <= 0 /\ -1-c2^post6 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_dDgPCO.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ADejKc.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ 1+c2^post6 <= 0 /\ -1-c2^post6 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-2+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EeNLgB.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n64 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_okKNpM.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n64 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ -1+n64 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 8
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_PEHNDA.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 8
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_Dkpbka.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 8
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14

Applied nonterm
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-2+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 14
New rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_OOAhfm.txt

Applied chaining
First rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0), cost: 6
Second rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1+c2^post6 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied simplification
Original rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (0 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n3 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n3 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n4 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n4 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n5 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n5 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (0 >= 0 /\ pattern^0 >= 0 /\ -1+it^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -pattern^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*it^0
New rule:
l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 <= 0 /\ pattern^0 >= 0 /\ -1+it^0 >= 0 /\ z^0 <= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*it^0

Applied simplification
Original rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (0 >= 0 /\ -1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*it^0
New rule:
l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 <= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*it^0

Applied simplification
Original rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=0, c2^0'=0, yy^0'=0, (0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*z^0
New rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*z^0

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n34 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n34 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n43 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ 1+c2^post6 <= 0 /\ -1-c2^post6 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -1-c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1-c2^post6 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ 1+c2^post6 <= 0 /\ -1-c2^post6 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n64 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n64 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0 /\ -1+n64 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+n64 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (-1-z^0 >= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l0 -> [17] : (0 >= 0 /\ 1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 == 0 /\ -z^0 >= 0), cost: NONTERM
New rule:
l0 -> [17] : (1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM

Applied deletion
Removed the following rules: 92 93 94 95 101 102 103 104 123 126 127 132

Accelerated simple loops
Start location: l16
 105: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 106: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 107: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 108: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 109: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ c1^0 == 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 110: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 111: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 112: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 113: l0 -> l0 : pattern^0'=1+pattern^0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-2+pattern^0 <= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 114: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 8
 115: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 116: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=0, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0 /\ c2^0 == 0), cost: 9
 117: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 118: l0 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (c1^0 == 0 /\ -3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 9
 119: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 120: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+c1^0 >= 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 121: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ -1+c2^0 >= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 122: l0 -> l0 : pattern^0'=0, xx^0'=1, it^0'=1+seqlen^0, z^0'=z^post7, seqlen^0'=1+seqlen^0, yy^0'=1, (-3+pattern^0 >= 0 /\ 1+c1^0 <= 0 /\ it^0 <= 0 /\ z^0 == 0 /\ 1+c2^0 <= 0 /\ -1+z^post7 >= 0 /\ -xx^0+yy^0 == 0), cost: 10
 124: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-2+pattern^0 <= 0 /\ -1+it^0 >= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0 /\ -1+pattern^0 >= 0), cost: 9
 125: l0 -> l0 : c1^0'=pattern^0, xx^0'=1, it^0'=-1+it^0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (-1+it^0 >= 0 /\ 1+pattern^0 <= 0 /\ z^0 == 0 /\ -xx^0+yy^0 == 0), cost: 9
 128: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 129: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 130: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
 131: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 7
 133: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7
 134: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: 7
 135: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0), cost: 7
 136: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: 7
 165: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
 166: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
 167: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
 168: l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
 169: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n3 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 170: l0 -> [17] : (1+z^0 <= 0 /\ -1+n4 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 171: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n5 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 172: l0 -> [17] : (1+z^0 <= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0 /\ -1+n6 >= 0), cost: NONTERM
 173: l0 -> l0 : c1^0'=pattern^0, xx^0'=0, it^0'=0, buffer^0'=pattern^0, c2^0'=0, yy^0'=0, (pattern^0 <= 0 /\ pattern^0 >= 0 /\ -1+it^0 >= 0 /\ z^0 <= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*it^0
 174: l0 -> l0 : c1^0'=-2+pattern^0, xx^0'=1, it^0'=0, buffer^0'=-2+pattern^0, c2^0'=1, yy^0'=1, (-1+it^0 >= 0 /\ -3+pattern^0 >= 0 /\ z^0 <= 0 /\ z^0 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 10*it^0
 175: l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*z^0
 176: l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n34 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 177: l0 -> [17] : (1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 178: l0 -> [17] : (1+z^0 <= 0 /\ -1+n43 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: NONTERM
 179: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 180: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+n44 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM
 181: l0 -> [17] : (1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 182: l0 -> [17] : (1+z^0 <= 0 /\ -1+n45 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ 1+c2^post6 <= 0), cost: NONTERM
 183: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 184: l0 -> [17] : (1+z^0 <= 0 /\ -1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -1+n46 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM
 185: l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+n64 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 186: l0 -> [17] : (1+z^0 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+n64 >= 0), cost: NONTERM
 187: l0 -> [17] : (1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 188: l0 -> [17] : (1+z^0 <= 0 /\ -1+n67 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM
 189: l0 -> [17] : (1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 190: l0 -> [17] : (1+z^0 <= 0 /\ -1+n70 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM
 191: l0 -> [17] : (1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 >= 0 /\ xx^0-yy^0 >= 0), cost: NONTERM
 192: l0 -> [17] : (1+z^0 <= 0 /\ -1+n73 >= 0 /\ -xx^0+yy^0 == 0), cost: NONTERM
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2


Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=0, yy^0'=0, (-1+z^post13 >= 0 /\ -1+c1^post6 >= 0), cost: 9

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=-1+z^0, c2^0'=0, yy^0'=0, (1+c1^post6 <= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=0, yy^0'=0, (-1+z^post13 >= 0 /\ 1+c1^post6 <= 0), cost: 9

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -xx^0+yy^0 == 0 /\ -1+z^0 >= 0), cost: 7
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0), cost: 9

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=-1+z^0, c2^0'=c2^post6, yy^0'=1, (-xx^0+yy^0 == 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0), cost: 7
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ 1+c2^post6 <= 0), cost: 9

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0 /\ -1+c1^post6 >= 0), cost: 2+8*z^post13

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c1^post6 >= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ -1+c1^post6 >= 0 /\ 1+c2^post6 <= 0), cost: 2+8*z^post13

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ 1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0 /\ 1+c1^post6 <= 0), cost: 2+8*z^post13

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=c1^post6, xx^0'=1, z^0'=0, c2^0'=c2^post6, yy^0'=1, (1+c1^post6 <= 0 /\ -xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ 1+c2^post6 <= 0 /\ xx^0-yy^0 >= 0), cost: 8*z^0
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ 1+c1^post6 <= 0 /\ 1+c2^post6 <= 0), cost: 2+8*z^post13

Applied chaining
First rule:
l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
Second rule:
l0 -> l0 : c1^0'=0, xx^0'=0, z^0'=0, c2^0'=0, yy^0'=0, (-xx^0+yy^0 >= 0 /\ -1+z^0 >= 0 /\ xx^0-yy^0 >= 0), cost: 6*z^0
New rule:
l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=0, yy^0'=0, -1+z^post13 >= 0, cost: 2+6*z^post13

Applied deletion
Removed the following rules: 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 124 125 128 129 130 131 133 134 135 136 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192

Chained accelerated rules with incoming rules
Start location: l16
  51: l16 -> l0 : pattern^0'=0, xx^0'=0, it^0'=1, z^0'=z^post13, seqlen^0'=1, yy^0'=0, -1+z^post13 >= 0, cost: 2
 193: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=0, yy^0'=0, (-1+z^post13 >= 0 /\ -1+c1^post6 >= 0), cost: 9
 194: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=0, yy^0'=0, (-1+z^post13 >= 0 /\ 1+c1^post6 <= 0), cost: 9
 195: l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0), cost: 9
 196: l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=-1+z^post13, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ 1+c2^post6 <= 0), cost: 9
 197: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0 /\ -1+c1^post6 >= 0), cost: 2+8*z^post13
 198: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ -1+c1^post6 >= 0 /\ 1+c2^post6 <= 0), cost: 2+8*z^post13
 199: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+c2^post6 >= 0 /\ -1+z^post13 >= 0 /\ 1+c1^post6 <= 0), cost: 2+8*z^post13
 200: l16 -> l0 : pattern^0'=0, c1^0'=c1^post6, xx^0'=1, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=c2^post6, yy^0'=1, (-1+z^post13 >= 0 /\ 1+c1^post6 <= 0 /\ 1+c2^post6 <= 0), cost: 2+8*z^post13
 201: l16 -> l0 : pattern^0'=0, c1^0'=0, xx^0'=0, it^0'=1, z^0'=0, seqlen^0'=1, c2^0'=0, yy^0'=0, -1+z^post13 >= 0, cost: 2+6*z^post13


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0