unknown

Initial ITS

Start location: l4
Program variables: tmp^0
   0: l0 -> l1 : tmp^0'=tmp^post1, -tmp^post1+tmp^0 == 0, cost: 1
   1: l2 -> l0 : tmp^0'=tmp^post2, tmp^0-tmp^post2 == 0, cost: 1
   2: l3 -> l2 : tmp^0'=tmp^post3, -tmp^post3+tmp^0 == 0, cost: 1
   3: l3 -> l0 : tmp^0'=tmp^post4, 0 == 0, cost: 1
   4: l3 -> l2 : tmp^0'=tmp^post5, tmp^0-tmp^post5 == 0, cost: 1
   5: l4 -> l3 : tmp^0'=tmp^post6, -tmp^post6+tmp^0 == 0, cost: 1

Simplified Transitions

Start location: l4
Program variables: tmp^0
   6: l0 -> l1 : T, cost: 1
   7: l2 -> l0 : T, cost: 1
   8: l3 -> l2 : T, cost: 1
   9: l3 -> l0 : tmp^0'=tmp^post4, T, cost: 1
  10: l3 -> l2 : T, cost: 1
  11: l4 -> l3 : T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : tmp^0'=tmp^post1, -tmp^post1+tmp^0 == 0, cost: 1
	New rule:
	l0 -> l1 : tmp^0'=tmp^0, 0 == 0, cost: 1
	
		propagated equality tmp^post1 = tmp^0
		
	Simplified Guard

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

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

	Original rule:
	l2 -> l0 : tmp^0'=tmp^post2, tmp^0-tmp^post2 == 0, cost: 1
	New rule:
	l2 -> l0 : tmp^0'=tmp^0, 0 == 0, cost: 1
	
		propagated equality tmp^post2 = tmp^0
		
	Simplified Guard

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

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

	Original rule:
	l3 -> l2 : tmp^0'=tmp^post3, -tmp^post3+tmp^0 == 0, cost: 1
	New rule:
	l3 -> l2 : tmp^0'=tmp^0, 0 == 0, cost: 1
	
		propagated equality tmp^post3 = tmp^0
		
	Simplified Guard

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

	Original rule:
	l3 -> l2 : tmp^0'=tmp^0, T, cost: 1
	New rule:
	l3 -> l2 : T, cost: 1
	
	Simplified Guard

	Original rule:
	l3 -> l0 : tmp^0'=tmp^post4, 0 == 0, cost: 1
	New rule:
	l3 -> l0 : tmp^0'=tmp^post4, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l2 : tmp^0'=tmp^post5, tmp^0-tmp^post5 == 0, cost: 1
	New rule:
	l3 -> l2 : tmp^0'=tmp^0, 0 == 0, cost: 1
	
		propagated equality tmp^post5 = tmp^0
		
	Simplified Guard

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

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

	Original rule:
	l4 -> l3 : tmp^0'=tmp^post6, -tmp^post6+tmp^0 == 0, cost: 1
	New rule:
	l4 -> l3 : tmp^0'=tmp^0, 0 == 0, cost: 1
	
		propagated equality tmp^post6 = tmp^0
		
	Simplified Guard

	Original rule:
	l4 -> l3 : tmp^0'=tmp^0, 0 == 0, cost: 1
	New rule:
	l4 -> l3 : tmp^0'=tmp^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l3 : tmp^0'=tmp^0, T, cost: 1
	New rule:
	l4 -> l3 : T, cost: 1

Step with 11

	Trace

	11[T]
	
	Blocked

	[{}, {}]

Step with 8

	Trace

	11[T], 8[T]
	
	Blocked

	[{}, {}, {}]

Step with 7

	Trace

	11[T], 8[T], 7[T]
	
	Blocked

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

Step with 6

	Trace

	11[T], 8[T], 7[T], 6[T]
	
	Blocked

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

Backtrack

	Trace

	11[T], 8[T], 7[T]
	
	Blocked

	[{}, {}, {}, {6[T]}]

Backtrack

	Trace

	11[T], 8[T]
	
	Blocked

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

Backtrack

	Trace

	11[T]
	
	Blocked

	[{}, {8[T]}]

Step with 9

	Trace

	11[T], 9[T]
	
	Blocked

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

Step with 6

	Trace

	11[T], 9[T], 6[T]
	
	Blocked

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

Backtrack

	Trace

	11[T], 9[T]
	
	Blocked

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

Backtrack

	Trace

	11[T]
	
	Blocked

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

Step with 10

	Trace

	11[T], 10[T]
	
	Blocked

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

Step with 7

	Trace

	11[T], 10[T], 7[T]
	
	Blocked

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

Step with 6

	Trace

	11[T], 10[T], 7[T], 6[T]
	
	Blocked

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

Backtrack

	Trace

	11[T], 10[T], 7[T]
	
	Blocked

	[{}, {8[T], 9[T]}, {}, {6[T]}]

Backtrack

	Trace

	11[T], 10[T]
	
	Blocked

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

Backtrack

	Trace

	11[T]
	
	Blocked

	[{}, {8[T], 9[T], 10[T]}]

Backtrack

	Trace

	Blocked

	[{11[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b