NO

Initial ITS

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

Chained Linear Paths

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

	Eliminating location l6 by chaining:

	Applied chaining

	First rule:
	l7 -> l6 : i^0'=i^post10, j^0'=j^post10, (-i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1
	Second rule:
	l6 -> l2 : i^0'=i^post9, j^0'=j^post9, (i^post9 == 0 /\ -j^post9+j^0 == 0), cost: 1
	New rule:
	l7 -> l2 : i^0'=i^post9, j^0'=j^post9, (i^post9 == 0 /\ -i^post10+i^0 == 0 /\ j^post10-j^post9 == 0 /\ -j^post10+j^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 8 9

Simplified Transitions

Start location: l7
Program variables: i^0 j^0
  11: l0 -> l1 : j^0'=i^0, T, cost: 1
  12: l1 -> l2 : i^0'=1+i^0, T, cost: 1
  18: l2 -> l4 : T, cost: 1
  13: l3 -> l0 : 6-i^0 <= 0, cost: 1
  14: l3 -> l0 : -4+i^0 <= 0, cost: 1
  15: l3 -> l1 : i^0'=i^post5, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
  16: l4 -> l5 : 10-i^0 <= 0, cost: 1
  17: l4 -> l3 : -9+i^0 <= 0, cost: 1
  19: l7 -> l2 : i^0'=0, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : i^0'=i^post1, j^0'=j^post1, (-i^post1+i^0 == 0 /\ j^post1-i^0 == 0), cost: 1
	New rule:
	l0 -> l1 : i^0'=i^0, j^0'=i^0, 0 == 0, cost: 1
	
		propagated equality i^post1 = i^0
		
		propagated equality j^post1 = i^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : i^0'=i^0, j^0'=i^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : i^0'=i^0, j^0'=i^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : i^0'=i^0, j^0'=i^0, T, cost: 1
	New rule:
	l0 -> l1 : j^0'=i^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l2 : i^0'=i^post2, j^0'=j^post2, (-1+i^post2-i^0 == 0 /\ -j^post2+j^0 == 0), cost: 1
	New rule:
	l1 -> l2 : i^0'=1+i^0, j^0'=j^0, 0 == 0, cost: 1
	
		propagated equality i^post2 = 1+i^0
		
		propagated equality j^post2 = j^0
		
	Simplified Guard

	Original rule:
	l1 -> l2 : i^0'=1+i^0, j^0'=j^0, 0 == 0, cost: 1
	New rule:
	l1 -> l2 : i^0'=1+i^0, j^0'=j^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l2 : i^0'=1+i^0, j^0'=j^0, T, cost: 1
	New rule:
	l1 -> l2 : i^0'=1+i^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l0 : i^0'=i^post3, j^0'=j^post3, (-i^post3+i^0 == 0 /\ 6-i^0 <= 0 /\ j^0-j^post3 == 0), cost: 1
	New rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ 6-i^0 <= 0), cost: 1
	
		propagated equality i^post3 = i^0
		
		propagated equality j^post3 = j^0
		
	Simplified Guard

	Original rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ 6-i^0 <= 0), cost: 1
	New rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, 6-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, 6-i^0 <= 0, cost: 1
	New rule:
	l3 -> l0 : 6-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l0 : i^0'=i^post4, j^0'=j^post4, (-4+i^0 <= 0 /\ -j^post4+j^0 == 0 /\ -i^post4+i^0 == 0), cost: 1
	New rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ -4+i^0 <= 0), cost: 1
	
		propagated equality j^post4 = j^0
		
		propagated equality i^post4 = i^0
		
	Simplified Guard

	Original rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ -4+i^0 <= 0), cost: 1
	New rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, -4+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l0 : i^0'=i^0, j^0'=j^0, -4+i^0 <= 0, cost: 1
	New rule:
	l3 -> l0 : -4+i^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -5+i^0 <= 0 /\ 5-i^0 <= 0 /\ -j^post5+j^0 == 0), cost: 1
	New rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0 /\ -j^post5+j^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^post5, (0 == 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0 /\ -j^post5+j^0 == 0), cost: 1
	New rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (0 == 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	
		propagated equality j^post5 = j^0
		
	Simplified Guard

	Original rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (0 == 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	New rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	New rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l1 : i^0'=i^post5, j^0'=j^0, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	New rule:
	l3 -> l1 : i^0'=i^post5, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l5 : i^0'=i^post6, j^0'=j^post6, (10-i^0 <= 0 /\ j^0-j^post6 == 0 /\ -i^post6+i^0 == 0), cost: 1
	New rule:
	l4 -> l5 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ 10-i^0 <= 0), cost: 1
	
		propagated equality j^post6 = j^0
		
		propagated equality i^post6 = i^0
		
	Simplified Guard

	Original rule:
	l4 -> l5 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ 10-i^0 <= 0), cost: 1
	New rule:
	l4 -> l5 : i^0'=i^0, j^0'=j^0, 10-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l5 : i^0'=i^0, j^0'=j^0, 10-i^0 <= 0, cost: 1
	New rule:
	l4 -> l5 : 10-i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l3 : i^0'=i^post7, j^0'=j^post7, (-9+i^0 <= 0 /\ -j^post7+j^0 == 0 /\ -i^post7+i^0 == 0), cost: 1
	New rule:
	l4 -> l3 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ -9+i^0 <= 0), cost: 1
	
		propagated equality j^post7 = j^0
		
		propagated equality i^post7 = i^0
		
	Simplified Guard

	Original rule:
	l4 -> l3 : i^0'=i^0, j^0'=j^0, (0 == 0 /\ -9+i^0 <= 0), cost: 1
	New rule:
	l4 -> l3 : i^0'=i^0, j^0'=j^0, -9+i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l3 : i^0'=i^0, j^0'=j^0, -9+i^0 <= 0, cost: 1
	New rule:
	l4 -> l3 : -9+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l4 : i^0'=i^post8, j^0'=j^post8, (-i^post8+i^0 == 0 /\ j^0-j^post8 == 0), cost: 1
	New rule:
	l2 -> l4 : i^0'=i^0, j^0'=j^0, 0 == 0, cost: 1
	
		propagated equality i^post8 = i^0
		
		propagated equality j^post8 = j^0
		
	Simplified Guard

	Original rule:
	l2 -> l4 : i^0'=i^0, j^0'=j^0, 0 == 0, cost: 1
	New rule:
	l2 -> l4 : i^0'=i^0, j^0'=j^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l4 : i^0'=i^0, j^0'=j^0, T, cost: 1
	New rule:
	l2 -> l4 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l2 : i^0'=i^post9, j^0'=j^post9, (i^post9 == 0 /\ -i^post10+i^0 == 0 /\ j^post10-j^post9 == 0 /\ -j^post10+j^0 == 0), cost: 1
	New rule:
	l7 -> l2 : i^0'=0, j^0'=j^post10, (0 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1
	
		propagated equality i^post9 = 0
		
		propagated equality j^post9 = j^post10
		
	Propagated Equalities

	Original rule:
	l7 -> l2 : i^0'=0, j^0'=j^post10, (0 == 0 /\ -i^post10+i^0 == 0 /\ -j^post10+j^0 == 0), cost: 1
	New rule:
	l7 -> l2 : i^0'=0, j^0'=j^0, 0 == 0, cost: 1
	
		propagated equality i^post10 = i^0
		
		propagated equality j^post10 = j^0
		
	Simplified Guard

	Original rule:
	l7 -> l2 : i^0'=0, j^0'=j^0, 0 == 0, cost: 1
	New rule:
	l7 -> l2 : i^0'=0, j^0'=j^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l2 : i^0'=0, j^0'=j^0, T, cost: 1
	New rule:
	l7 -> l2 : i^0'=0, T, cost: 1

Step with 19

	Trace

	19[T]
	
	Blocked

	[{}, {}]

Step with 18

	Trace

	19[T], 18[T]
	
	Blocked

	[{}, {}, {}]

Step with 17

	Trace

	19[T], 18[T], 17[(-9+i^0 <= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {}]

Step with 14

	Trace

	19[T], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)]
	
	Blocked

	[{}, {}, {16[T]}, {13[T]}, {}]

Step with 11

	Trace

	19[T], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)], 11[T]
	
	Blocked

	[{}, {}, {16[T]}, {13[T]}, {}, {}]

Step with 12

	Trace

	19[T], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)], 11[T], 12[T]
	
	Blocked

	[{}, {}, {16[T]}, {13[T]}, {}, {}, {}]

Accelerate

Start location: l7
Program variables: i^0 j^0
  11: l0 -> l1 : j^0'=i^0, T, cost: 1
  12: l1 -> l2 : i^0'=1+i^0, T, cost: 1
  18: l2 -> l4 : T, cost: 1
  20: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0), cost: 1
  13: l3 -> l0 : 6-i^0 <= 0, cost: 1
  14: l3 -> l0 : -4+i^0 <= 0, cost: 1
  15: l3 -> l1 : i^0'=i^post5, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
  16: l4 -> l5 : 10-i^0 <= 0, cost: 1
  17: l4 -> l3 : -9+i^0 <= 0, cost: 1
  19: l7 -> l2 : i^0'=0, T, cost: 1

	Loop Acceleration

	Original rule:
	l2 -> l2 : i^0'=1+i^0, j^0'=i^0, (-9+i^0 <= 0 /\ -4+i^0 <= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0), cost: 1

		4-i^0 >= 0 [0]: montonic decrease yields 5-n-i^0 >= 0
		
		4-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 4-i^0 >= 0)
		
		9-i^0 >= 0 [0]: monotonic increase yields 9-i^0 >= 0, dependencies: 4-i^0 >= 0
		
		Replacement map: {4-i^0 >= 0 -> 5-n-i^0 >= 0, 9-i^0 >= 0 -> 9-i^0 >= 0}

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)]
	
	Blocked

	[{}, {}, {20[T]}]

Step with 18

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T]
	
	Blocked

	[{}, {}, {20[T]}, {}]

Step with 17

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}]

Step with 14

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}, {}]

Step with 11

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)], 11[T]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}, {}, {}]

Step with 12

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)], 11[T], 12[T]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}, {}, {}, {}]

Covered

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)], 11[T]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}, {}, {12[T]}]

Backtrack

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 14[(-4+i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {}, {}, {11[T]}]

Backtrack

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {}, {14[T]}]

Step with 15

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 15[(-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {}, {14[T]}, {}]

Step with 12

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 18[T], 17[(-9+i^0 <= 0)], 15[(-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0)], 12[T]
	
	Blocked

	[{}, {}, {20[T]}, {}, {14[T]}, {}, {}]

Nonterm

Start location: l7
Program variables: i^0 j^0
  11: l0 -> l1 : j^0'=i^0, T, cost: 1
  12: l1 -> l2 : i^0'=1+i^0, T, cost: 1
  18: l2 -> l4 : T, cost: 1
  20: l2 -> l2 : i^0'=n+i^0, j^0'=-1+n+i^0, (-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0), cost: 1
  21: l2 -> LoAT_sink : (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0 /\ -1-i^post51+i^0 <= 0), cost: NONTERM
  22: l2 -> l2 : i^0'=5, (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0), cost: 1
  13: l3 -> l0 : 6-i^0 <= 0, cost: 1
  14: l3 -> l0 : -4+i^0 <= 0, cost: 1
  15: l3 -> l1 : i^0'=i^post5, (-5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
  16: l4 -> l5 : 10-i^0 <= 0, cost: 1
  17: l4 -> l3 : -9+i^0 <= 0, cost: 1
  19: l7 -> l2 : i^0'=0, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l2 -> l2 : i^0'=1+i^post51, (-9+i^0 <= 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	New rule:
	l2 -> LoAT_sink : (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0 /\ -1-i^post51+i^0 <= 0), cost: NONTERM

		-5+i^0 >= 0 [0]: eventual decrease yields (-4+i^post51 >= 0 /\ -5+i^0 >= 0)
		
		-5+i^0 >= 0 [1]: eventual increase yields (-5+i^0 >= 0 /\ -1-i^post51+i^0 <= 0)
		
		5-i^0 >= 0 [0]: eventual decrease yields (4-i^post51 >= 0 /\ 5-i^0 >= 0)
		
		5-i^0 >= 0 [1]: eventual increase yields (5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0)
		
		9-i^0 >= 0 [0]: montonic decrease yields 8-i^post51 >= 0, dependencies: 5-i^0 >= 0
		
		9-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0)
		
		Replacement map: {-5+i^0 >= 0 -> (-5+i^0 >= 0 /\ -1-i^post51+i^0 <= 0), 5-i^0 >= 0 -> (5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0), 9-i^0 >= 0 -> (1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0)}

	Loop Acceleration

	Original rule:
	l2 -> l2 : i^0'=1+i^post51, (-9+i^0 <= 0 /\ -5+i^0 <= 0 /\ -5+i^0 == 0 /\ 5-i^0 <= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=1+i^post51, (-4+i^post51 >= 0 /\ 4-i^post51 >= 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ -1+n2 >= 0 /\ 8-i^post51 >= 0), cost: 1

		-5+i^0 >= 0 [0]: eventual decrease yields (-4+i^post51 >= 0 /\ -5+i^0 >= 0)
		
		-5+i^0 >= 0 [1]: eventual increase yields (-5+i^0 >= 0 /\ -1-i^post51+i^0 <= 0)
		
		5-i^0 >= 0 [0]: eventual decrease yields (4-i^post51 >= 0 /\ 5-i^0 >= 0)
		
		5-i^0 >= 0 [1]: eventual increase yields (5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0)
		
		9-i^0 >= 0 [0]: montonic decrease yields 8-i^post51 >= 0, dependencies: 5-i^0 >= 0
		
		9-i^0 >= 0 [1]: eventual increase yields (1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0)
		
		Replacement map: {-5+i^0 >= 0 -> (-4+i^post51 >= 0 /\ -5+i^0 >= 0), 5-i^0 >= 0 -> (4-i^post51 >= 0 /\ 5-i^0 >= 0), 9-i^0 >= 0 -> 8-i^post51 >= 0}

	made implied equalities explicit

	Original rule:
	l2 -> l2 : i^0'=1+i^post51, (-4+i^post51 >= 0 /\ 4-i^post51 >= 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ -1+n2 >= 0 /\ 8-i^post51 >= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=1+i^post51, (-4+i^post51 >= 0 /\ 4-i^post51 >= 0 /\ 4-i^post51 == 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0 /\ 8-i^post51 >= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l2 : i^0'=1+i^post51, (-4+i^post51 >= 0 /\ 4-i^post51 >= 0 /\ 4-i^post51 == 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0 /\ 8-i^post51 >= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=5, (0 >= 0 /\ 0 == 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0 /\ 4 >= 0), cost: 1
	
		propagated equality i^post51 = 4
		
	Simplified Guard

	Original rule:
	l2 -> l2 : i^0'=5, (0 >= 0 /\ 0 == 0 /\ -5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0 /\ 4 >= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=5, (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	l2 -> l2 : i^0'=5, (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0 /\ -1+n2 >= 0), cost: 1
	New rule:
	l2 -> l2 : i^0'=5, (-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 5-i^0 == 0), cost: 1

Step with 21

	Trace

	19[T], 20[(-1+n >= 0 /\ 5-n-i^0 >= 0 /\ 9-i^0 >= 0)], 21[(-5+i^0 >= 0 /\ 5-i^0 >= 0 /\ 1+i^post51-i^0 <= 0 /\ 9-i^0 >= 0 /\ -1-i^post51+i^0 <= 0)]
	
	Blocked

	[{}, {}, {20[T]}, {21[T]}]

Refute

	Counterexample

	[ i^0=0 j^0=0 ] 19 [ i^0=5 j^0=4 ] 20 [ i^0=i^0 j^0=0 ] 21
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b