NO

Initial ITS

Start location: l9
Program variables: a^0 dobreak^0 n^0 r^0
   0: l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ -dobreak^post1+dobreak^0 == 0 /\ dobreak^0 <= 0 /\ a^post1 == 0 /\ -r^post1+r^0 == 0 /\ -1+a^1 == 0), cost: 1
   1: l0 -> l2 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (1-dobreak^0 <= 0 /\ n^0-n^post2 == 0 /\ -r^post2+r^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0), cost: 1
   3: l1 -> l4 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0-dobreak^post4 == 0 /\ n^0-n^post4 == 0 /\ -a^post4+a^0 == 0 /\ -r^post4+r^0 == 0), cost: 1
   5: l2 -> l7 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-dobreak^post6+dobreak^0 == 0 /\ -r^post6+r^0 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0), cost: 1
   2: l3 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (n^0-n^post3 == 0 /\ -r^post3+r^0 == 0 /\ -dobreak^post3+dobreak^0 == 0 /\ -a^post3+a^0 == 0), cost: 1
   7: l4 -> l1 : a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (1+n^post8-n^0 == 0 /\ -a^post8+a^0 == 0 /\ 1-n^0 <= 0 /\ -r^post8+r^0 == 0 /\ dobreak^0-dobreak^post8 == 0), cost: 1
   8: l4 -> l3 : a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0 /\ n^0-n^post9 == 0 /\ a^0-a^post9 == 0 /\ r^post9 == 0), cost: 1
   4: l5 -> l6 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (n^0-n^post5 == 0 /\ -r^post5+r^0 == 0 /\ -a^post5+a^0 == 0 /\ -dobreak^post5+dobreak^0 == 0), cost: 1
   6: l7 -> l2 : a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (-a^post7+a^0 == 0 /\ n^0-n^post7 == 0 /\ -dobreak^post7+dobreak^0 == 0 /\ -r^post7+r^0 == 0), cost: 1
   9: l8 -> l3 : a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ n^0-n^post10 == 0 /\ r^post10 == 0 /\ a^post10 == 0), cost: 1
  10: l9 -> l8 : a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (-r^post11+r^0 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1

Chained Linear Paths

Start location: l9
Program variables: a^0 dobreak^0 n^0 r^0
   0: l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ -dobreak^post1+dobreak^0 == 0 /\ dobreak^0 <= 0 /\ a^post1 == 0 /\ -r^post1+r^0 == 0 /\ -1+a^1 == 0), cost: 1
   1: l0 -> l2 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (1-dobreak^0 <= 0 /\ n^0-n^post2 == 0 /\ -r^post2+r^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0), cost: 1
   3: l1 -> l4 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0-dobreak^post4 == 0 /\ n^0-n^post4 == 0 /\ -a^post4+a^0 == 0 /\ -r^post4+r^0 == 0), cost: 1
  12: l2 -> l2 : a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (-dobreak^post6+dobreak^0 == 0 /\ -a^post7+a^post6 == 0 /\ -r^post6+r^0 == 0 /\ dobreak^post6-dobreak^post7 == 0 /\ n^post6-n^post7 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0 /\ -r^post7+r^post6 == 0), cost: 1
   2: l3 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (n^0-n^post3 == 0 /\ -r^post3+r^0 == 0 /\ -dobreak^post3+dobreak^0 == 0 /\ -a^post3+a^0 == 0), cost: 1
   7: l4 -> l1 : a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (1+n^post8-n^0 == 0 /\ -a^post8+a^0 == 0 /\ 1-n^0 <= 0 /\ -r^post8+r^0 == 0 /\ dobreak^0-dobreak^post8 == 0), cost: 1
   8: l4 -> l3 : a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0 /\ n^0-n^post9 == 0 /\ a^0-a^post9 == 0 /\ r^post9 == 0), cost: 1
   4: l5 -> l6 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (n^0-n^post5 == 0 /\ -r^post5+r^0 == 0 /\ -a^post5+a^0 == 0 /\ -dobreak^post5+dobreak^0 == 0), cost: 1
  11: l9 -> l3 : a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ -r^post11+r^0 == 0 /\ n^post11-n^post10 == 0 /\ r^post10 == 0 /\ a^post10 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1

	Eliminating location l8 by chaining:

	Applied chaining

	First rule:
	l9 -> l8 : a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (-r^post11+r^0 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1
	Second rule:
	l8 -> l3 : a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ n^0-n^post10 == 0 /\ r^post10 == 0 /\ a^post10 == 0), cost: 1
	New rule:
	l9 -> l3 : a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ -r^post11+r^0 == 0 /\ n^post11-n^post10 == 0 /\ r^post10 == 0 /\ a^post10 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 9 10
	
	Eliminating location l7 by chaining:

	Applied chaining

	First rule:
	l2 -> l7 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-dobreak^post6+dobreak^0 == 0 /\ -r^post6+r^0 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0), cost: 1
	Second rule:
	l7 -> l2 : a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (-a^post7+a^0 == 0 /\ n^0-n^post7 == 0 /\ -dobreak^post7+dobreak^0 == 0 /\ -r^post7+r^0 == 0), cost: 1
	New rule:
	l2 -> l2 : a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (-dobreak^post6+dobreak^0 == 0 /\ -a^post7+a^post6 == 0 /\ -r^post6+r^0 == 0 /\ dobreak^post6-dobreak^post7 == 0 /\ n^post6-n^post7 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0 /\ -r^post7+r^post6 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 5 6

Simplified Transitions

Start location: l9
Program variables: a^0 dobreak^0 n^0 r^0
  13: l0 -> l1 : a^0'=0, n^0'=n^post1, dobreak^0 <= 0, cost: 1
  14: l0 -> l2 : 1-dobreak^0 <= 0, cost: 1
  16: l1 -> l4 : T, cost: 1
  21: l2 -> l2 : T, cost: 1
  15: l3 -> l0 : T, cost: 1
  18: l4 -> l1 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1
  19: l4 -> l3 : dobreak^0'=dobreak^post9, r^0'=0, n^0 <= 0, cost: 1
  17: l5 -> l6 : T, cost: 1
  20: l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (0 == 0 /\ -dobreak^post1+dobreak^0 == 0 /\ dobreak^0 <= 0 /\ a^post1 == 0 /\ -r^post1+r^0 == 0 /\ -1+a^1 == 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1
	
		propagated equality dobreak^post1 = dobreak^0
		
		propagated equality a^post1 = 0
		
		propagated equality r^post1 = r^0
		
	Propagated Equalities

	Original rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1
	
		propagated equality a^1 = 1
		
	Simplified Guard

	Original rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, dobreak^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post1, r^0'=r^0, dobreak^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : a^0'=0, n^0'=n^post1, dobreak^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l2 : a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (1-dobreak^0 <= 0 /\ n^0-n^post2 == 0 /\ -r^post2+r^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0), cost: 1
	New rule:
	l0 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-dobreak^0 <= 0), cost: 1
	
		propagated equality n^post2 = n^0
		
		propagated equality r^post2 = r^0
		
		propagated equality dobreak^post2 = dobreak^0
		
		propagated equality a^post2 = a^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-dobreak^0 <= 0), cost: 1
	New rule:
	l0 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-dobreak^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-dobreak^0 <= 0, cost: 1
	New rule:
	l0 -> l2 : 1-dobreak^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l0 : a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (n^0-n^post3 == 0 /\ -r^post3+r^0 == 0 /\ -dobreak^post3+dobreak^0 == 0 /\ -a^post3+a^0 == 0), cost: 1
	New rule:
	l3 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	
		propagated equality n^post3 = n^0
		
		propagated equality r^post3 = r^0
		
		propagated equality dobreak^post3 = dobreak^0
		
		propagated equality a^post3 = a^0
		
	Simplified Guard

	Original rule:
	l3 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	New rule:
	l3 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l0 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	New rule:
	l3 -> l0 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l4 : a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (dobreak^0-dobreak^post4 == 0 /\ n^0-n^post4 == 0 /\ -a^post4+a^0 == 0 /\ -r^post4+r^0 == 0), cost: 1
	New rule:
	l1 -> l4 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	
		propagated equality dobreak^post4 = dobreak^0
		
		propagated equality n^post4 = n^0
		
		propagated equality a^post4 = a^0
		
		propagated equality r^post4 = r^0
		
	Simplified Guard

	Original rule:
	l1 -> l4 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	New rule:
	l1 -> l4 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l4 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	New rule:
	l1 -> l4 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (n^0-n^post5 == 0 /\ -r^post5+r^0 == 0 /\ -a^post5+a^0 == 0 /\ -dobreak^post5+dobreak^0 == 0), cost: 1
	New rule:
	l5 -> l6 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	
		propagated equality n^post5 = n^0
		
		propagated equality r^post5 = r^0
		
		propagated equality a^post5 = a^0
		
		propagated equality dobreak^post5 = dobreak^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	New rule:
	l5 -> l6 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	New rule:
	l5 -> l6 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l1 : a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (1+n^post8-n^0 == 0 /\ -a^post8+a^0 == 0 /\ 1-n^0 <= 0 /\ -r^post8+r^0 == 0 /\ dobreak^0-dobreak^post8 == 0), cost: 1
	New rule:
	l4 -> l1 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1
	
		propagated equality n^post8 = -1+n^0
		
		propagated equality a^post8 = a^0
		
		propagated equality r^post8 = r^0
		
		propagated equality dobreak^post8 = dobreak^0
		
	Simplified Guard

	Original rule:
	l4 -> l1 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1
	New rule:
	l4 -> l1 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l1 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=-1+n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1
	New rule:
	l4 -> l1 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l3 : a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0 /\ n^0-n^post9 == 0 /\ a^0-a^post9 == 0 /\ r^post9 == 0), cost: 1
	New rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0), cost: 1
	
		propagated equality n^post9 = n^0
		
		propagated equality a^post9 = a^0
		
		propagated equality r^post9 = 0
		
	Propagated Equalities

	Original rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0), cost: 1
	New rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1
	
		propagated equality r^1 = 1
		
	Simplified Guard

	Original rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1
	New rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l3 : a^0'=a^0, dobreak^0'=dobreak^post9, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1
	New rule:
	l4 -> l3 : dobreak^0'=dobreak^post9, r^0'=0, n^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l3 : a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ -r^post11+r^0 == 0 /\ n^post11-n^post10 == 0 /\ r^post10 == 0 /\ a^post10 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1
	New rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ -r^post11+r^0 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1
	
		propagated equality n^post10 = n^post11
		
		propagated equality r^post10 = 0
		
		propagated equality a^post10 = 0
		
	Propagated Equalities

	Original rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ -r^post11+r^0 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ n^0-n^post11 == 0), cost: 1
	New rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, 0 == 0, cost: 1
	
		propagated equality r^post11 = r^0
		
		propagated equality dobreak^post11 = dobreak^0
		
		propagated equality a^post11 = a^0
		
		propagated equality n^post11 = n^0
		
	Simplified Guard

	Original rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, 0 == 0, cost: 1
	New rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, T, cost: 1
	New rule:
	l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l2 : a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (-dobreak^post6+dobreak^0 == 0 /\ -a^post7+a^post6 == 0 /\ -r^post6+r^0 == 0 /\ dobreak^post6-dobreak^post7 == 0 /\ n^post6-n^post7 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0 /\ -r^post7+r^post6 == 0), cost: 1
	New rule:
	l2 -> l2 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (0 == 0 /\ -dobreak^post6+dobreak^0 == 0 /\ -r^post6+r^0 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0), cost: 1
	
		propagated equality a^post7 = a^post6
		
		propagated equality dobreak^post7 = dobreak^post6
		
		propagated equality n^post7 = n^post6
		
		propagated equality r^post7 = r^post6
		
	Propagated Equalities

	Original rule:
	l2 -> l2 : a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (0 == 0 /\ -dobreak^post6+dobreak^0 == 0 /\ -r^post6+r^0 == 0 /\ a^0-a^post6 == 0 /\ n^0-n^post6 == 0), cost: 1
	New rule:
	l2 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	
		propagated equality dobreak^post6 = dobreak^0
		
		propagated equality r^post6 = r^0
		
		propagated equality a^post6 = a^0
		
		propagated equality n^post6 = n^0
		
	Simplified Guard

	Original rule:
	l2 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1
	New rule:
	l2 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l2 : a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1
	New rule:
	l2 -> l2 : T, cost: 1

Step with 20

	Trace

	20[T]
	
	Blocked

	[{}, {}]

Step with 15

	Trace

	20[T], 15[T]
	
	Blocked

	[{}, {}, {}]

Step with 14

	Trace

	20[T], 15[T], 14[(1-dobreak^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}]

Step with 21

	Trace

	20[T], 15[T], 14[(1-dobreak^0 <= 0)], 21[T]
	
	Blocked

	[{}, {}, {}, {}, {}]

Nonterm

Start location: l9
Program variables: a^0 dobreak^0 n^0 r^0
  13: l0 -> l1 : a^0'=0, n^0'=n^post1, dobreak^0 <= 0, cost: 1
  14: l0 -> l2 : 1-dobreak^0 <= 0, cost: 1
  16: l1 -> l4 : T, cost: 1
  21: l2 -> l2 : T, cost: 1
  22: l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM
  15: l3 -> l0 : T, cost: 1
  18: l4 -> l1 : n^0'=-1+n^0, 1-n^0 <= 0, cost: 1
  19: l4 -> l3 : dobreak^0'=dobreak^post9, r^0'=0, n^0 <= 0, cost: 1
  17: l5 -> l6 : T, cost: 1
  20: l9 -> l3 : a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l2 -> l2 : T, cost: 1
	New rule:
	l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM

		Replacement map: {}

Step with 22

	Trace

	20[T], 15[T], 14[(1-dobreak^0 <= 0)], 22[-1+n >= 0]
	
	Blocked

	[{}, {}, {}, {}, {22[T]}]

Refute

	Counterexample

	[ a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 20 [ a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 15 [ a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 14 [ a^0=a^0 dobreak^0=dobreak^0 n^0=0 r^0=r^0 ] 22
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b