WORST_CASE(Omega(0),?)

Initial ITS
Start location: l3
   0: l0 -> l1 : n^0'=n^post0, c2^0'=c2^post0, z^0'=z^post0, pos^0'=pos^post0, max^0'=max^post0, c1^0'=c1^post0, wpos^0'=wpos^post0, pi^0'=pi^post0, m^0'=m^post0, seq^0'=seq^post0, (0 == 0 /\ -1+wpos^50-wpos^40 == 0 /\ 1-pos^post0 <= 0 /\ -1+pos^post0 <= 0 /\ 1-m^20 <= 0 /\ -c1^30 <= 0 /\ wpos^20 <= 0 /\ wpos^20 == 0 /\ 1+m^10-m^0 == 0 /\ 1-c1^30 <= 0 /\ -1+c1^30 <= 0 /\ -1+m^20-m^10 == 0 /\ 1-wpos^50 <= 0 /\ -1+wpos^50 <= 0 /\ z^0 <= 0 /\ -1+seq^post0-seq^0 == 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ -1-pos^10+pos^post0 == 0 /\ -c2^post0 <= 0 /\ pi^20-seq^post0 == 0 /\ -z^10 <= 0 /\ 1-m^30 <= 0 /\ -1-wpos^20+wpos^30 == 0 /\ c2^post0 <= 0 /\ c2^10 <= 0 /\ 1-c2^30 <= 0 /\ -1+c2^30 <= 0 /\ -1+c2^10 <= 0 /\ -1+c2^post0 <= 0 /\ 1-m^0 <= 0 /\ 1-z^10 <= 0 /\ 1-m^10 <= 0 /\ pos^10 <= 0 /\ pos^10 == 0 /\ -c2^30 <= 0 /\ -c2^10 <= 0 /\ 1-max^0+m^20 <= 0 /\ 1+z^20-z^10 == 0 /\ pi^10 <= 0 /\ 1-wpos^30 <= 0 /\ -1+wpos^30 <= 0 /\ -max^post0+max^0 == 0 /\ c1^40 <= 0 /\ wpos^0 <= 0 /\ 1-wpos^10 <= 0 /\ -1+wpos^10 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^20+pi^post0 == 0 /\ 1-z^20 <= 0 /\ 1-c1^20 <= 0 /\ -1+c1^20 <= 0 /\ -c1^40 <= 0 /\ 1-c2^20 <= 0 /\ -1+c2^20 <= 0 /\ -1+m^30-m^20 == 0 /\ 1-c1^10 <= 0 /\ -1+c1^10 <= 0 /\ wpos^post0 == 0 /\ -1+wpos^10-wpos^0 == 0 /\ n^0-n^post0 == 0 /\ z^post0 <= 0 /\ -c1^post0 <= 0 /\ 1-m^30+m^post0 == 0 /\ -c1^20 <= 0 /\ -1+c1^40 <= 0 /\ -c2^20 <= 0 /\ 1-z^20+z^post0 == 0 /\ wpos^40 <= 0 /\ wpos^40 == 0 /\ -c1^10 <= 0 /\ 1-pi^20 <= 0 /\ 1-c1^post0 <= 0 /\ -1+c1^post0 <= 0 /\ 1+pi^10-pi^0 == 0 /\ 1-max^0+m^10 <= 0), cost: 1
   1: l1 -> l0 : n^0'=n^post1, c2^0'=c2^post1, z^0'=z^post1, pos^0'=pos^post1, max^0'=max^post1, c1^0'=c1^post1, wpos^0'=wpos^post1, pi^0'=pi^post1, m^0'=m^post1, seq^0'=seq^post1, (-pi^post1+pi^0 == 0 /\ -c1^post1+c1^0 == 0 /\ n^0-n^post1 == 0 /\ z^0-z^post1 == 0 /\ c2^0-c2^post1 == 0 /\ m^0-m^post1 == 0 /\ max^0-max^post1 == 0 /\ -seq^post1+seq^0 == 0 /\ pos^0-pos^post1 == 0 /\ -wpos^post1+wpos^0 == 0), cost: 1
   2: l2 -> l0 : n^0'=n^post2, c2^0'=c2^post2, z^0'=z^post2, pos^0'=pos^post2, max^0'=max^post2, c1^0'=c1^post2, wpos^0'=wpos^post2, pi^0'=pi^post2, m^0'=m^post2, seq^0'=seq^post2, (0 == 0 /\ pos^11 <= 0 /\ pos^11 == 0 /\ pi^post2-seq^post2 == 0 /\ wpos^post2 == 0 /\ -n^post2 <= 0 /\ -1+seq^post2 == 0 /\ -z^post2 <= 0 /\ -1-pos^11+pos^post2 == 0 /\ c1^post2 <= 0 /\ z^post2 <= 0 /\ -max^post2 <= 0 /\ -1+c1^post2 <= 0 /\ -m^post2 <= 0 /\ -c2^post2+c2^0 == 0 /\ -n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -c1^post2 <= 0 /\ 1-m^post2 <= 0), cost: 1
   3: l3 -> l2 : n^0'=n^post3, c2^0'=c2^post3, z^0'=z^post3, pos^0'=pos^post3, max^0'=max^post3, c1^0'=c1^post3, wpos^0'=wpos^post3, pi^0'=pi^post3, m^0'=m^post3, seq^0'=seq^post3, (-pi^post3+pi^0 == 0 /\ c1^0-c1^post3 == 0 /\ wpos^0-wpos^post3 == 0 /\ -max^post3+max^0 == 0 /\ -seq^post3+seq^0 == 0 /\ -m^post3+m^0 == 0 /\ -pos^post3+pos^0 == 0 /\ n^0-n^post3 == 0 /\ c2^0-c2^post3 == 0 /\ z^0-z^post3 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : n^0'=n^post0, c2^0'=c2^post0, z^0'=z^post0, pos^0'=pos^post0, max^0'=max^post0, c1^0'=c1^post0, wpos^0'=wpos^post0, pi^0'=pi^post0, m^0'=m^post0, seq^0'=seq^post0, (0 == 0 /\ -1+wpos^50-wpos^40 == 0 /\ 1-pos^post0 <= 0 /\ -1+pos^post0 <= 0 /\ 1-m^20 <= 0 /\ -c1^30 <= 0 /\ wpos^20 <= 0 /\ wpos^20 == 0 /\ 1+m^10-m^0 == 0 /\ 1-c1^30 <= 0 /\ -1+c1^30 <= 0 /\ -1+m^20-m^10 == 0 /\ 1-wpos^50 <= 0 /\ -1+wpos^50 <= 0 /\ z^0 <= 0 /\ -1+seq^post0-seq^0 == 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ -1-pos^10+pos^post0 == 0 /\ -c2^post0 <= 0 /\ pi^20-seq^post0 == 0 /\ -z^10 <= 0 /\ 1-m^30 <= 0 /\ -1-wpos^20+wpos^30 == 0 /\ c2^post0 <= 0 /\ c2^10 <= 0 /\ 1-c2^30 <= 0 /\ -1+c2^30 <= 0 /\ -1+c2^10 <= 0 /\ -1+c2^post0 <= 0 /\ 1-m^0 <= 0 /\ 1-z^10 <= 0 /\ 1-m^10 <= 0 /\ pos^10 <= 0 /\ pos^10 == 0 /\ -c2^30 <= 0 /\ -c2^10 <= 0 /\ 1-max^0+m^20 <= 0 /\ 1+z^20-z^10 == 0 /\ pi^10 <= 0 /\ 1-wpos^30 <= 0 /\ -1+wpos^30 <= 0 /\ -max^post0+max^0 == 0 /\ c1^40 <= 0 /\ wpos^0 <= 0 /\ 1-wpos^10 <= 0 /\ -1+wpos^10 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^20+pi^post0 == 0 /\ 1-z^20 <= 0 /\ 1-c1^20 <= 0 /\ -1+c1^20 <= 0 /\ -c1^40 <= 0 /\ 1-c2^20 <= 0 /\ -1+c2^20 <= 0 /\ -1+m^30-m^20 == 0 /\ 1-c1^10 <= 0 /\ -1+c1^10 <= 0 /\ wpos^post0 == 0 /\ -1+wpos^10-wpos^0 == 0 /\ n^0-n^post0 == 0 /\ z^post0 <= 0 /\ -c1^post0 <= 0 /\ 1-m^30+m^post0 == 0 /\ -c1^20 <= 0 /\ -1+c1^40 <= 0 /\ -c2^20 <= 0 /\ 1-z^20+z^post0 == 0 /\ wpos^40 <= 0 /\ wpos^40 == 0 /\ -c1^10 <= 0 /\ 1-pi^20 <= 0 /\ 1-c1^post0 <= 0 /\ -1+c1^post0 <= 0 /\ 1+pi^10-pi^0 == 0 /\ 1-max^0+m^10 <= 0), cost: 1
New rule:
l0 -> l1 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : n^0'=n^post1, c2^0'=c2^post1, z^0'=z^post1, pos^0'=pos^post1, max^0'=max^post1, c1^0'=c1^post1, wpos^0'=wpos^post1, pi^0'=pi^post1, m^0'=m^post1, seq^0'=seq^post1, (-pi^post1+pi^0 == 0 /\ -c1^post1+c1^0 == 0 /\ n^0-n^post1 == 0 /\ z^0-z^post1 == 0 /\ c2^0-c2^post1 == 0 /\ m^0-m^post1 == 0 /\ max^0-max^post1 == 0 /\ -seq^post1+seq^0 == 0 /\ pos^0-pos^post1 == 0 /\ -wpos^post1+wpos^0 == 0), cost: 1
New rule:
l1 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : n^0'=n^post2, c2^0'=c2^post2, z^0'=z^post2, pos^0'=pos^post2, max^0'=max^post2, c1^0'=c1^post2, wpos^0'=wpos^post2, pi^0'=pi^post2, m^0'=m^post2, seq^0'=seq^post2, (0 == 0 /\ pos^11 <= 0 /\ pos^11 == 0 /\ pi^post2-seq^post2 == 0 /\ wpos^post2 == 0 /\ -n^post2 <= 0 /\ -1+seq^post2 == 0 /\ -z^post2 <= 0 /\ -1-pos^11+pos^post2 == 0 /\ c1^post2 <= 0 /\ z^post2 <= 0 /\ -max^post2 <= 0 /\ -1+c1^post2 <= 0 /\ -m^post2 <= 0 /\ -c2^post2+c2^0 == 0 /\ -n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -c1^post2 <= 0 /\ 1-m^post2 <= 0), cost: 1
New rule:
l2 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 1

Applied preprocessing
Original rule:
l3 -> l2 : n^0'=n^post3, c2^0'=c2^post3, z^0'=z^post3, pos^0'=pos^post3, max^0'=max^post3, c1^0'=c1^post3, wpos^0'=wpos^post3, pi^0'=pi^post3, m^0'=m^post3, seq^0'=seq^post3, (-pi^post3+pi^0 == 0 /\ c1^0-c1^post3 == 0 /\ wpos^0-wpos^post3 == 0 /\ -max^post3+max^0 == 0 /\ -seq^post3+seq^0 == 0 /\ -m^post3+m^0 == 0 /\ -pos^post3+pos^0 == 0 /\ n^0-n^post3 == 0 /\ c2^0-c2^post3 == 0 /\ z^0-z^post3 == 0), cost: 1
New rule:
l3 -> l2 : TRUE, cost: 1

Simplified rules
Start location: l3
   4: l0 -> l1 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 1
   5: l1 -> l0 : TRUE, cost: 1
   6: l2 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 1
   7: l3 -> l2 : TRUE, cost: 1


Eliminating location l2 by chaining:

Applied chaining
First rule:
l3 -> l2 : TRUE, cost: 1
Second rule:
l2 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 1
New rule:
l3 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 2

Applied deletion
Removed the following rules: 6 7

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 1
Second rule:
l1 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 4 5

Eliminated locations on linear paths
Start location: l3
   9: l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 2
   8: l3 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 2


Applied acceleration
Original rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=seq^0, seq^0'=1+seq^0, (z^0 <= 0 /\ -1+pos^0 == 0 /\ -2+m^0 >= 0 /\ wpos^0 == 0 /\ -1+pi^0 == 0 /\ 1-max^0+m^0 <= 0 /\ seq^0 >= 0), cost: 2
New rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=-1+n+seq^0, seq^0'=n+seq^0, (3-n-seq^0 >= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 >= 0 /\ -z^0 >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ -1+n >= 0 /\ pi^0-seq^0 <= 0 /\ -wpos^0 >= 0 /\ seq^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bmIObe.txt

Applied instantiation
Original rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=-1+n+seq^0, seq^0'=n+seq^0, (3-n-seq^0 >= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 >= 0 /\ -z^0 >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ -1+n >= 0 /\ pi^0-seq^0 <= 0 /\ -wpos^0 >= 0 /\ seq^0 >= 0), cost: 2*n
New rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=2, seq^0'=3, (0 >= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ 2-seq^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 >= 0 /\ -z^0 >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ pi^0-seq^0 <= 0 /\ -wpos^0 >= 0 /\ seq^0 >= 0), cost: 6-2*seq^0

Applied simplification
Original rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=2, seq^0'=3, (0 >= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ 2-seq^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 >= 0 /\ -z^0 >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ pi^0-seq^0 <= 0 /\ -wpos^0 >= 0 /\ seq^0 >= 0), cost: 6-2*seq^0
New rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=2, seq^0'=3, (z^0 <= 0 /\ -1+pos^0 <= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 <= 0 /\ wpos^0 >= 0 /\ -1+pi^0 <= 0 /\ -1+pi^0 >= 0 /\ pi^0-seq^0 <= 0 /\ -2+seq^0 <= 0), cost: 6-2*seq^0

Applied deletion
Removed the following rules: 9

Accelerated simple loops
Start location: l3
  11: l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=2, seq^0'=3, (z^0 <= 0 /\ -1+pos^0 <= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 <= 0 /\ wpos^0 >= 0 /\ -1+pi^0 <= 0 /\ -1+pi^0 >= 0 /\ pi^0-seq^0 <= 0 /\ -2+seq^0 <= 0), cost: 6-2*seq^0
   8: l3 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 2


Applied chaining
First rule:
l3 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 2
Second rule:
l0 -> l0 : c2^0'=0, z^0'=0, pos^0'=1, c1^0'=1, wpos^0'=0, pi^0'=2, seq^0'=3, (z^0 <= 0 /\ -1+pos^0 <= 0 /\ -1+pos^0 >= 0 /\ -1+max^0-m^0 >= 0 /\ -2+m^0 >= 0 /\ wpos^0 <= 0 /\ wpos^0 >= 0 /\ -1+pi^0 <= 0 /\ -1+pi^0 >= 0 /\ pi^0-seq^0 <= 0 /\ -2+seq^0 <= 0), cost: 6-2*seq^0
New rule:
l3 -> l0 : n^0'=n^post2, c2^0'=0, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=1, wpos^0'=0, pi^0'=2, m^0'=m^post2, seq^0'=3, (-2+m^post2 >= 0 /\ -1-m^post2+max^post2 >= 0 /\ -n^post2+max^post2 <= 0), cost: 6

Applied deletion
Removed the following rules: 11

Chained accelerated rules with incoming rules
Start location: l3
   8: l3 -> l0 : n^0'=n^post2, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=0, wpos^0'=0, pi^0'=1, m^0'=m^post2, seq^0'=1, (-n^post2+max^post2 <= 0 /\ m^post2-max^post2 <= 0 /\ -1+m^post2 >= 0), cost: 2
  12: l3 -> l0 : n^0'=n^post2, c2^0'=0, z^0'=0, pos^0'=1, max^0'=max^post2, c1^0'=1, wpos^0'=0, pi^0'=2, m^0'=m^post2, seq^0'=3, (-2+m^post2 >= 0 /\ -1-m^post2+max^post2 >= 0 /\ -n^post2+max^post2 <= 0), cost: 6


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0