NO

Initial ITS

Start location: [1]
Program variables: tmp x xtmp y
   0: [1] -> [2] : x'=nondet, T, cost: 1
   1: [2] -> [3] : y'=nondet1, T, cost: 1
   2: [3] -> [4] : (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
  17: [3] -> [16] : (y < 0 \/ x < 0 \/ (y <= 0 /\ y >= 0)), cost: 1
   3: [4] -> [5] : tmp'=y, T, cost: 1
   4: [5] -> [6] : xtmp'=x, T, cost: 1
   5: [6] -> [8] : -y+x == 0, cost: 1
   8: [6] -> [10] : (-y+x < 0 \/ -y+x > 0), cost: 1
  14: [7] -> [14] : y'=xtmp, T, cost: 1
   6: [8] -> [9] : y'=0, T, cost: 1
   7: [9] -> [7] : T, cost: 1
   9: [10] -> [11] : xtmp-y > 0, cost: 1
  12: [10] -> [13] : xtmp-y <= 0, cost: 1
  10: [11] -> [12] : xtmp'=xtmp-y, T, cost: 1
  11: [12] -> [10] : T, cost: 1
  13: [13] -> [7] : T, cost: 1
  15: [14] -> [15] : x'=tmp, T, cost: 1
  16: [15] -> [3] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: tmp x xtmp y
  18: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
  17: [3] -> [16] : (y < 0 \/ x < 0 \/ (y <= 0 /\ y >= 0)), cost: 1
  20: [3] -> [6] : tmp'=y, xtmp'=x, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
   8: [6] -> [10] : (-y+x < 0 \/ -y+x > 0), cost: 1
  22: [6] -> [7] : y'=0, -y+x == 0, cost: 1
  24: [7] -> [3] : x'=tmp, y'=xtmp, T, cost: 1
  26: [10] -> [7] : xtmp-y <= 0, cost: 1
  27: [10] -> [10] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1

	Eliminating location [2] by chaining:

	Applied chaining

	First rule:
	[1] -> [2] : x'=nondet, T, cost: 1
	Second rule:
	[2] -> [3] : y'=nondet1, T, cost: 1
	New rule:
	[1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
	
	Applied deletion

	Removed the following rules: 0 1
	
	Eliminating location [4] by chaining:

	Applied chaining

	First rule:
	[3] -> [4] : (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
	Second rule:
	[4] -> [5] : tmp'=y, T, cost: 1
	New rule:
	[3] -> [5] : tmp'=y, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
	
	Applied deletion

	Removed the following rules: 2 3
	
	Eliminating location [5] by chaining:

	Applied chaining

	First rule:
	[3] -> [5] : tmp'=y, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
	Second rule:
	[5] -> [6] : xtmp'=x, T, cost: 1
	New rule:
	[3] -> [6] : tmp'=y, xtmp'=x, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
	
	Applied deletion

	Removed the following rules: 4 19
	
	Eliminating location [8] by chaining:

	Applied chaining

	First rule:
	[6] -> [8] : -y+x == 0, cost: 1
	Second rule:
	[8] -> [9] : y'=0, T, cost: 1
	New rule:
	[6] -> [9] : y'=0, -y+x == 0, cost: 1
	
	Applied deletion

	Removed the following rules: 5 6
	
	Eliminating location [9] by chaining:

	Applied chaining

	First rule:
	[6] -> [9] : y'=0, -y+x == 0, cost: 1
	Second rule:
	[9] -> [7] : T, cost: 1
	New rule:
	[6] -> [7] : y'=0, -y+x == 0, cost: 1
	
	Applied deletion

	Removed the following rules: 7 21
	
	Eliminating location [14] by chaining:

	Applied chaining

	First rule:
	[7] -> [14] : y'=xtmp, T, cost: 1
	Second rule:
	[14] -> [15] : x'=tmp, T, cost: 1
	New rule:
	[7] -> [15] : x'=tmp, y'=xtmp, T, cost: 1
	
	Applied deletion

	Removed the following rules: 14 15
	
	Eliminating location [15] by chaining:

	Applied chaining

	First rule:
	[7] -> [15] : x'=tmp, y'=xtmp, T, cost: 1
	Second rule:
	[15] -> [3] : T, cost: 1
	New rule:
	[7] -> [3] : x'=tmp, y'=xtmp, T, cost: 1
	
	Applied deletion

	Removed the following rules: 16 23
	
	Eliminating location [11] by chaining:

	Applied chaining

	First rule:
	[10] -> [11] : xtmp-y > 0, cost: 1
	Second rule:
	[11] -> [12] : xtmp'=xtmp-y, T, cost: 1
	New rule:
	[10] -> [12] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 9 10
	
	Eliminating location [13] by chaining:

	Applied chaining

	First rule:
	[10] -> [13] : xtmp-y <= 0, cost: 1
	Second rule:
	[13] -> [7] : T, cost: 1
	New rule:
	[10] -> [7] : xtmp-y <= 0, cost: 1
	
	Applied deletion

	Removed the following rules: 12 13
	
	Eliminating location [12] by chaining:

	Applied chaining

	First rule:
	[10] -> [12] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1
	Second rule:
	[12] -> [10] : T, cost: 1
	New rule:
	[10] -> [10] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1
	
	Applied deletion

	Removed the following rules: 11 25

Step with 18

	Trace

	18[T]
	
	Blocked

	[{}, {}]

Step with 17

	Trace

	18[T], 17[(y <= 0 /\ y >= 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {17[(y <= 0 /\ y >= 0)]}]

Step with 17

	Trace

	18[T], 17[(x < 0)]
	
	Blocked

	[{}, {17[(y <= 0 /\ y >= 0)]}, {}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {17[(y <= 0 /\ y >= 0 /\ x < 0)]}]

Step with 17

	Trace

	18[T], 17[(y < 0)]
	
	Blocked

	[{}, {17[(y <= 0 /\ y >= 0 /\ x < 0)]}, {}]

Backtrack

	Trace

	18[T]
	
	Blocked

	[{}, {17[(y < 0 /\ y <= 0 /\ y >= 0 /\ x < 0)]}]

Step with 20

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {17[T]}, {}]

Step with 8

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {}]

Step with 27

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 27[(xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {}]

Accelerate

Start location: [1]
Program variables: tmp x xtmp y
  18: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
  17: [3] -> [16] : (y < 0 \/ x < 0 \/ (y <= 0 /\ y >= 0)), cost: 1
  20: [3] -> [6] : tmp'=y, xtmp'=x, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
   8: [6] -> [10] : (-y+x < 0 \/ -y+x > 0), cost: 1
  22: [6] -> [7] : y'=0, -y+x == 0, cost: 1
  24: [7] -> [3] : x'=tmp, y'=xtmp, T, cost: 1
  26: [10] -> [7] : xtmp-y <= 0, cost: 1
  27: [10] -> [10] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1
  28: [10] -> LoAT_sink : (xtmp-y > 0 /\ y <= 0), cost: NONTERM
  29: [10] -> [10] : xtmp'=-n*y+xtmp, (xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0), cost: 1

	Certificate of Non-Termination

	Original rule:
	[10] -> [10] : xtmp'=xtmp-y, (xtmp-y > 0), cost: 1
	New rule:
	[10] -> LoAT_sink : (xtmp-y > 0 /\ y <= 0), cost: NONTERM

		xtmp-y > 0 [0]: eventual decrease yields (xtmp-(-1+n)*y-y > 0 /\ xtmp-y > 0)
		
		xtmp-y > 0 [1]: eventual increase yields (xtmp-y > 0 /\ y <= 0)
		
		Replacement map: {xtmp-y > 0 -> (xtmp-y > 0 /\ y <= 0)}

	Loop Acceleration

	Original rule:
	[10] -> [10] : xtmp'=xtmp-y, (xtmp-y > 0), cost: 1
	New rule:
	[10] -> [10] : xtmp'=-n*y+xtmp, (xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0), cost: 1

		xtmp-y > 0 [0]: eventual decrease yields (xtmp-(-1+n)*y-y > 0 /\ xtmp-y > 0)
		
		xtmp-y > 0 [1]: eventual increase yields (xtmp-y > 0 /\ y <= 0)
		
		Replacement map: {xtmp-y > 0 -> (xtmp-(-1+n)*y-y > 0 /\ xtmp-y > 0)}

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 29[T]}]

Step with 26

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}]

Step with 24

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 20

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 8

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 27

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 27[(xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 28[T]}, {}]

Covered

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}]

Step with 29

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {29[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 26

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {28[T], 29[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 24

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {28[T], 29[T]}, {}, {}]

Covered

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {28[T], 29[T]}, {24[T]}]

Backtrack

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {26[T], 28[T], 29[T]}]

Step with 27

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 27[(xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {26[T], 28[T], 29[T]}, {}]

Covered

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T]}, {26[T], 27[T], 28[T], 29[T]}]

Backtrack

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {}, {26[T], 27[T], 28[T], 29[T]}]

Backtrack

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {8[-y+x > 0]}]

Step with 22

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 24[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 22[(-y+x == 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {}, {8[T]}, {}]

Nonterm

Start location: [1]
Program variables: tmp x xtmp y
  18: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1
  17: [3] -> [16] : (y < 0 \/ x < 0 \/ (y <= 0 /\ y >= 0)), cost: 1
  20: [3] -> [6] : tmp'=y, xtmp'=x, (y >= 0 /\ x >= 0 /\ (y < 0 \/ y > 0)), cost: 1
   8: [6] -> [10] : (-y+x < 0 \/ -y+x > 0), cost: 1
  22: [6] -> [7] : y'=0, -y+x == 0, cost: 1
  24: [7] -> [3] : x'=tmp, y'=xtmp, T, cost: 1
  30: [7] -> LoAT_sink : (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0), cost: NONTERM
  31: [7] -> [7] : x'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1
  26: [10] -> [7] : xtmp-y <= 0, cost: 1
  27: [10] -> [10] : xtmp'=xtmp-y, xtmp-y > 0, cost: 1
  28: [10] -> LoAT_sink : (xtmp-y > 0 /\ y <= 0), cost: NONTERM
  29: [10] -> [10] : xtmp'=-n*y+xtmp, (xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0), cost: 1

	unrolling

	Original rule:
	[7] -> [7] : tmp'=xtmp, x'=tmp, xtmp'=tmp, y'=0, (tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp == 0), cost: 1
	New rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp == 0 /\ -tmp+xtmp == 0), cost: 1
	
	Certificate of Non-Termination

	Original rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp == 0 /\ -tmp+xtmp == 0), cost: 1
	New rule:
	[7] -> LoAT_sink : (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0), cost: NONTERM

		tmp > 0 [0]: monotonic increase yields tmp > 0
		
		tmp >= 0 [0]: monotonic increase yields tmp >= 0, dependencies: tmp > 0
		
		xtmp > 0 [0]: monotonic increase yields xtmp > 0
		
		xtmp >= 0 [0]: monotonic increase yields xtmp >= 0, dependencies: xtmp > 0
		
		tmp-xtmp >= 0 [0]: monotonic increase yields tmp-xtmp >= 0
		
		-tmp+xtmp >= 0 [0]: monotonic increase yields -tmp+xtmp >= 0
		
		Replacement map: {tmp > 0 -> tmp > 0, tmp >= 0 -> tmp >= 0, xtmp > 0 -> xtmp > 0, xtmp >= 0 -> xtmp >= 0, tmp-xtmp >= 0 -> tmp-xtmp >= 0, -tmp+xtmp >= 0 -> -tmp+xtmp >= 0}

	Loop Acceleration

	Original rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp == 0 /\ -tmp+xtmp == 0), cost: 1
	New rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0), cost: 1

		tmp > 0 [0]: monotonic increase yields tmp > 0
		
		tmp >= 0 [0]: monotonic increase yields tmp >= 0, dependencies: tmp > 0
		
		xtmp > 0 [0]: monotonic increase yields xtmp > 0
		
		xtmp >= 0 [0]: monotonic increase yields xtmp >= 0, dependencies: xtmp > 0
		
		tmp-xtmp >= 0 [0]: monotonic increase yields tmp-xtmp >= 0
		
		-tmp+xtmp >= 0 [0]: monotonic increase yields -tmp+xtmp >= 0
		
		Replacement map: {tmp > 0 -> tmp > 0, tmp >= 0 -> tmp >= 0, xtmp > 0 -> xtmp > 0, xtmp >= 0 -> xtmp >= 0, tmp-xtmp >= 0 -> tmp-xtmp >= 0, -tmp+xtmp >= 0 -> -tmp+xtmp >= 0}

	made implied equalities explicit

	Original rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0), cost: 1
	New rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1
	New rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	[7] -> [7] : tmp'=tmp, x'=xtmp, xtmp'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1
	New rule:
	[7] -> [7] : x'=xtmp, y'=0, (tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0 /\ -tmp+xtmp == 0), cost: 1

Step with 30

	Trace

	18[T], 20[(y > 0 /\ y >= 0 /\ x >= 0)], 8[(-y+x > 0)], 29[(xtmp-(-1+n)*y-y > 0 /\ -1+n >= 0 /\ xtmp-y > 0)], 26[(xtmp-y <= 0)], 30[(-1+n5 >= 0 /\ tmp > 0 /\ tmp >= 0 /\ xtmp > 0 /\ xtmp >= 0 /\ tmp-xtmp >= 0 /\ -tmp+xtmp >= 0)]
	
	Blocked

	[{}, {17[T]}, {}, {26[T]}, {27[T], 28[T], 29[T]}, {}, {30[T]}]

Refute

	Counterexample

	[ tmp=0 x=5 xtmp=0 y=1 ] 18 [ tmp=1 x=5 xtmp=5 y=1 ] 20 [ tmp=1 x=5 xtmp=5 y=1 ] 8 [ tmp=1 x=5 xtmp=1 y=1 ] 29 [ tmp=1 x=5 xtmp=1 y=1 ] 26 [ tmp=0 x=x xtmp=0 y=y ] 30
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b