unknown

Initial ITS

Start location: l3
Program variables: c1^0 c2^0 m^0 max^0 n^0 pi^0 pos^0 seq^0 wpos^0 z^0
   0: l0 -> l1 : c1^0'=c1^post1, c2^0'=c2^post1, m^0'=m^post1, max^0'=max^post1, n^0'=n^post1, pi^0'=pi^post1, pos^0'=pos^post1, seq^0'=seq^post1, wpos^0'=wpos^post1, z^0'=z^post1, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ -1+c1^3 <= 0 /\ 1-c1^2 <= 0 /\ -1+c1^2 <= 0 /\ -c1^2 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ -1+c2^3 <= 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ 1-c2^2 <= 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
   1: l1 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (-max^post2+max^0 == 0 /\ c2^0-c2^post2 == 0 /\ -pos^post2+pos^0 == 0 /\ seq^0-seq^post2 == 0 /\ -n^post2+n^0 == 0 /\ -m^post2+m^0 == 0 /\ -pi^post2+pi^0 == 0 /\ c1^0-c1^post2 == 0 /\ z^0-z^post2 == 0 /\ -wpos^post2+wpos^0 == 0), cost: 1
   2: l2 -> l0 : c1^0'=c1^post3, c2^0'=c2^post3, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=pi^post3, pos^0'=pos^post3, seq^0'=seq^post3, wpos^0'=wpos^post3, z^0'=z^post3, (0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -1+seq^post3 == 0 /\ -c2^post3+c2^0 == 0 /\ -n^post3 <= 0 /\ wpos^post3 == 0 /\ -1-pos^1+pos^post3 == 0 /\ -z^post3 <= 0 /\ -seq^post3+pi^post3 == 0 /\ z^post3 <= 0 /\ -max^post3 <= 0 /\ -1+c1^post3 <= 0 /\ -c1^post3 <= 0 /\ c1^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
   3: l3 -> l2 : c1^0'=c1^post4, c2^0'=c2^post4, m^0'=m^post4, max^0'=max^post4, n^0'=n^post4, pi^0'=pi^post4, pos^0'=pos^post4, seq^0'=seq^post4, wpos^0'=wpos^post4, z^0'=z^post4, (-pos^post4+pos^0 == 0 /\ -c2^post4+c2^0 == 0 /\ max^0-max^post4 == 0 /\ -wpos^post4+wpos^0 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ z^0-z^post4 == 0 /\ -c1^post4+c1^0 == 0 /\ -pi^post4+pi^0 == 0), cost: 1

Chained Linear Paths

Start location: l3
Program variables: c1^0 c2^0 m^0 max^0 n^0 pi^0 pos^0 seq^0 wpos^0 z^0
   5: l0 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ -1+c1^3 <= 0 /\ n^post1-n^post2 == 0 /\ 1-c1^2 <= 0 /\ -1+c1^2 <= 0 /\ z^post1-z^post2 == 0 /\ -c1^2 <= 0 /\ c1^post1-c1^post2 == 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ c2^post1-c2^post2 == 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ -1+c2^3 <= 0 /\ -m^post2+m^post1 == 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ seq^post1-seq^post2 == 0 /\ -pi^post2+pi^post1 == 0 /\ max^post1-max^post2 == 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ pos^post1-pos^post2 == 0 /\ 1-c2^2 <= 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ -wpos^post2+wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
   4: l3 -> l0 : c1^0'=c1^post3, c2^0'=c2^post3, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=pi^post3, pos^0'=pos^post3, seq^0'=seq^post3, wpos^0'=wpos^post3, z^0'=z^post3, (0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -1+seq^post3 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ wpos^post3 == 0 /\ -1-pos^1+pos^post3 == 0 /\ -z^post3 <= 0 /\ -c2^post3+c2^post4 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ -seq^post3+pi^post3 == 0 /\ z^0-z^post4 == 0 /\ z^post3 <= 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1+c1^post3 <= 0 /\ -pi^post4+pi^0 == 0 /\ -c1^post3 <= 0 /\ c1^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1

	Eliminating location l2 by chaining:

	Applied chaining

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

	Removed the following rules: 2 3
	
	Eliminating location l1 by chaining:

	Applied chaining

	First rule:
	l0 -> l1 : c1^0'=c1^post1, c2^0'=c2^post1, m^0'=m^post1, max^0'=max^post1, n^0'=n^post1, pi^0'=pi^post1, pos^0'=pos^post1, seq^0'=seq^post1, wpos^0'=wpos^post1, z^0'=z^post1, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ -1+c1^3 <= 0 /\ 1-c1^2 <= 0 /\ -1+c1^2 <= 0 /\ -c1^2 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ -1+c2^3 <= 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ 1-c2^2 <= 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	Second rule:
	l1 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (-max^post2+max^0 == 0 /\ c2^0-c2^post2 == 0 /\ -pos^post2+pos^0 == 0 /\ seq^0-seq^post2 == 0 /\ -n^post2+n^0 == 0 /\ -m^post2+m^0 == 0 /\ -pi^post2+pi^0 == 0 /\ c1^0-c1^post2 == 0 /\ z^0-z^post2 == 0 /\ -wpos^post2+wpos^0 == 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ -1+c1^3 <= 0 /\ n^post1-n^post2 == 0 /\ 1-c1^2 <= 0 /\ -1+c1^2 <= 0 /\ z^post1-z^post2 == 0 /\ -c1^2 <= 0 /\ c1^post1-c1^post2 == 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ c2^post1-c2^post2 == 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ -1+c2^3 <= 0 /\ -m^post2+m^post1 == 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ seq^post1-seq^post2 == 0 /\ -pi^post2+pi^post1 == 0 /\ max^post1-max^post2 == 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ pos^post1-pos^post2 == 0 /\ 1-c2^2 <= 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ -wpos^post2+wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 1

Simplified Transitions

Start location: l3
Program variables: c1^0 c2^0 m^0 max^0 n^0 pi^0 pos^0 seq^0 wpos^0 z^0
   7: l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
   6: l3 -> l0 : c1^0'=0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1

	made implied equalities explicit

	Original rule:
	l3 -> l0 : c1^0'=c1^post3, c2^0'=c2^post3, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=pi^post3, pos^0'=pos^post3, seq^0'=seq^post3, wpos^0'=wpos^post3, z^0'=z^post3, (0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -1+seq^post3 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ wpos^post3 == 0 /\ -1-pos^1+pos^post3 == 0 /\ -z^post3 <= 0 /\ -c2^post3+c2^post4 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ -seq^post3+pi^post3 == 0 /\ z^0-z^post4 == 0 /\ z^post3 <= 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1+c1^post3 <= 0 /\ -pi^post4+pi^0 == 0 /\ -c1^post3 <= 0 /\ c1^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	New rule:
	l3 -> l0 : c1^0'=c1^post3, c2^0'=c2^post3, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=pi^post3, pos^0'=pos^post3, seq^0'=seq^post3, wpos^0'=wpos^post3, z^0'=z^post3, (0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -1+seq^post3 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ wpos^post3 == 0 /\ -1-pos^1+pos^post3 == 0 /\ -z^post3 <= 0 /\ -z^post3 == 0 /\ -c2^post3+c2^post4 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ -seq^post3+pi^post3 == 0 /\ z^0-z^post4 == 0 /\ z^post3 <= 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1+c1^post3 <= 0 /\ -pi^post4+pi^0 == 0 /\ -c1^post3 <= 0 /\ -c1^post3 == 0 /\ c1^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l0 : c1^0'=c1^post3, c2^0'=c2^post3, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=pi^post3, pos^0'=pos^post3, seq^0'=seq^post3, wpos^0'=wpos^post3, z^0'=z^post3, (0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -1+seq^post3 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ wpos^post3 == 0 /\ -1-pos^1+pos^post3 == 0 /\ -z^post3 <= 0 /\ -z^post3 == 0 /\ -c2^post3+c2^post4 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ -seq^post3+pi^post3 == 0 /\ z^0-z^post4 == 0 /\ z^post3 <= 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1+c1^post3 <= 0 /\ -pi^post4+pi^0 == 0 /\ -c1^post3 <= 0 /\ -c1^post3 == 0 /\ c1^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	New rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^post4, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1+pos^1, seq^0'=1, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ z^0-z^post4 == 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1 <= 0 /\ -pi^post4+pi^0 == 0 /\ m^post3-max^post3 <= 0), cost: 1
	
		propagated equality seq^post3 = 1
		
		propagated equality wpos^post3 = 0
		
		propagated equality pos^post3 = 1+pos^1
		
		propagated equality z^post3 = 0
		
		propagated equality c2^post3 = c2^post4
		
		propagated equality pi^post3 = 1
		
		propagated equality c1^post3 = 0
		
	Propagated Equalities

	Original rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^post4, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1+pos^1, seq^0'=1, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ -pos^post4+pos^0 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ -m^post3 <= 0 /\ -c2^post4+c2^0 == 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ max^0-max^post4 == 0 /\ -n^post3 <= 0 /\ -wpos^post4+wpos^0 == 0 /\ m^0-m^post4 == 0 /\ -n^post4+n^0 == 0 /\ -seq^post4+seq^0 == 0 /\ z^0-z^post4 == 0 /\ -max^post3 <= 0 /\ -c1^post4+c1^0 == 0 /\ -1 <= 0 /\ -pi^post4+pi^0 == 0 /\ m^post3-max^post3 <= 0), cost: 1
	New rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ -m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ -1 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	
		propagated equality pos^post4 = pos^0
		
		propagated equality pos^1 = 0
		
		propagated equality c2^post4 = c2^0
		
		propagated equality max^post4 = max^0
		
		propagated equality wpos^post4 = wpos^0
		
		propagated equality m^post4 = m^0
		
		propagated equality n^post4 = n^0
		
		propagated equality seq^post4 = seq^0
		
		propagated equality z^post4 = z^0
		
		propagated equality c1^post4 = c1^0
		
		propagated equality pi^post4 = pi^0
		
	Simplified Guard

	Original rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ -m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ -1 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	New rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l0 : c1^0'=0, c2^0'=c2^0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	New rule:
	l3 -> l0 : c1^0'=0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l0 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ -1+c1^3 <= 0 /\ n^post1-n^post2 == 0 /\ 1-c1^2 <= 0 /\ -1+c1^2 <= 0 /\ z^post1-z^post2 == 0 /\ -c1^2 <= 0 /\ c1^post1-c1^post2 == 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ c2^post1-c2^post2 == 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ -1+c2^3 <= 0 /\ -m^post2+m^post1 == 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ seq^post1-seq^post2 == 0 /\ -pi^post2+pi^post1 == 0 /\ max^post1-max^post2 == 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ pos^post1-pos^post2 == 0 /\ 1-c2^2 <= 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ -wpos^post2+wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ -c2^1 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ c1^4 == 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ 1-c1^3 == 0 /\ -1+c1^3 <= 0 /\ n^post1-n^post2 == 0 /\ 1-c1^2 <= 0 /\ 1-c1^2 == 0 /\ -1+c1^2 <= 0 /\ z^post1-z^post2 == 0 /\ -c1^2 <= 0 /\ c1^post1-c1^post2 == 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -c2^post1 == 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ c2^post1-c2^post2 == 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ 1-wpos^1 == 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ 1-c2^3 == 0 /\ -1+c2^3 <= 0 /\ -m^post2+m^post1 == 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ seq^post1-seq^post2 == 0 /\ -pi^post2+pi^post1 == 0 /\ max^post1-max^post2 == 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ 1-pos^post1 == 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ pos^post1-pos^post2 == 0 /\ 1-c2^2 <= 0 /\ 1-c2^2 == 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ 1-c1^post1 == 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ 1-wpos^3 == 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ 1-wpos^5 == 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ -wpos^post2+wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ 1-c1^1 == 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l0 : c1^0'=c1^post2, c2^0'=c2^post2, m^0'=m^post2, max^0'=max^post2, n^0'=n^post2, pi^0'=pi^post2, pos^0'=pos^post2, seq^0'=seq^post2, wpos^0'=wpos^post2, z^0'=z^post2, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ -c2^1 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ c1^4 == 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ 1-c1^3 == 0 /\ -1+c1^3 <= 0 /\ n^post1-n^post2 == 0 /\ 1-c1^2 <= 0 /\ 1-c1^2 == 0 /\ -1+c1^2 <= 0 /\ z^post1-z^post2 == 0 /\ -c1^2 <= 0 /\ c1^post1-c1^post2 == 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -c2^post1 == 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ c2^post1-c2^post2 == 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ 1-wpos^1 == 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ 1-c2^3 == 0 /\ -1+c2^3 <= 0 /\ -m^post2+m^post1 == 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ seq^post1-seq^post2 == 0 /\ -pi^post2+pi^post1 == 0 /\ max^post1-max^post2 == 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ 1-pos^post1 == 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ pos^post1-pos^post2 == 0 /\ 1-c2^2 <= 0 /\ 1-c2^2 == 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ 1-c1^post1 == 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ 1-wpos^3 == 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ 1-wpos^5 == 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ -wpos^post2+wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ 1-c1^1 == 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=c1^post1, c2^0'=c2^post1, m^0'=m^post1, max^0'=max^post1, n^0'=n^post1, pi^0'=pi^post1, pos^0'=pos^post1, seq^0'=seq^post1, wpos^0'=wpos^post1, z^0'=z^post1, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ -c2^1 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ c1^4 == 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ 1-c1^3 == 0 /\ -1+c1^3 <= 0 /\ 1-c1^2 <= 0 /\ 1-c1^2 == 0 /\ -1+c1^2 <= 0 /\ -c1^2 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -c2^post1 == 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ 1-wpos^1 == 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ 1-c2^3 == 0 /\ -1+c2^3 <= 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ 1-pos^post1 == 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ 1-c2^2 <= 0 /\ 1-c2^2 == 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ 1-c1^post1 == 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ 1-wpos^3 == 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ 1-wpos^5 == 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ 1-c1^1 == 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	
		propagated equality n^post2 = n^post1
		
		propagated equality z^post2 = z^post1
		
		propagated equality c1^post2 = c1^post1
		
		propagated equality c2^post2 = c2^post1
		
		propagated equality m^post2 = m^post1
		
		propagated equality seq^post2 = seq^post1
		
		propagated equality pi^post2 = pi^post1
		
		propagated equality max^post2 = max^post1
		
		propagated equality pos^post2 = pos^post1
		
		propagated equality wpos^post2 = wpos^post1
		
	Propagated Equalities

	Original rule:
	l0 -> l0 : c1^0'=c1^post1, c2^0'=c2^post1, m^0'=m^post1, max^0'=max^post1, n^0'=n^post1, pi^0'=pi^post1, pos^0'=pos^post1, seq^0'=seq^post1, wpos^0'=wpos^post1, z^0'=z^post1, (0 == 0 /\ -1+c2^1 <= 0 /\ -c2^1 <= 0 /\ -c2^1 == 0 /\ pos^1 <= 0 /\ pos^1 == 0 /\ 1+pi^1-pi^0 == 0 /\ 1-m^0+m^1 == 0 /\ c1^4 <= 0 /\ c1^4 == 0 /\ -c1^3 <= 0 /\ -1+m^2-m^1 == 0 /\ wpos^2 <= 0 /\ wpos^2 == 0 /\ 1-c1^3 <= 0 /\ 1-c1^3 == 0 /\ -1+c1^3 <= 0 /\ 1-c1^2 <= 0 /\ 1-c1^2 == 0 /\ -1+c1^2 <= 0 /\ -c1^2 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ pi^2-seq^post1 == 0 /\ 1-z^1 <= 0 /\ -1+c2^post1 <= 0 /\ -1-m^2+m^3 == 0 /\ -c2^post1 <= 0 /\ -c2^post1 == 0 /\ -z^1 <= 0 /\ -1-pos^1+pos^post1 == 0 /\ -c1^4 <= 0 /\ z^0 <= 0 /\ -1+c1^4 <= 0 /\ 1+z^post1-z^2 == 0 /\ 1-m^0 <= 0 /\ 1-wpos^1 <= 0 /\ 1-wpos^1 == 0 /\ -1+wpos^1 <= 0 /\ -1-seq^0+seq^post1 == 0 /\ 1-c2^3 <= 0 /\ 1-c2^3 == 0 /\ -1+c2^3 <= 0 /\ 1-z^1+z^2 == 0 /\ -c2^3 <= 0 /\ -n^post1+n^0 == 0 /\ pi^1 <= 0 /\ 1-m^2 <= 0 /\ c2^1 <= 0 /\ 1+m^2-max^0 <= 0 /\ 1-m^1 <= 0 /\ -c2^2 <= 0 /\ 1-pos^post1 <= 0 /\ 1-pos^post1 == 0 /\ -1+pos^post1 <= 0 /\ 1+m^1-max^0 <= 0 /\ 1-c2^2 <= 0 /\ 1-c2^2 == 0 /\ -1+c2^2 <= 0 /\ 1-m^3+m^post1 == 0 /\ 1-c1^post1 <= 0 /\ 1-c1^post1 == 0 /\ -1+c1^post1 <= 0 /\ -1-wpos^2+wpos^3 == 0 /\ 1-pi^0 <= 0 /\ c2^post1 <= 0 /\ -c1^post1 <= 0 /\ 1-m^3 <= 0 /\ 1-pi^2+pi^post1 == 0 /\ wpos^4 <= 0 /\ wpos^4 == 0 /\ -1+wpos^1-wpos^0 == 0 /\ 1-pi^2 <= 0 /\ 1-z^2 <= 0 /\ 1-wpos^3 <= 0 /\ 1-wpos^3 == 0 /\ -1+wpos^3 <= 0 /\ -max^post1+max^0 == 0 /\ wpos^0 <= 0 /\ 1-wpos^5 <= 0 /\ 1-wpos^5 == 0 /\ -1+wpos^5 <= 0 /\ wpos^post1 == 0 /\ 1-c1^1 <= 0 /\ 1-c1^1 == 0 /\ -1+c1^1 <= 0 /\ -1-wpos^4+wpos^5 == 0 /\ -c1^1 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (0 <= 0 /\ 0 == 0 /\ m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
		propagated equality c2^1 = 0
		
		propagated equality pos^1 = 0
		
		propagated equality pi^1 = -1+pi^0
		
		propagated equality m^1 = -1+m^0
		
		propagated equality c1^4 = 0
		
		propagated equality m^2 = m^0
		
		propagated equality wpos^2 = 0
		
		propagated equality c1^3 = 1
		
		propagated equality c1^2 = 1
		
		propagated equality pi^2 = seq^post1
		
		propagated equality m^3 = 1+m^0
		
		propagated equality c2^post1 = 0
		
		propagated equality pos^post1 = 1
		
		propagated equality z^2 = 1+z^post1
		
		propagated equality wpos^1 = 1
		
		propagated equality seq^post1 = 1+seq^0
		
		propagated equality c2^3 = 1
		
		propagated equality z^1 = 2+z^post1
		
		propagated equality n^post1 = n^0
		
		propagated equality c2^2 = 1
		
		propagated equality m^post1 = m^0
		
		propagated equality c1^post1 = 1
		
		propagated equality wpos^3 = 1
		
		propagated equality pi^post1 = seq^0
		
		propagated equality wpos^4 = 0
		
		propagated equality max^post1 = max^0
		
		propagated equality wpos^5 = 1
		
		propagated equality wpos^post1 = 0
		
		propagated equality c1^1 = 1
		
	Simplified Guard

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (0 <= 0 /\ 0 == 0 /\ m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ z^post1 == 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ z^post1 == 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ m^0-max^0 <= 0 /\ -2 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
		propagated equality z^post1 = 0
		
	Simplified Guard

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ m^0-max^0 <= 0 /\ -2 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, m^0'=m^0, max^0'=max^0, n^0'=n^0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ z^post1 == 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=z^post1, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ z^post1 <= 0 /\ z^post1 == 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ -2-z^post1 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ -z^post1 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1-z^post1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	New rule:
	l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (0 <= 0 /\ 0 == 0 /\ m^0-max^0 <= 0 /\ -2 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -1 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
	
		propagated equality z^post1 = 0
		
	Simplified Guard

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

Step with 6

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)]
	
	Blocked

	[{}, {}]

Step with 7

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)], 7[(m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Accelerate

Start location: l3
Program variables: c1^0 c2^0 m^0 max^0 n^0 pi^0 pos^0 seq^0 wpos^0 z^0
   7: l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=seq^0, pos^0'=1, seq^0'=1+seq^0, wpos^0'=0, z^0'=0, (m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0), cost: 1
   8: l0 -> l0 : c1^0'=1, c2^0'=0, pi^0'=-1+seq^0+n, pos^0'=1, seq^0'=seq^0+n, wpos^0'=0, z^0'=0, (-seq^0+pi^0 <= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+m^0 >= 0 /\ -m^0+max^0 >= 0 /\ seq^0 >= 0 /\ -z^0 >= 0 /\ -1+n >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ -2+m^0 >= 0 /\ m^0 >= 0 /\ 3-seq^0-n >= 0 /\ -1-m^0+max^0 >= 0 /\ -wpos^0 >= 0 /\ wpos^0 >= 0), cost: 1
   6: l3 -> l0 : c1^0'=0, m^0'=m^post3, max^0'=max^post3, n^0'=n^post3, pi^0'=1, pos^0'=1, seq^0'=1, wpos^0'=0, z^0'=0, (-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0), cost: 1

	Loop Acceleration

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

		1-pos^0 >= 0 [0]: monotonic increase yields 1-pos^0 >= 0
		
		-1+pos^0 >= 0 [0]: monotonic increase yields -1+pos^0 >= 0
		
		-1+m^0 >= 0 [0]: monotonic increase yields -1+m^0 >= 0
		
		-m^0+max^0 >= 0 [0]: monotonic increase yields -m^0+max^0 >= 0
		
		seq^0 >= 0 [0]: monotonic increase yields seq^0 >= 0
		
		-z^0 >= 0 [0]: monotonic increase yields -z^0 >= 0
		
		1-pi^0 >= 0 [0]: eventual decrease yields (1-pi^0 >= 0 /\ 3-seq^0-n >= 0)
		
		-1+pi^0 >= 0 [0]: eventual increase yields (-seq^0+pi^0 <= 0 /\ -1+pi^0 >= 0)
		
		-2+m^0 >= 0 [0]: monotonic increase yields -2+m^0 >= 0
		
		m^0 >= 0 [0]: monotonic increase yields m^0 >= 0, dependencies: -1+m^0 >= 0
		
		-1-m^0+max^0 >= 0 [0]: monotonic increase yields -1-m^0+max^0 >= 0
		
		-wpos^0 >= 0 [0]: monotonic increase yields -wpos^0 >= 0
		
		wpos^0 >= 0 [0]: monotonic increase yields wpos^0 >= 0
		
		Replacement map: {1-pos^0 >= 0 -> 1-pos^0 >= 0, -1+pos^0 >= 0 -> -1+pos^0 >= 0, -1+m^0 >= 0 -> -1+m^0 >= 0, -m^0+max^0 >= 0 -> -m^0+max^0 >= 0, seq^0 >= 0 -> seq^0 >= 0, -z^0 >= 0 -> -z^0 >= 0, 1-pi^0 >= 0 -> (1-pi^0 >= 0 /\ 3-seq^0-n >= 0), -1+pi^0 >= 0 -> (-seq^0+pi^0 <= 0 /\ -1+pi^0 >= 0), -2+m^0 >= 0 -> -2+m^0 >= 0, m^0 >= 0 -> m^0 >= 0, -1-m^0+max^0 >= 0 -> -1-m^0+max^0 >= 0, -wpos^0 >= 0 -> -wpos^0 >= 0, wpos^0 >= 0 -> wpos^0 >= 0}

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)], 8[(-seq^0+pi^0 <= 0 /\ 1-pos^0 >= 0 /\ -1+pos^0 >= 0 /\ -1+m^0 >= 0 /\ -m^0+max^0 >= 0 /\ seq^0 >= 0 /\ -z^0 >= 0 /\ -1+n >= 0 /\ 1-pi^0 >= 0 /\ -1+pi^0 >= 0 /\ -2+m^0 >= 0 /\ m^0 >= 0 /\ 3-seq^0-n >= 0 /\ -1-m^0+max^0 >= 0 /\ -wpos^0 >= 0 /\ wpos^0 >= 0)]
	
	Blocked

	[{}, {}, {7[T], 8[T]}]

Backtrack

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)]
	
	Blocked

	[{}, {8[T]}]

Step with 7

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)], 7[(m^0-max^0 <= 0 /\ 2-m^0 <= 0 /\ 1+m^0-max^0 <= 0 /\ 1-pos^0 <= 0 /\ 1-pos^0 == 0 /\ -1+pos^0 <= 0 /\ z^0 <= 0 /\ 1-m^0 <= 0 /\ -m^0 <= 0 /\ 1-pi^0 <= 0 /\ 1-pi^0 == 0 /\ -1+pi^0 <= 0 /\ -wpos^0 == 0 /\ -seq^0 <= 0 /\ wpos^0 <= 0)]
	
	Blocked

	[{}, {8[T]}, {}]

Covered

	Trace

	6[(-m^post3 <= 0 /\ 1-m^post3 <= 0 /\ -n^post3+max^post3 <= 0 /\ -n^post3 <= 0 /\ -max^post3 <= 0 /\ m^post3-max^post3 <= 0)]
	
	Blocked

	[{}, {7[T], 8[T]}]

Backtrack

	Trace

	Blocked

	[{6[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b