NO

Initial ITS

Start location: l9
Program variables: i^0 k^0
   0: l0 -> l1 : i^0'=i^post1, k^0'=k^post1, (k^0-k^post1 == 0 /\ -1+i^post1-i^0 == 0), cost: 1
   4: l1 -> l2 : i^0'=i^post5, k^0'=k^post5, (-k^post5+k^0 == 0 /\ -i^post5+i^0 == 0), cost: 1
   1: l2 -> l0 : i^0'=i^post2, k^0'=k^post2, (-k^post2+k^0 == 0 /\ -i^post2+i^0 == 0), cost: 1
   2: l2 -> l0 : i^0'=i^post3, k^0'=k^post3, (-i^post3+i^0 == 0 /\ k^0-k^post3 == 0), cost: 1
   3: l2 -> l3 : i^0'=i^post4, k^0'=k^post4, (k^0-k^post4 == 0 /\ -i^post4+i^0 == 0), cost: 1
  11: l3 -> l4 : i^0'=i^post12, k^0'=k^post12, (-i^post12+i^0 == 0 /\ 1+k^0 <= 0 /\ k^0-k^post12 == 0), cost: 1
  12: l3 -> l7 : i^0'=i^post13, k^0'=k^post13, (-i^post13+i^0 == 0 /\ -k^0 <= 0 /\ k^0-k^post13 == 0), cost: 1
   5: l4 -> l5 : i^0'=i^post6, k^0'=k^post6, (k^0-k^post6 == 0 /\ -i^post6+i^0 == 0), cost: 1
   6: l6 -> l4 : i^0'=i^post7, k^0'=k^post7, (-i^post7+i^0 == 0 /\ k^0-k^post7 == 0), cost: 1
   7: l6 -> l4 : i^0'=i^post8, k^0'=k^post8, (-i^post8+i^0 == 0 /\ k^0-k^post8 == 0), cost: 1
   8: l6 -> l5 : i^0'=i^post9, k^0'=k^post9, (k^0-k^post9 == 0 /\ -i^post9+i^0 == 0), cost: 1
   9: l7 -> l4 : i^0'=i^post10, k^0'=k^post10, (-i^post10+i^0 == 0 /\ -k^post10+k^0 == 0 /\ -k^0+i^0 <= 0), cost: 1
  10: l7 -> l6 : i^0'=i^post11, k^0'=k^post11, (1+k^0-i^0 <= 0 /\ -i^post11+i^0 == 0 /\ k^0-k^post11 == 0), cost: 1
  13: l8 -> l1 : i^0'=i^post14, k^0'=k^post14, (0 == 0 /\ i^post14 == 0), cost: 1
  14: l9 -> l8 : i^0'=i^post15, k^0'=k^post15, (-k^post15+k^0 == 0 /\ -i^post15+i^0 == 0), cost: 1

Chained Linear Paths

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

	Eliminating location l8 by chaining:

	Applied chaining

	First rule:
	l9 -> l8 : i^0'=i^post15, k^0'=k^post15, (-k^post15+k^0 == 0 /\ -i^post15+i^0 == 0), cost: 1
	Second rule:
	l8 -> l1 : i^0'=i^post14, k^0'=k^post14, (0 == 0 /\ i^post14 == 0), cost: 1
	New rule:
	l9 -> l1 : i^0'=i^post14, k^0'=k^post14, (0 == 0 /\ -k^post15+k^0 == 0 /\ i^post14 == 0 /\ -i^post15+i^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 13 14

Simplified Transitions

Start location: l9
Program variables: i^0 k^0
  16: l0 -> l1 : i^0'=1+i^0, T, cost: 1
  20: l1 -> l2 : T, cost: 1
  17: l2 -> l0 : T, cost: 1
  18: l2 -> l0 : T, cost: 1
  19: l2 -> l3 : T, cost: 1
  27: l3 -> l4 : 1+k^0 <= 0, cost: 1
  28: l3 -> l7 : -k^0 <= 0, cost: 1
  21: l4 -> l5 : T, cost: 1
  22: l6 -> l4 : T, cost: 1
  23: l6 -> l4 : T, cost: 1
  24: l6 -> l5 : T, cost: 1
  25: l7 -> l4 : -k^0+i^0 <= 0, cost: 1
  26: l7 -> l6 : 1+k^0-i^0 <= 0, cost: 1
  29: l9 -> l1 : i^0'=0, k^0'=k^post14, T, cost: 1

	Propagated Equalities

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

	Original rule:
	l6 -> l5 : i^0'=i^post9, k^0'=k^post9, (k^0-k^post9 == 0 /\ -i^post9+i^0 == 0), cost: 1
	New rule:
	l6 -> l5 : i^0'=i^0, k^0'=k^0, 0 == 0, cost: 1
	
		propagated equality k^post9 = k^0
		
		propagated equality i^post9 = i^0
		
	Simplified Guard

	Original rule:
	l6 -> l5 : i^0'=i^0, k^0'=k^0, 0 == 0, cost: 1
	New rule:
	l6 -> l5 : i^0'=i^0, k^0'=k^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l5 : i^0'=i^0, k^0'=k^0, T, cost: 1
	New rule:
	l6 -> l5 : T, cost: 1
	
	Propagated Equalities

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

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

	Original rule:
	l7 -> l4 : i^0'=i^0, k^0'=k^0, -k^0+i^0 <= 0, cost: 1
	New rule:
	l7 -> l4 : -k^0+i^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l6 : i^0'=i^post11, k^0'=k^post11, (1+k^0-i^0 <= 0 /\ -i^post11+i^0 == 0 /\ k^0-k^post11 == 0), cost: 1
	New rule:
	l7 -> l6 : i^0'=i^0, k^0'=k^0, (0 == 0 /\ 1+k^0-i^0 <= 0), cost: 1
	
		propagated equality i^post11 = i^0
		
		propagated equality k^post11 = k^0
		
	Simplified Guard

	Original rule:
	l7 -> l6 : i^0'=i^0, k^0'=k^0, (0 == 0 /\ 1+k^0-i^0 <= 0), cost: 1
	New rule:
	l7 -> l6 : i^0'=i^0, k^0'=k^0, 1+k^0-i^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l6 : i^0'=i^0, k^0'=k^0, 1+k^0-i^0 <= 0, cost: 1
	New rule:
	l7 -> l6 : 1+k^0-i^0 <= 0, cost: 1
	
	Propagated Equalities

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

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

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

	Original rule:
	l3 -> l7 : i^0'=i^post13, k^0'=k^post13, (-i^post13+i^0 == 0 /\ -k^0 <= 0 /\ k^0-k^post13 == 0), cost: 1
	New rule:
	l3 -> l7 : i^0'=i^0, k^0'=k^0, (0 == 0 /\ -k^0 <= 0), cost: 1
	
		propagated equality i^post13 = i^0
		
		propagated equality k^post13 = k^0
		
	Simplified Guard

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

	Original rule:
	l3 -> l7 : i^0'=i^0, k^0'=k^0, -k^0 <= 0, cost: 1
	New rule:
	l3 -> l7 : -k^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l1 : i^0'=i^post14, k^0'=k^post14, (0 == 0 /\ -k^post15+k^0 == 0 /\ i^post14 == 0 /\ -i^post15+i^0 == 0), cost: 1
	New rule:
	l9 -> l1 : i^0'=0, k^0'=k^post14, (0 == 0 /\ -k^post15+k^0 == 0 /\ -i^post15+i^0 == 0), cost: 1
	
		propagated equality i^post14 = 0
		
	Propagated Equalities

	Original rule:
	l9 -> l1 : i^0'=0, k^0'=k^post14, (0 == 0 /\ -k^post15+k^0 == 0 /\ -i^post15+i^0 == 0), cost: 1
	New rule:
	l9 -> l1 : i^0'=0, k^0'=k^post14, 0 == 0, cost: 1
	
		propagated equality k^post15 = k^0
		
		propagated equality i^post15 = i^0
		
	Simplified Guard

	Original rule:
	l9 -> l1 : i^0'=0, k^0'=k^post14, 0 == 0, cost: 1
	New rule:
	l9 -> l1 : i^0'=0, k^0'=k^post14, T, cost: 1

Step with 29

	Trace

	29[T]
	
	Blocked

	[{}, {}]

Step with 20

	Trace

	29[T], 20[T]
	
	Blocked

	[{}, {}, {}]

Step with 19

	Trace

	29[T], 20[T], 19[T]
	
	Blocked

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

Step with 27

	Trace

	29[T], 20[T], 19[T], 27[(1+k^0 <= 0)]
	
	Blocked

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

Step with 21

	Trace

	29[T], 20[T], 19[T], 27[(1+k^0 <= 0)], 21[T]
	
	Blocked

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

Backtrack

	Trace

	29[T], 20[T], 19[T], 27[(1+k^0 <= 0)]
	
	Blocked

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

Backtrack

	Trace

	29[T], 20[T], 19[T]
	
	Blocked

	[{}, {}, {}, {27[T]}]

Step with 28

	Trace

	29[T], 20[T], 19[T], 28[(-k^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {27[T]}, {}]

Step with 25

	Trace

	29[T], 20[T], 19[T], 28[(-k^0 <= 0)], 25[(-k^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {27[T]}, {}, {}]

Step with 21

	Trace

	29[T], 20[T], 19[T], 28[(-k^0 <= 0)], 25[(-k^0+i^0 <= 0)], 21[T]
	
	Blocked

	[{}, {}, {}, {27[T]}, {}, {}, {}]

Backtrack

	Trace

	29[T], 20[T], 19[T], 28[(-k^0 <= 0)], 25[(-k^0+i^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {27[T]}, {}, {21[T]}]

Backtrack

	Trace

	29[T], 20[T], 19[T], 28[(-k^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {27[T]}, {25[T]}]

Backtrack

	Trace

	29[T], 20[T], 19[T]
	
	Blocked

	[{}, {}, {}, {27[T], 28[T]}]

Backtrack

	Trace

	29[T], 20[T]
	
	Blocked

	[{}, {}, {19[T]}]

Step with 17

	Trace

	29[T], 20[T], 17[T]
	
	Blocked

	[{}, {}, {19[T]}, {}]

Step with 16

	Trace

	29[T], 20[T], 17[T], 16[T]
	
	Blocked

	[{}, {}, {19[T]}, {}, {}]

Nonterm

Start location: l9
Program variables: i^0 k^0
  16: l0 -> l1 : i^0'=1+i^0, T, cost: 1
  20: l1 -> l2 : T, cost: 1
  30: l1 -> LoAT_sink : -1+n >= 0, cost: NONTERM
  31: l1 -> l1 : i^0'=n+i^0, -1+n >= 0, cost: 1
  17: l2 -> l0 : T, cost: 1
  18: l2 -> l0 : T, cost: 1
  19: l2 -> l3 : T, cost: 1
  27: l3 -> l4 : 1+k^0 <= 0, cost: 1
  28: l3 -> l7 : -k^0 <= 0, cost: 1
  21: l4 -> l5 : T, cost: 1
  22: l6 -> l4 : T, cost: 1
  23: l6 -> l4 : T, cost: 1
  24: l6 -> l5 : T, cost: 1
  25: l7 -> l4 : -k^0+i^0 <= 0, cost: 1
  26: l7 -> l6 : 1+k^0-i^0 <= 0, cost: 1
  29: l9 -> l1 : i^0'=0, k^0'=k^post14, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l1 -> l1 : i^0'=1+i^0, T, cost: 1
	New rule:
	l1 -> LoAT_sink : -1+n >= 0, cost: NONTERM

		Replacement map: {}

	Loop Acceleration

	Original rule:
	l1 -> l1 : i^0'=1+i^0, T, cost: 1
	New rule:
	l1 -> l1 : i^0'=n+i^0, -1+n >= 0, cost: 1

		Replacement map: {}

Step with 30

	Trace

	29[T], 30[-1+n >= 0]
	
	Blocked

	[{}, {}, {30[T]}]

Refute

	Counterexample

	[ i^0=0 k^0=0 ] 29 [ i^0=i^0 k^0=k^0 ] 30
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b