WORST_CASE(Omega(0),?)

Initial ITS
Start location: l10
   0: l0 -> l1 : seq^0'=seq^post0, choice^0'=choice^post0, z^0'=z^post0, pos^0'=pos^post0, N^0'=N^post0, walker^0'=walker^post0, i^0'=i^post0, (seq^0-seq^post0 == 0 /\ -choice^post0+choice^0 == 0 /\ -i^post0+i^0 == 0 /\ -walker^post0+walker^0 == 0 /\ -N^post0+N^0 == 0 /\ pos^0-pos^post0 == 0 /\ z^0-z^post0 == 0), cost: 1
   1: l2 -> l3 : seq^0'=seq^post1, choice^0'=choice^post1, z^0'=z^post1, pos^0'=pos^post1, N^0'=N^post1, walker^0'=walker^post1, i^0'=i^post1, (-N^post1+N^0 == 0 /\ z^0-z^post1 == 0 /\ seq^0-seq^post1 == 0 /\ -1+seq^0-N^0 <= 0 /\ choice^0-choice^post1 == 0 /\ -i^post1+i^0 == 0 /\ pos^0-pos^post1 == 0 /\ -walker^post1+walker^0 == 0), cost: 1
  13: l3 -> l9 : seq^0'=seq^post13, choice^0'=choice^post13, z^0'=z^post13, pos^0'=pos^post13, N^0'=N^post13, walker^0'=walker^post13, i^0'=i^post13, (-walker^post13+walker^0 == 0 /\ -i^post13+i^0 == 0 /\ z^0-z^post13 == 0 /\ choice^0-choice^post13 == 0 /\ -N^post13+N^0 == 0 /\ pos^0-pos^post13 == 0 /\ seq^0-seq^post13 == 0), cost: 1
   2: l4 -> l2 : seq^0'=seq^post2, choice^0'=choice^post2, z^0'=z^post2, pos^0'=pos^post2, N^0'=N^post2, walker^0'=walker^post2, i^0'=i^post2, (choice^0-choice^post2 == 0 /\ i^0-i^post2 == 0 /\ seq^0-seq^post2 == 0 /\ -1+walker^post2-walker^0 == 0 /\ 1-choice^0 <= 0 /\ z^0-z^post2 == 0 /\ -pos^post2+pos^0 == 0 /\ -N^post2+N^0 == 0), cost: 1
   3: l4 -> l2 : seq^0'=seq^post3, choice^0'=choice^post3, z^0'=z^post3, pos^0'=pos^post3, N^0'=N^post3, walker^0'=walker^post3, i^0'=i^post3, (choice^0 <= 0 /\ -i^post3+i^0 == 0 /\ -z^post3+z^0 == 0 /\ choice^0-choice^post3 == 0 /\ seq^0-seq^post3 == 0 /\ -pos^post3+pos^0 == 0 /\ 1-walker^0+walker^post3 == 0 /\ N^0-N^post3 == 0), cost: 1
   4: l5 -> l3 : seq^0'=seq^post4, choice^0'=choice^post4, z^0'=z^post4, pos^0'=pos^post4, N^0'=N^post4, walker^0'=walker^post4, i^0'=i^post4, (0 == 0 /\ -1+walker^post4 == 0 /\ -2+N^post4 <= 0 /\ pos^post4 == 0 /\ i^post4-seq^post4 == 0 /\ -1+seq^post4 == 0 /\ 2-N^post4 <= 0 /\ -z^post4 <= 0 /\ choice^0-choice^post4 == 0), cost: 1
   5: l6 -> l4 : seq^0'=seq^post5, choice^0'=choice^post5, z^0'=z^post5, pos^0'=pos^post5, N^0'=N^post5, walker^0'=walker^post5, i^0'=i^post5, (0 == 0 /\ pos^0-pos^post5 == 0 /\ -z^post5 <= 0 /\ -1-seq^0+seq^post5 == 0 /\ N^0-N^post5 == 0 /\ -walker^post5+walker^0 == 0 /\ i^post5-seq^post5 == 0 /\ i^0 <= 0 /\ choice^0-choice^post5 == 0), cost: 1
   6: l6 -> l4 : seq^0'=seq^post6, choice^0'=choice^post6, z^0'=z^post6, pos^0'=pos^post6, N^0'=N^post6, walker^0'=walker^post6, i^0'=i^post6, (choice^0 <= 0 /\ seq^0-seq^post6 == 0 /\ -N^post6+N^0 == 0 /\ -walker^post6+walker^0 == 0 /\ pos^0-pos^post6 == 0 /\ 1-i^0 <= 0 /\ z^0-z^post6 == 0 /\ -choice^post6+choice^0 == 0 /\ 1+i^post6-i^0 == 0), cost: 1
   7: l7 -> l4 : seq^0'=seq^post7, choice^0'=choice^post7, z^0'=z^post7, pos^0'=pos^post7, N^0'=N^post7, walker^0'=walker^post7, i^0'=i^post7, (-pos^post7+pos^0 == 0 /\ 1-z^0+z^post7 == 0 /\ 1-z^0 <= 0 /\ -i^post7+i^0 == 0 /\ -walker^post7+walker^0 == 0 /\ seq^0-seq^post7 == 0 /\ -N^post7+N^0 == 0 /\ choice^0-choice^post7 == 0), cost: 1
   8: l7 -> l6 : seq^0'=seq^post8, choice^0'=choice^post8, z^0'=z^post8, pos^0'=pos^post8, N^0'=N^post8, walker^0'=walker^post8, i^0'=i^post8, (-walker^post8+walker^0 == 0 /\ choice^0-choice^post8 == 0 /\ -N^post8+N^0 == 0 /\ z^0 <= 0 /\ i^0-i^post8 == 0 /\ -pos^post8+pos^0 == 0 /\ z^0-z^post8 == 0 /\ seq^0-seq^post8 == 0), cost: 1
   9: l8 -> l0 : seq^0'=seq^post9, choice^0'=choice^post9, z^0'=z^post9, pos^0'=pos^post9, N^0'=N^post9, walker^0'=walker^post9, i^0'=i^post9, (choice^0-choice^post9 == 0 /\ seq^0-seq^post9 == 0 /\ i^0-i^post9 == 0 /\ walker^0-walker^post9 == 0 /\ walker^0 <= 0 /\ z^0-z^post9 == 0 /\ -pos^post9+pos^0 == 0 /\ -N^post9+N^0 == 0), cost: 1
  10: l8 -> l7 : seq^0'=seq^post10, choice^0'=choice^post10, z^0'=z^post10, pos^0'=pos^post10, N^0'=N^post10, walker^0'=walker^post10, i^0'=i^post10, (0 == 0 /\ seq^0-seq^post10 == 0 /\ -choice^post10 <= 0 /\ -z^post10+z^0 == 0 /\ -1+choice^post10 <= 0 /\ -pos^post10+pos^0 == 0 /\ 1-walker^0 <= 0 /\ walker^0-walker^post10 == 0 /\ -i^post10+i^0 == 0 /\ N^0-N^post10 == 0), cost: 1
  11: l9 -> l0 : seq^0'=seq^post11, choice^0'=choice^post11, z^0'=z^post11, pos^0'=pos^post11, N^0'=N^post11, walker^0'=walker^post11, i^0'=i^post11, (-i^post11+i^0 == 0 /\ N^0-N^post11 == 0 /\ -z^post11+z^0 == 0 /\ pos^0-pos^post11 == 0 /\ -walker^post11+walker^0 == 0 /\ seq^0-seq^post11 == 0 /\ -choice^post11+choice^0 == 0 /\ 1+N^0-walker^0 <= 0), cost: 1
  12: l9 -> l8 : seq^0'=seq^post12, choice^0'=choice^post12, z^0'=z^post12, pos^0'=pos^post12, N^0'=N^post12, walker^0'=walker^post12, i^0'=i^post12, (-i^post12+i^0 == 0 /\ z^0-z^post12 == 0 /\ -N^post12+N^0 == 0 /\ choice^0-choice^post12 == 0 /\ seq^0-seq^post12 == 0 /\ pos^0-pos^post12 == 0 /\ -walker^post12+walker^0 == 0 /\ -N^0+walker^0 <= 0), cost: 1
  14: l10 -> l5 : seq^0'=seq^post14, choice^0'=choice^post14, z^0'=z^post14, pos^0'=pos^post14, N^0'=N^post14, walker^0'=walker^post14, i^0'=i^post14, (-walker^post14+walker^0 == 0 /\ -N^post14+N^0 == 0 /\ z^0-z^post14 == 0 /\ choice^0-choice^post14 == 0 /\ -i^post14+i^0 == 0 /\ -seq^post14+seq^0 == 0 /\ pos^0-pos^post14 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l10
   1: l2 -> l3 : seq^0'=seq^post1, choice^0'=choice^post1, z^0'=z^post1, pos^0'=pos^post1, N^0'=N^post1, walker^0'=walker^post1, i^0'=i^post1, (-N^post1+N^0 == 0 /\ z^0-z^post1 == 0 /\ seq^0-seq^post1 == 0 /\ -1+seq^0-N^0 <= 0 /\ choice^0-choice^post1 == 0 /\ -i^post1+i^0 == 0 /\ pos^0-pos^post1 == 0 /\ -walker^post1+walker^0 == 0), cost: 1
  13: l3 -> l9 : seq^0'=seq^post13, choice^0'=choice^post13, z^0'=z^post13, pos^0'=pos^post13, N^0'=N^post13, walker^0'=walker^post13, i^0'=i^post13, (-walker^post13+walker^0 == 0 /\ -i^post13+i^0 == 0 /\ z^0-z^post13 == 0 /\ choice^0-choice^post13 == 0 /\ -N^post13+N^0 == 0 /\ pos^0-pos^post13 == 0 /\ seq^0-seq^post13 == 0), cost: 1
   2: l4 -> l2 : seq^0'=seq^post2, choice^0'=choice^post2, z^0'=z^post2, pos^0'=pos^post2, N^0'=N^post2, walker^0'=walker^post2, i^0'=i^post2, (choice^0-choice^post2 == 0 /\ i^0-i^post2 == 0 /\ seq^0-seq^post2 == 0 /\ -1+walker^post2-walker^0 == 0 /\ 1-choice^0 <= 0 /\ z^0-z^post2 == 0 /\ -pos^post2+pos^0 == 0 /\ -N^post2+N^0 == 0), cost: 1
   3: l4 -> l2 : seq^0'=seq^post3, choice^0'=choice^post3, z^0'=z^post3, pos^0'=pos^post3, N^0'=N^post3, walker^0'=walker^post3, i^0'=i^post3, (choice^0 <= 0 /\ -i^post3+i^0 == 0 /\ -z^post3+z^0 == 0 /\ choice^0-choice^post3 == 0 /\ seq^0-seq^post3 == 0 /\ -pos^post3+pos^0 == 0 /\ 1-walker^0+walker^post3 == 0 /\ N^0-N^post3 == 0), cost: 1
   4: l5 -> l3 : seq^0'=seq^post4, choice^0'=choice^post4, z^0'=z^post4, pos^0'=pos^post4, N^0'=N^post4, walker^0'=walker^post4, i^0'=i^post4, (0 == 0 /\ -1+walker^post4 == 0 /\ -2+N^post4 <= 0 /\ pos^post4 == 0 /\ i^post4-seq^post4 == 0 /\ -1+seq^post4 == 0 /\ 2-N^post4 <= 0 /\ -z^post4 <= 0 /\ choice^0-choice^post4 == 0), cost: 1
   5: l6 -> l4 : seq^0'=seq^post5, choice^0'=choice^post5, z^0'=z^post5, pos^0'=pos^post5, N^0'=N^post5, walker^0'=walker^post5, i^0'=i^post5, (0 == 0 /\ pos^0-pos^post5 == 0 /\ -z^post5 <= 0 /\ -1-seq^0+seq^post5 == 0 /\ N^0-N^post5 == 0 /\ -walker^post5+walker^0 == 0 /\ i^post5-seq^post5 == 0 /\ i^0 <= 0 /\ choice^0-choice^post5 == 0), cost: 1
   6: l6 -> l4 : seq^0'=seq^post6, choice^0'=choice^post6, z^0'=z^post6, pos^0'=pos^post6, N^0'=N^post6, walker^0'=walker^post6, i^0'=i^post6, (choice^0 <= 0 /\ seq^0-seq^post6 == 0 /\ -N^post6+N^0 == 0 /\ -walker^post6+walker^0 == 0 /\ pos^0-pos^post6 == 0 /\ 1-i^0 <= 0 /\ z^0-z^post6 == 0 /\ -choice^post6+choice^0 == 0 /\ 1+i^post6-i^0 == 0), cost: 1
   7: l7 -> l4 : seq^0'=seq^post7, choice^0'=choice^post7, z^0'=z^post7, pos^0'=pos^post7, N^0'=N^post7, walker^0'=walker^post7, i^0'=i^post7, (-pos^post7+pos^0 == 0 /\ 1-z^0+z^post7 == 0 /\ 1-z^0 <= 0 /\ -i^post7+i^0 == 0 /\ -walker^post7+walker^0 == 0 /\ seq^0-seq^post7 == 0 /\ -N^post7+N^0 == 0 /\ choice^0-choice^post7 == 0), cost: 1
   8: l7 -> l6 : seq^0'=seq^post8, choice^0'=choice^post8, z^0'=z^post8, pos^0'=pos^post8, N^0'=N^post8, walker^0'=walker^post8, i^0'=i^post8, (-walker^post8+walker^0 == 0 /\ choice^0-choice^post8 == 0 /\ -N^post8+N^0 == 0 /\ z^0 <= 0 /\ i^0-i^post8 == 0 /\ -pos^post8+pos^0 == 0 /\ z^0-z^post8 == 0 /\ seq^0-seq^post8 == 0), cost: 1
  10: l8 -> l7 : seq^0'=seq^post10, choice^0'=choice^post10, z^0'=z^post10, pos^0'=pos^post10, N^0'=N^post10, walker^0'=walker^post10, i^0'=i^post10, (0 == 0 /\ seq^0-seq^post10 == 0 /\ -choice^post10 <= 0 /\ -z^post10+z^0 == 0 /\ -1+choice^post10 <= 0 /\ -pos^post10+pos^0 == 0 /\ 1-walker^0 <= 0 /\ walker^0-walker^post10 == 0 /\ -i^post10+i^0 == 0 /\ N^0-N^post10 == 0), cost: 1
  12: l9 -> l8 : seq^0'=seq^post12, choice^0'=choice^post12, z^0'=z^post12, pos^0'=pos^post12, N^0'=N^post12, walker^0'=walker^post12, i^0'=i^post12, (-i^post12+i^0 == 0 /\ z^0-z^post12 == 0 /\ -N^post12+N^0 == 0 /\ choice^0-choice^post12 == 0 /\ seq^0-seq^post12 == 0 /\ pos^0-pos^post12 == 0 /\ -walker^post12+walker^0 == 0 /\ -N^0+walker^0 <= 0), cost: 1
  14: l10 -> l5 : seq^0'=seq^post14, choice^0'=choice^post14, z^0'=z^post14, pos^0'=pos^post14, N^0'=N^post14, walker^0'=walker^post14, i^0'=i^post14, (-walker^post14+walker^0 == 0 /\ -N^post14+N^0 == 0 /\ z^0-z^post14 == 0 /\ choice^0-choice^post14 == 0 /\ -i^post14+i^0 == 0 /\ -seq^post14+seq^0 == 0 /\ pos^0-pos^post14 == 0), cost: 1


Applied preprocessing
Original rule:
l2 -> l3 : seq^0'=seq^post1, choice^0'=choice^post1, z^0'=z^post1, pos^0'=pos^post1, N^0'=N^post1, walker^0'=walker^post1, i^0'=i^post1, (-N^post1+N^0 == 0 /\ z^0-z^post1 == 0 /\ seq^0-seq^post1 == 0 /\ -1+seq^0-N^0 <= 0 /\ choice^0-choice^post1 == 0 /\ -i^post1+i^0 == 0 /\ pos^0-pos^post1 == 0 /\ -walker^post1+walker^0 == 0), cost: 1
New rule:
l2 -> l3 : -1+seq^0-N^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : seq^0'=seq^post2, choice^0'=choice^post2, z^0'=z^post2, pos^0'=pos^post2, N^0'=N^post2, walker^0'=walker^post2, i^0'=i^post2, (choice^0-choice^post2 == 0 /\ i^0-i^post2 == 0 /\ seq^0-seq^post2 == 0 /\ -1+walker^post2-walker^0 == 0 /\ 1-choice^0 <= 0 /\ z^0-z^post2 == 0 /\ -pos^post2+pos^0 == 0 /\ -N^post2+N^0 == 0), cost: 1
New rule:
l4 -> l2 : walker^0'=1+walker^0, -1+choice^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : seq^0'=seq^post3, choice^0'=choice^post3, z^0'=z^post3, pos^0'=pos^post3, N^0'=N^post3, walker^0'=walker^post3, i^0'=i^post3, (choice^0 <= 0 /\ -i^post3+i^0 == 0 /\ -z^post3+z^0 == 0 /\ choice^0-choice^post3 == 0 /\ seq^0-seq^post3 == 0 /\ -pos^post3+pos^0 == 0 /\ 1-walker^0+walker^post3 == 0 /\ N^0-N^post3 == 0), cost: 1
New rule:
l4 -> l2 : walker^0'=-1+walker^0, choice^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l3 : seq^0'=seq^post4, choice^0'=choice^post4, z^0'=z^post4, pos^0'=pos^post4, N^0'=N^post4, walker^0'=walker^post4, i^0'=i^post4, (0 == 0 /\ -1+walker^post4 == 0 /\ -2+N^post4 <= 0 /\ pos^post4 == 0 /\ i^post4-seq^post4 == 0 /\ -1+seq^post4 == 0 /\ 2-N^post4 <= 0 /\ -z^post4 <= 0 /\ choice^0-choice^post4 == 0), cost: 1
New rule:
l5 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l4 : seq^0'=seq^post5, choice^0'=choice^post5, z^0'=z^post5, pos^0'=pos^post5, N^0'=N^post5, walker^0'=walker^post5, i^0'=i^post5, (0 == 0 /\ pos^0-pos^post5 == 0 /\ -z^post5 <= 0 /\ -1-seq^0+seq^post5 == 0 /\ N^0-N^post5 == 0 /\ -walker^post5+walker^0 == 0 /\ i^post5-seq^post5 == 0 /\ i^0 <= 0 /\ choice^0-choice^post5 == 0), cost: 1
New rule:
l6 -> l4 : seq^0'=1+seq^0, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ i^0 <= 0), cost: 1

Applied preprocessing
Original rule:
l6 -> l4 : seq^0'=seq^post6, choice^0'=choice^post6, z^0'=z^post6, pos^0'=pos^post6, N^0'=N^post6, walker^0'=walker^post6, i^0'=i^post6, (choice^0 <= 0 /\ seq^0-seq^post6 == 0 /\ -N^post6+N^0 == 0 /\ -walker^post6+walker^0 == 0 /\ pos^0-pos^post6 == 0 /\ 1-i^0 <= 0 /\ z^0-z^post6 == 0 /\ -choice^post6+choice^0 == 0 /\ 1+i^post6-i^0 == 0), cost: 1
New rule:
l6 -> l4 : i^0'=-1+i^0, (choice^0 <= 0 /\ -1+i^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l7 -> l4 : seq^0'=seq^post7, choice^0'=choice^post7, z^0'=z^post7, pos^0'=pos^post7, N^0'=N^post7, walker^0'=walker^post7, i^0'=i^post7, (-pos^post7+pos^0 == 0 /\ 1-z^0+z^post7 == 0 /\ 1-z^0 <= 0 /\ -i^post7+i^0 == 0 /\ -walker^post7+walker^0 == 0 /\ seq^0-seq^post7 == 0 /\ -N^post7+N^0 == 0 /\ choice^0-choice^post7 == 0), cost: 1
New rule:
l7 -> l4 : z^0'=-1+z^0, -1+z^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l6 : seq^0'=seq^post8, choice^0'=choice^post8, z^0'=z^post8, pos^0'=pos^post8, N^0'=N^post8, walker^0'=walker^post8, i^0'=i^post8, (-walker^post8+walker^0 == 0 /\ choice^0-choice^post8 == 0 /\ -N^post8+N^0 == 0 /\ z^0 <= 0 /\ i^0-i^post8 == 0 /\ -pos^post8+pos^0 == 0 /\ z^0-z^post8 == 0 /\ seq^0-seq^post8 == 0), cost: 1
New rule:
l7 -> l6 : z^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : seq^0'=seq^post10, choice^0'=choice^post10, z^0'=z^post10, pos^0'=pos^post10, N^0'=N^post10, walker^0'=walker^post10, i^0'=i^post10, (0 == 0 /\ seq^0-seq^post10 == 0 /\ -choice^post10 <= 0 /\ -z^post10+z^0 == 0 /\ -1+choice^post10 <= 0 /\ -pos^post10+pos^0 == 0 /\ 1-walker^0 <= 0 /\ walker^0-walker^post10 == 0 /\ -i^post10+i^0 == 0 /\ N^0-N^post10 == 0), cost: 1
New rule:
l8 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ choice^post10 >= 0), cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : seq^0'=seq^post12, choice^0'=choice^post12, z^0'=z^post12, pos^0'=pos^post12, N^0'=N^post12, walker^0'=walker^post12, i^0'=i^post12, (-i^post12+i^0 == 0 /\ z^0-z^post12 == 0 /\ -N^post12+N^0 == 0 /\ choice^0-choice^post12 == 0 /\ seq^0-seq^post12 == 0 /\ pos^0-pos^post12 == 0 /\ -walker^post12+walker^0 == 0 /\ -N^0+walker^0 <= 0), cost: 1
New rule:
l9 -> l8 : -N^0+walker^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l9 : seq^0'=seq^post13, choice^0'=choice^post13, z^0'=z^post13, pos^0'=pos^post13, N^0'=N^post13, walker^0'=walker^post13, i^0'=i^post13, (-walker^post13+walker^0 == 0 /\ -i^post13+i^0 == 0 /\ z^0-z^post13 == 0 /\ choice^0-choice^post13 == 0 /\ -N^post13+N^0 == 0 /\ pos^0-pos^post13 == 0 /\ seq^0-seq^post13 == 0), cost: 1
New rule:
l3 -> l9 : TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l5 : seq^0'=seq^post14, choice^0'=choice^post14, z^0'=z^post14, pos^0'=pos^post14, N^0'=N^post14, walker^0'=walker^post14, i^0'=i^post14, (-walker^post14+walker^0 == 0 /\ -N^post14+N^0 == 0 /\ z^0-z^post14 == 0 /\ choice^0-choice^post14 == 0 /\ -i^post14+i^0 == 0 /\ -seq^post14+seq^0 == 0 /\ pos^0-pos^post14 == 0), cost: 1
New rule:
l10 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l10
  15: l2 -> l3 : -1+seq^0-N^0 <= 0, cost: 1
  25: l3 -> l9 : TRUE, cost: 1
  16: l4 -> l2 : walker^0'=1+walker^0, -1+choice^0 >= 0, cost: 1
  17: l4 -> l2 : walker^0'=-1+walker^0, choice^0 <= 0, cost: 1
  18: l5 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 1
  19: l6 -> l4 : seq^0'=1+seq^0, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ i^0 <= 0), cost: 1
  20: l6 -> l4 : i^0'=-1+i^0, (choice^0 <= 0 /\ -1+i^0 >= 0), cost: 1
  21: l7 -> l4 : z^0'=-1+z^0, -1+z^0 >= 0, cost: 1
  22: l7 -> l6 : z^0 <= 0, cost: 1
  23: l8 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ choice^post10 >= 0), cost: 1
  24: l9 -> l8 : -N^0+walker^0 <= 0, cost: 1
  26: l10 -> l5 : TRUE, cost: 1


Eliminating location l5 by chaining:

Applied chaining
First rule:
l10 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 1
New rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2

Applied deletion
Removed the following rules: 18 26

Eliminating location l9 by chaining:

Applied chaining
First rule:
l3 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l8 : -N^0+walker^0 <= 0, cost: 1
New rule:
l3 -> l8 : -N^0+walker^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 24 25

Eliminating location l8 by chaining:

Applied chaining
First rule:
l3 -> l8 : -N^0+walker^0 <= 0, cost: 2
Second rule:
l8 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ choice^post10 >= 0), cost: 1
New rule:
l3 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 3

Applied deletion
Removed the following rules: 23 28

Eliminated locations on linear paths
Start location: l10
  15: l2 -> l3 : -1+seq^0-N^0 <= 0, cost: 1
  29: l3 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 3
  16: l4 -> l2 : walker^0'=1+walker^0, -1+choice^0 >= 0, cost: 1
  17: l4 -> l2 : walker^0'=-1+walker^0, choice^0 <= 0, cost: 1
  19: l6 -> l4 : seq^0'=1+seq^0, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ i^0 <= 0), cost: 1
  20: l6 -> l4 : i^0'=-1+i^0, (choice^0 <= 0 /\ -1+i^0 >= 0), cost: 1
  21: l7 -> l4 : z^0'=-1+z^0, -1+z^0 >= 0, cost: 1
  22: l7 -> l6 : z^0 <= 0, cost: 1
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Eliminating location l7 by chaining:

Applied chaining
First rule:
l3 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 3
Second rule:
l7 -> l4 : z^0'=-1+z^0, -1+z^0 >= 0, cost: 1
New rule:
l3 -> l4 : choice^0'=choice^post10, z^0'=-1+z^0, (-1+z^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4

Applied chaining
First rule:
l3 -> l7 : choice^0'=choice^post10, (-1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 3
Second rule:
l7 -> l6 : z^0 <= 0, cost: 1
New rule:
l3 -> l6 : choice^0'=choice^post10, (z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4

Applied deletion
Removed the following rules: 21 22 29

Eliminating location l2 by chaining:

Applied chaining
First rule:
l4 -> l2 : walker^0'=1+walker^0, -1+choice^0 >= 0, cost: 1
Second rule:
l2 -> l3 : -1+seq^0-N^0 <= 0, cost: 1
New rule:
l4 -> l3 : walker^0'=1+walker^0, (-1+seq^0-N^0 <= 0 /\ -1+choice^0 >= 0), cost: 2

Applied chaining
First rule:
l4 -> l2 : walker^0'=-1+walker^0, choice^0 <= 0, cost: 1
Second rule:
l2 -> l3 : -1+seq^0-N^0 <= 0, cost: 1
New rule:
l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 15 16 17

Eliminated locations on tree-shaped paths
Start location: l10
  30: l3 -> l4 : choice^0'=choice^post10, z^0'=-1+z^0, (-1+z^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
  31: l3 -> l6 : choice^0'=choice^post10, (z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
  32: l4 -> l3 : walker^0'=1+walker^0, (-1+seq^0-N^0 <= 0 /\ -1+choice^0 >= 0), cost: 2
  33: l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2
  19: l6 -> l4 : seq^0'=1+seq^0, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ i^0 <= 0), cost: 1
  20: l6 -> l4 : i^0'=-1+i^0, (choice^0 <= 0 /\ -1+i^0 >= 0), cost: 1
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Eliminating location l6 by chaining:

Applied chaining
First rule:
l3 -> l6 : choice^0'=choice^post10, (z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
Second rule:
l6 -> l4 : seq^0'=1+seq^0, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ i^0 <= 0), cost: 1
New rule:
l3 -> l4 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 5

Applied chaining
First rule:
l3 -> l6 : choice^0'=choice^post10, (z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
Second rule:
l6 -> l4 : i^0'=-1+i^0, (choice^0 <= 0 /\ -1+i^0 >= 0), cost: 1
New rule:
l3 -> l4 : choice^0'=choice^post10, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 5

Applied simplification
Original rule:
l3 -> l4 : choice^0'=choice^post10, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 5
New rule:
l3 -> l4 : choice^0'=choice^post10, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 5

Applied deletion
Removed the following rules: 19 20 31

Eliminated locations on tree-shaped paths
Start location: l10
  30: l3 -> l4 : choice^0'=choice^post10, z^0'=-1+z^0, (-1+z^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
  34: l3 -> l4 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 5
  35: l3 -> l4 : choice^0'=choice^post10, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 5
  32: l4 -> l3 : walker^0'=1+walker^0, (-1+seq^0-N^0 <= 0 /\ -1+choice^0 >= 0), cost: 2
  33: l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Eliminating location l4 by chaining:

Applied chaining
First rule:
l3 -> l4 : choice^0'=choice^post10, z^0'=-1+z^0, (-1+z^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
Second rule:
l4 -> l3 : walker^0'=1+walker^0, (-1+seq^0-N^0 <= 0 /\ -1+choice^0 >= 0), cost: 2
New rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 6

Applied simplification
Original rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6

Applied chaining
First rule:
l3 -> l4 : choice^0'=choice^post10, z^0'=-1+z^0, (-1+z^0 >= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0), cost: 4
Second rule:
l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2
New rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 6

Applied simplification
Original rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 6

Applied chaining
First rule:
l3 -> l4 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 5
Second rule:
l4 -> l3 : walker^0'=1+walker^0, (-1+seq^0-N^0 <= 0 /\ -1+choice^0 >= 0), cost: 2
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7

Applied chaining
First rule:
l3 -> l4 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 5
Second rule:
l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7

Applied chaining
First rule:
l3 -> l4 : choice^0'=choice^post10, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 5
Second rule:
l4 -> l3 : walker^0'=-1+walker^0, (choice^0 <= 0 /\ -1+seq^0-N^0 <= 0), cost: 2
New rule:
l3 -> l3 : choice^0'=choice^post10, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 7

Applied deletion
Removed the following rules: 30 32 33 34 35

Eliminated locations on tree-shaped paths
Start location: l10
  36: l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
  37: l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 6
  38: l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
  39: l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7
  40: l3 -> l3 : choice^0'=choice^post10, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 7
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Applied simplification
Original rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6

Applied simplification
Original rule:
l3 -> l3 : choice^0'=choice^post10, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=0, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+choice^post10 <= 0 /\ -1+choice^post10 >= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=1, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=choice^post10, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=0, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7

Applied simplification
Original rule:
l3 -> l3 : choice^0'=choice^post10, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ choice^post10 <= 0 /\ choice^post10 >= 0), cost: 7
New rule:
l3 -> l3 : choice^0'=0, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 7

Simplified simple loops
Start location: l10
  41: l3 -> l3 : choice^0'=1, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
  42: l3 -> l3 : choice^0'=0, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
  43: l3 -> l3 : seq^0'=1+seq^0, choice^0'=1, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
  44: l3 -> l3 : seq^0'=1+seq^0, choice^0'=0, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
  45: l3 -> l3 : choice^0'=0, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 7
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Applied acceleration
Original rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0, walker^0'=1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=1, z^0'=z^0-n, walker^0'=n+walker^0, (z^0-n >= 0 /\ 1-n+N^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ -1+n >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bGbGgo.txt

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=1, z^0'=z^0-n, walker^0'=n+walker^0, (z^0-n >= 0 /\ 1-n+N^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ -1+n >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*n
New rule:
l3 -> l3 : choice^0'=1, z^0'=0, walker^0'=z^0+walker^0, (0 >= 0 /\ 1-z^0+N^0-walker^0 >= 0 /\ -1+z^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*z^0

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=1, z^0'=z^0-n, walker^0'=n+walker^0, (z^0-n >= 0 /\ 1-n+N^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ -1+n >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*n
New rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0-N^0+walker^0, walker^0'=1+N^0, (0 >= 0 /\ -1+walker^0 >= 0 /\ -1+z^0-N^0+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6+6*N^0-6*walker^0

Applied acceleration
Original rule:
l3 -> l3 : choice^0'=0, z^0'=-1+z^0, walker^0'=-1+walker^0, (-1+z^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 6
New rule:
l3 -> l3 : choice^0'=0, z^0'=-n0+z^0, walker^0'=-n0+walker^0, (-n0+walker^0 >= 0 /\ -1+n0 >= 0 /\ -n0+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_JEKDgE.txt

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=0, z^0'=-n0+z^0, walker^0'=-n0+walker^0, (-n0+walker^0 >= 0 /\ -1+n0 >= 0 /\ -n0+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*n0
New rule:
l3 -> l3 : choice^0'=0, z^0'=0, walker^0'=-z^0+walker^0, (0 >= 0 /\ -z^0+walker^0 >= 0 /\ -1+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*z^0

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=0, z^0'=-n0+z^0, walker^0'=-n0+walker^0, (-n0+walker^0 >= 0 /\ -1+n0 >= 0 /\ -n0+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*n0
New rule:
l3 -> l3 : choice^0'=0, z^0'=z^0-walker^0, walker^0'=0, (0 >= 0 /\ z^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*walker^0

Applied acceleration
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=1, z^0'=z^post5, walker^0'=1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=seq^0+n1, choice^0'=1, z^0'=z^post5, walker^0'=n1+walker^0, i^0'=seq^0+n1, (-z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+n1 >= 0 /\ 1-n1+N^0-walker^0 >= 0 /\ 1-seq^0-n1+N^0 >= 0 /\ 1-seq^0-n1 >= 0 /\ -1+walker^0 >= 0), cost: 7*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LHiBPB.txt

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n1, choice^0'=1, z^0'=z^post5, walker^0'=n1+walker^0, i^0'=seq^0+n1, (-z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+n1 >= 0 /\ 1-n1+N^0-walker^0 >= 0 /\ 1-seq^0-n1+N^0 >= 0 /\ 1-seq^0-n1 >= 0 /\ -1+walker^0 >= 0), cost: 7*n1
New rule:
l3 -> l3 : seq^0'=1+seq^0+N^0-walker^0, choice^0'=1, z^0'=z^post5, walker^0'=1+N^0, i^0'=1+seq^0+N^0-walker^0, (0 >= 0 /\ -z^0 >= 0 /\ -seq^0-N^0+walker^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -seq^0+walker^0 >= 0 /\ -1+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7+7*N^0-7*walker^0

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n1, choice^0'=1, z^0'=z^post5, walker^0'=n1+walker^0, i^0'=seq^0+n1, (-z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+n1 >= 0 /\ 1-n1+N^0-walker^0 >= 0 /\ 1-seq^0-n1+N^0 >= 0 /\ 1-seq^0-n1 >= 0 /\ -1+walker^0 >= 0), cost: 7*n1
New rule:
l3 -> l3 : seq^0'=1+N^0, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+N^0+walker^0, i^0'=1+N^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+walker^0 >= 0 /\ -N^0 >= 0 /\ seq^0-walker^0 >= 0 /\ -seq^0+N^0 >= 0), cost: 7-7*seq^0+7*N^0

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n1, choice^0'=1, z^0'=z^post5, walker^0'=n1+walker^0, i^0'=seq^0+n1, (-z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+n1 >= 0 /\ 1-n1+N^0-walker^0 >= 0 /\ 1-seq^0-n1+N^0 >= 0 /\ 1-seq^0-n1 >= 0 /\ -1+walker^0 >= 0), cost: 7*n1
New rule:
l3 -> l3 : seq^0'=1, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+walker^0, i^0'=1, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ seq^0+N^0-walker^0 >= 0 /\ N^0 >= 0 /\ -1+walker^0 >= 0 /\ -seq^0 >= 0), cost: 7-7*seq^0

Applied acceleration
Original rule:
l3 -> l3 : seq^0'=1+seq^0, choice^0'=0, z^0'=z^post5, walker^0'=-1+walker^0, i^0'=1+seq^0, (z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0 /\ seq^0-N^0 <= 0 /\ i^0 <= 0), cost: 7
New rule:
l3 -> l3 : seq^0'=seq^0+n2, choice^0'=0, z^0'=z^post5, walker^0'=-n2+walker^0, i^0'=seq^0+n2, (-z^0 >= 0 /\ 1-seq^0-n2+N^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -1+n2 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0-n2 >= 0 /\ -n2+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_nOMPaJ.txt

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n2, choice^0'=0, z^0'=z^post5, walker^0'=-n2+walker^0, i^0'=seq^0+n2, (-z^0 >= 0 /\ 1-seq^0-n2+N^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -1+n2 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0-n2 >= 0 /\ -n2+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n2
New rule:
l3 -> l3 : seq^0'=seq^0+walker^0, choice^0'=0, z^0'=z^post5, walker^0'=0, i^0'=seq^0+walker^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0+N^0-walker^0 >= 0 /\ 1-seq^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n2, choice^0'=0, z^0'=z^post5, walker^0'=-n2+walker^0, i^0'=seq^0+n2, (-z^0 >= 0 /\ 1-seq^0-n2+N^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -1+n2 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0-n2 >= 0 /\ -n2+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n2
New rule:
l3 -> l3 : seq^0'=1+N^0, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0-N^0+walker^0, i^0'=1+N^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -N^0 >= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0-N^0+walker^0 >= 0 /\ -seq^0+N^0 >= 0), cost: 7-7*seq^0+7*N^0

Applied instantiation
Original rule:
l3 -> l3 : seq^0'=seq^0+n2, choice^0'=0, z^0'=z^post5, walker^0'=-n2+walker^0, i^0'=seq^0+n2, (-z^0 >= 0 /\ 1-seq^0-n2+N^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -1+n2 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0-n2 >= 0 /\ -n2+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n2
New rule:
l3 -> l3 : seq^0'=1, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0+walker^0, i^0'=1, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ N^0 >= 0 /\ -seq^0 >= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0+walker^0 >= 0), cost: 7-7*seq^0

Applied acceleration
Original rule:
l3 -> l3 : choice^0'=0, walker^0'=-1+walker^0, i^0'=-1+i^0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ -1+seq^0-N^0 <= 0 /\ -1+walker^0 >= 0 /\ -N^0+walker^0 <= 0), cost: 7
New rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-n3, i^0'=i^0-n3, (-z^0 >= 0 /\ -1+n3 >= 0 /\ i^0-n3 >= 0 /\ walker^0-n3 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_CinpEh.txt

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-n3, i^0'=i^0-n3, (-z^0 >= 0 /\ -1+n3 >= 0 /\ i^0-n3 >= 0 /\ walker^0-n3 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n3
New rule:
l3 -> l3 : choice^0'=0, walker^0'=0, i^0'=-walker^0+i^0, (0 >= 0 /\ -z^0 >= 0 /\ -1+walker^0 >= 0 /\ -walker^0+i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0

Applied instantiation
Original rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-n3, i^0'=i^0-n3, (-z^0 >= 0 /\ -1+n3 >= 0 /\ i^0-n3 >= 0 /\ walker^0-n3 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*n3
New rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-i^0, i^0'=0, (0 >= 0 /\ -z^0 >= 0 /\ -1+i^0 >= 0 /\ walker^0-i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*i^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=1, z^0'=0, walker^0'=z^0+walker^0, (0 >= 0 /\ 1-z^0+N^0-walker^0 >= 0 /\ -1+z^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*z^0
New rule:
l3 -> l3 : choice^0'=1, z^0'=0, walker^0'=z^0+walker^0, (1-z^0+N^0-walker^0 >= 0 /\ -1+z^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*z^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0-N^0+walker^0, walker^0'=1+N^0, (0 >= 0 /\ -1+walker^0 >= 0 /\ -1+z^0-N^0+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6+6*N^0-6*walker^0
New rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0-N^0+walker^0, walker^0'=1+N^0, (-1+walker^0 >= 0 /\ -1+z^0-N^0+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6+6*N^0-6*walker^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=0, z^0'=0, walker^0'=-z^0+walker^0, (0 >= 0 /\ -z^0+walker^0 >= 0 /\ -1+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*z^0
New rule:
l3 -> l3 : choice^0'=0, z^0'=0, walker^0'=-z^0+walker^0, (-z^0+walker^0 >= 0 /\ -1+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*z^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=0, z^0'=z^0-walker^0, walker^0'=0, (0 >= 0 /\ z^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*walker^0
New rule:
l3 -> l3 : choice^0'=0, z^0'=z^0-walker^0, walker^0'=0, (z^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*walker^0

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1+seq^0+N^0-walker^0, choice^0'=1, z^0'=z^post5, walker^0'=1+N^0, i^0'=1+seq^0+N^0-walker^0, (0 >= 0 /\ -z^0 >= 0 /\ -seq^0-N^0+walker^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -seq^0+walker^0 >= 0 /\ -1+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7+7*N^0-7*walker^0
New rule:
l3 -> l3 : seq^0'=1+seq^0+N^0-walker^0, choice^0'=1, z^0'=z^post5, walker^0'=1+N^0, i^0'=1+seq^0+N^0-walker^0, (-seq^0-N^0+walker^0 >= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0), cost: 7+7*N^0-7*walker^0

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+walker^0, i^0'=1, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ seq^0+N^0-walker^0 >= 0 /\ N^0 >= 0 /\ -1+walker^0 >= 0 /\ -seq^0 >= 0), cost: 7-7*seq^0
New rule:
l3 -> l3 : seq^0'=1, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+walker^0, i^0'=1, (seq^0 <= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ seq^0+N^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0), cost: 7-7*seq^0

Applied simplification
Original rule:
l3 -> l3 : seq^0'=seq^0+walker^0, choice^0'=0, z^0'=z^post5, walker^0'=0, i^0'=seq^0+walker^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ 1-seq^0+N^0-walker^0 >= 0 /\ 1-seq^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0
New rule:
l3 -> l3 : seq^0'=seq^0+walker^0, choice^0'=0, z^0'=z^post5, walker^0'=0, i^0'=seq^0+walker^0, (z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ 1-seq^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0

Applied simplification
Original rule:
l3 -> l3 : seq^0'=1, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0+walker^0, i^0'=1, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ N^0 >= 0 /\ -seq^0 >= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0+walker^0 >= 0), cost: 7-7*seq^0
New rule:
l3 -> l3 : seq^0'=1, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0+walker^0, i^0'=1, (seq^0 <= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0+walker^0 >= 0), cost: 7-7*seq^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=0, walker^0'=0, i^0'=-walker^0+i^0, (0 >= 0 /\ -z^0 >= 0 /\ -1+walker^0 >= 0 /\ -walker^0+i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0
New rule:
l3 -> l3 : choice^0'=0, walker^0'=0, i^0'=-walker^0+i^0, (z^0 <= 0 /\ -1+walker^0 >= 0 /\ -walker^0+i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0

Applied simplification
Original rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-i^0, i^0'=0, (0 >= 0 /\ -z^0 >= 0 /\ -1+i^0 >= 0 /\ walker^0-i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*i^0
New rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-i^0, i^0'=0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ walker^0-i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*i^0

Applied deletion
Removed the following rules: 41 42 43 44 45

Accelerated simple loops
Start location: l10
  51: l3 -> l3 : seq^0'=1+N^0, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+N^0+walker^0, i^0'=1+N^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -1+walker^0 >= 0 /\ -N^0 >= 0 /\ seq^0-walker^0 >= 0 /\ -seq^0+N^0 >= 0), cost: 7-7*seq^0+7*N^0
  54: l3 -> l3 : seq^0'=1+N^0, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0-N^0+walker^0, i^0'=1+N^0, (0 >= 0 /\ -z^0 >= 0 /\ z^post5 >= 0 /\ -i^0 >= 0 /\ -z^post5 >= 0 /\ -N^0 >= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0-N^0+walker^0 >= 0 /\ -seq^0+N^0 >= 0), cost: 7-7*seq^0+7*N^0
  58: l3 -> l3 : choice^0'=1, z^0'=0, walker^0'=z^0+walker^0, (1-z^0+N^0-walker^0 >= 0 /\ -1+z^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*z^0
  59: l3 -> l3 : choice^0'=1, z^0'=-1+z^0-N^0+walker^0, walker^0'=1+N^0, (-1+walker^0 >= 0 /\ -1+z^0-N^0+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6+6*N^0-6*walker^0
  60: l3 -> l3 : choice^0'=0, z^0'=0, walker^0'=-z^0+walker^0, (-z^0+walker^0 >= 0 /\ -1+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*z^0
  61: l3 -> l3 : choice^0'=0, z^0'=z^0-walker^0, walker^0'=0, (z^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*walker^0
  62: l3 -> l3 : seq^0'=1+seq^0+N^0-walker^0, choice^0'=1, z^0'=z^post5, walker^0'=1+N^0, i^0'=1+seq^0+N^0-walker^0, (-seq^0-N^0+walker^0 >= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0), cost: 7+7*N^0-7*walker^0
  63: l3 -> l3 : seq^0'=1, choice^0'=1, z^0'=z^post5, walker^0'=1-seq^0+walker^0, i^0'=1, (seq^0 <= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ seq^0+N^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0), cost: 7-7*seq^0
  64: l3 -> l3 : seq^0'=seq^0+walker^0, choice^0'=0, z^0'=z^post5, walker^0'=0, i^0'=seq^0+walker^0, (z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ 1-seq^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0
  65: l3 -> l3 : seq^0'=1, choice^0'=0, z^0'=z^post5, walker^0'=-1+seq^0+walker^0, i^0'=1, (seq^0 <= 0 /\ z^post5 <= 0 /\ z^post5 >= 0 /\ z^0 <= 0 /\ i^0 <= 0 /\ N^0-walker^0 >= 0 /\ -1+seq^0+walker^0 >= 0), cost: 7-7*seq^0
  66: l3 -> l3 : choice^0'=0, walker^0'=0, i^0'=-walker^0+i^0, (z^0 <= 0 /\ -1+walker^0 >= 0 /\ -walker^0+i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0
  67: l3 -> l3 : choice^0'=0, walker^0'=walker^0-i^0, i^0'=0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ walker^0-i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*i^0
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2


Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=1, z^0'=0, walker^0'=z^0+walker^0, (1-z^0+N^0-walker^0 >= 0 /\ -1+z^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0), cost: 6*z^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=1, z^0'=0, pos^0'=0, N^0'=2, walker^0'=1+z^post4, i^0'=1, (-2+z^post4 <= 0 /\ -1+z^post4 >= 0), cost: 2+6*z^post4

Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=1, z^0'=-1+z^0-N^0+walker^0, walker^0'=1+N^0, (-1+walker^0 >= 0 /\ -1+z^0-N^0+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6+6*N^0-6*walker^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=1, z^0'=-2+z^post4, pos^0'=0, N^0'=2, walker^0'=3, i^0'=1, -2+z^post4 >= 0, cost: 14

Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=0, z^0'=0, walker^0'=-z^0+walker^0, (-z^0+walker^0 >= 0 /\ -1+z^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*z^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=0, pos^0'=0, N^0'=2, walker^0'=0, i^0'=1, (1 >= 0 /\ 2 >= 0), cost: 8

Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=0, z^0'=z^0-walker^0, walker^0'=0, (z^0-walker^0 >= 0 /\ -1+walker^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 6*walker^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=-1+z^post4, pos^0'=0, N^0'=2, walker^0'=0, i^0'=1, -1+z^post4 >= 0, cost: 8

Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=0, walker^0'=0, i^0'=-walker^0+i^0, (z^0 <= 0 /\ -1+walker^0 >= 0 /\ -walker^0+i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*walker^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=0, pos^0'=0, N^0'=2, walker^0'=0, i^0'=0, (0 >= 0 /\ 1 >= 0 /\ 2 >= 0), cost: 9

Applied chaining
First rule:
l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
Second rule:
l3 -> l3 : choice^0'=0, walker^0'=walker^0-i^0, i^0'=0, (z^0 <= 0 /\ -1+i^0 >= 0 /\ walker^0-i^0 >= 0 /\ 1-seq^0+N^0 >= 0 /\ N^0-walker^0 >= 0), cost: 7*i^0
New rule:
l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=0, pos^0'=0, N^0'=2, walker^0'=0, i^0'=0, (0 >= 0 /\ 1 >= 0 /\ 2 >= 0), cost: 9

Applied deletion
Removed the following rules: 51 54 58 59 60 61 62 63 64 65 66 67

Chained accelerated rules with incoming rules
Start location: l10
  27: l10 -> l3 : seq^0'=1, z^0'=z^post4, pos^0'=0, N^0'=2, walker^0'=1, i^0'=1, z^post4 >= 0, cost: 2
  68: l10 -> l3 : seq^0'=1, choice^0'=1, z^0'=0, pos^0'=0, N^0'=2, walker^0'=1+z^post4, i^0'=1, (-2+z^post4 <= 0 /\ -1+z^post4 >= 0), cost: 2+6*z^post4
  69: l10 -> l3 : seq^0'=1, choice^0'=1, z^0'=-2+z^post4, pos^0'=0, N^0'=2, walker^0'=3, i^0'=1, -2+z^post4 >= 0, cost: 14
  70: l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=0, pos^0'=0, N^0'=2, walker^0'=0, i^0'=1, (1 >= 0 /\ 2 >= 0), cost: 8
  71: l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=-1+z^post4, pos^0'=0, N^0'=2, walker^0'=0, i^0'=1, -1+z^post4 >= 0, cost: 8
  72: l10 -> l3 : seq^0'=1, choice^0'=0, z^0'=0, pos^0'=0, N^0'=2, walker^0'=0, i^0'=0, (0 >= 0 /\ 1 >= 0 /\ 2 >= 0), cost: 9


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0