NO

Initial ITS
Start location: l10
   0: l0 -> l1 : k4^0'=k4^post0, ResourceIrp^0'=ResourceIrp^post0, keR^0'=keR^post0, ___rho_99_^0'=___rho_99_^post0, IsochResourceData^0'=IsochResourceData^post0, pIrb^0'=pIrb^post0, keA^0'=keA^post0, StackSize^0'=StackSize^post0, ntStatus^0'=ntStatus^post0, (IsochResourceData^0-IsochResourceData^post0 == 0 /\ -ntStatus^post0+ntStatus^0 == 0 /\ pIrb^0-pIrb^post0 == 0 /\ keR^0-keR^post0 == 0 /\ k4^0-k4^post0 == 0 /\ ResourceIrp^0-ResourceIrp^post0 == 0 /\ -StackSize^post0+StackSize^0 == 0 /\ -keA^post0+keA^0 == 0 /\ ___rho_99_^0-___rho_99_^post0 == 0), cost: 1
   1: l1 -> l0 : k4^0'=k4^post1, ResourceIrp^0'=ResourceIrp^post1, keR^0'=keR^post1, ___rho_99_^0'=___rho_99_^post1, IsochResourceData^0'=IsochResourceData^post1, pIrb^0'=pIrb^post1, keA^0'=keA^post1, StackSize^0'=StackSize^post1, ntStatus^0'=ntStatus^post1, (-ntStatus^post1+ntStatus^0 == 0 /\ -StackSize^post1+StackSize^0 == 0 /\ -keA^post1+keA^0 == 0 /\ k4^0-k4^post1 == 0 /\ keR^0-keR^post1 == 0 /\ -ResourceIrp^post1+ResourceIrp^0 == 0 /\ -pIrb^post1+pIrb^0 == 0 /\ -IsochResourceData^post1+IsochResourceData^0 == 0 /\ ___rho_99_^0-___rho_99_^post1 == 0), cost: 1
   2: l2 -> l3 : k4^0'=k4^post2, ResourceIrp^0'=ResourceIrp^post2, keR^0'=keR^post2, ___rho_99_^0'=___rho_99_^post2, IsochResourceData^0'=IsochResourceData^post2, pIrb^0'=pIrb^post2, keA^0'=keA^post2, StackSize^0'=StackSize^post2, ntStatus^0'=ntStatus^post2, (ResourceIrp^0-ResourceIrp^post2 == 0 /\ StackSize^0-StackSize^post2 == 0 /\ -ntStatus^post2+ntStatus^0 == 0 /\ ___rho_99_^0-___rho_99_^post2 == 0 /\ -pIrb^post2+pIrb^0 == 0 /\ k4^0-k4^post2 == 0 /\ keR^0-keR^post2 == 0 /\ keA^0-keA^post2 == 0 /\ -IsochResourceData^post2+IsochResourceData^0 == 0), cost: 1
  13: l3 -> l8 : k4^0'=k4^post13, ResourceIrp^0'=ResourceIrp^post13, keR^0'=keR^post13, ___rho_99_^0'=___rho_99_^post13, IsochResourceData^0'=IsochResourceData^post13, pIrb^0'=pIrb^post13, keA^0'=keA^post13, StackSize^0'=StackSize^post13, ntStatus^0'=ntStatus^post13, (-IsochResourceData^post13+IsochResourceData^0 == 0 /\ k4^0-k4^post13 == 0 /\ keA^post13 == 0 /\ keR^0-keR^post13 == 0 /\ -StackSize^post13+StackSize^0 == 0 /\ -1+keA^10 == 0 /\ ___rho_99_^0-___rho_99_^post13 == 0 /\ ResourceIrp^0-ResourceIrp^post13 == 0 /\ -ntStatus^post13+ntStatus^0 == 0 /\ -pIrb^post13+pIrb^0 == 0), cost: 1
   3: l4 -> l2 : k4^0'=k4^post3, ResourceIrp^0'=ResourceIrp^post3, keR^0'=keR^post3, ___rho_99_^0'=___rho_99_^post3, IsochResourceData^0'=IsochResourceData^post3, pIrb^0'=pIrb^post3, keA^0'=keA^post3, StackSize^0'=StackSize^post3, ntStatus^0'=ntStatus^post3, (0 == 0 /\ -StackSize^post3+StackSize^0 == 0 /\ -keA^post3+keA^0 == 0 /\ -___rho_99_^post3+___rho_99_^0 == 0 /\ IsochResourceData^0-IsochResourceData^post3 == 0 /\ k4^0-k4^post3 == 0 /\ 1-pIrb^0 <= 0 /\ -keR^post3+keR^0 == 0 /\ ResourceIrp^0-ResourceIrp^post3 == 0 /\ -pIrb^post3+pIrb^0 == 0), cost: 1
   4: l4 -> l2 : k4^0'=k4^post4, ResourceIrp^0'=ResourceIrp^post4, keR^0'=keR^post4, ___rho_99_^0'=___rho_99_^post4, IsochResourceData^0'=IsochResourceData^post4, pIrb^0'=pIrb^post4, keA^0'=keA^post4, StackSize^0'=StackSize^post4, ntStatus^0'=ntStatus^post4, (k4^0-k4^post4 == 0 /\ -keA^post4+keA^0 == 0 /\ -keR^post4+keR^0 == 0 /\ pIrb^0-pIrb^post4 == 0 /\ -___rho_99_^post4+___rho_99_^0 == 0 /\ -StackSize^post4+StackSize^0 == 0 /\ pIrb^0 <= 0 /\ -ntStatus^post4+ntStatus^0 == 0 /\ IsochResourceData^0-IsochResourceData^post4 == 0 /\ ResourceIrp^0-ResourceIrp^post4 == 0), cost: 1
   5: l5 -> l4 : k4^0'=k4^post5, ResourceIrp^0'=ResourceIrp^post5, keR^0'=keR^post5, ___rho_99_^0'=___rho_99_^post5, IsochResourceData^0'=IsochResourceData^post5, pIrb^0'=pIrb^post5, keA^0'=keA^post5, StackSize^0'=StackSize^post5, ntStatus^0'=ntStatus^post5, (0 == 0 /\ -___rho_99_^post5+___rho_99_^0 == 0 /\ -ResourceIrp^post5+ResourceIrp^0 == 0 /\ -ntStatus^post5+ntStatus^0 == 0 /\ -StackSize^post5+StackSize^0 == 0 /\ k4^0-k4^post5 == 0 /\ keR^0-keR^post5 == 0 /\ -keA^post5+keA^0 == 0 /\ IsochResourceData^0-IsochResourceData^post5 == 0), cost: 1
   6: l6 -> l5 : k4^0'=k4^post6, ResourceIrp^0'=ResourceIrp^post6, keR^0'=keR^post6, ___rho_99_^0'=___rho_99_^post6, IsochResourceData^0'=IsochResourceData^post6, pIrb^0'=pIrb^post6, keA^0'=keA^post6, StackSize^0'=StackSize^post6, ntStatus^0'=ntStatus^post6, (-pIrb^post6+pIrb^0 == 0 /\ keR^0-keR^post6 == 0 /\ -ntStatus^post6+ntStatus^0 == 0 /\ 1+ResourceIrp^0 <= 0 /\ StackSize^0-StackSize^post6 == 0 /\ ResourceIrp^0-ResourceIrp^post6 == 0 /\ ___rho_99_^0-___rho_99_^post6 == 0 /\ k4^0-k4^post6 == 0 /\ keA^0-keA^post6 == 0 /\ -IsochResourceData^post6+IsochResourceData^0 == 0), cost: 1
   7: l6 -> l5 : k4^0'=k4^post7, ResourceIrp^0'=ResourceIrp^post7, keR^0'=keR^post7, ___rho_99_^0'=___rho_99_^post7, IsochResourceData^0'=IsochResourceData^post7, pIrb^0'=pIrb^post7, keA^0'=keA^post7, StackSize^0'=StackSize^post7, ntStatus^0'=ntStatus^post7, (ResourceIrp^0-ResourceIrp^post7 == 0 /\ -keR^post7+keR^0 == 0 /\ -pIrb^post7+pIrb^0 == 0 /\ -IsochResourceData^post7+IsochResourceData^0 == 0 /\ keA^0-keA^post7 == 0 /\ -StackSize^post7+StackSize^0 == 0 /\ 1-ResourceIrp^0 <= 0 /\ -ntStatus^post7+ntStatus^0 == 0 /\ ___rho_99_^0-___rho_99_^post7 == 0 /\ -k4^post7+k4^0 == 0), cost: 1
   8: l6 -> l2 : k4^0'=k4^post8, ResourceIrp^0'=ResourceIrp^post8, keR^0'=keR^post8, ___rho_99_^0'=___rho_99_^post8, IsochResourceData^0'=IsochResourceData^post8, pIrb^0'=pIrb^post8, keA^0'=keA^post8, StackSize^0'=StackSize^post8, ntStatus^0'=ntStatus^post8, (-StackSize^post8+StackSize^0 == 0 /\ -ntStatus^post8+ntStatus^0 == 0 /\ ResourceIrp^0 <= 0 /\ ResourceIrp^0-ResourceIrp^post8 == 0 /\ IsochResourceData^0-IsochResourceData^post8 == 0 /\ keA^0-keA^post8 == 0 /\ k4^0-k4^post8 == 0 /\ -___rho_99_^post8+___rho_99_^0 == 0 /\ -ResourceIrp^0 <= 0 /\ -keR^post8+keR^0 == 0 /\ -pIrb^post8+pIrb^0 == 0), cost: 1
   9: l7 -> l2 : k4^0'=k4^post9, ResourceIrp^0'=ResourceIrp^post9, keR^0'=keR^post9, ___rho_99_^0'=___rho_99_^post9, IsochResourceData^0'=IsochResourceData^post9, pIrb^0'=pIrb^post9, keA^0'=keA^post9, StackSize^0'=StackSize^post9, ntStatus^0'=ntStatus^post9, (-ntStatus^post9+ntStatus^0 == 0 /\ -StackSize^post9+StackSize^0 == 0 /\ IsochResourceData^0-IsochResourceData^post9 == 0 /\ -keA^post9+keA^0 == 0 /\ pIrb^0-pIrb^post9 == 0 /\ keR^0-keR^post9 == 0 /\ IsochResourceData^0 <= 0 /\ -___rho_99_^post9+___rho_99_^0 == 0 /\ -ResourceIrp^post9+ResourceIrp^0 == 0 /\ k4^0-k4^post9 == 0), cost: 1
  10: l7 -> l6 : k4^0'=k4^post10, ResourceIrp^0'=ResourceIrp^post10, keR^0'=keR^post10, ___rho_99_^0'=___rho_99_^post10, IsochResourceData^0'=IsochResourceData^post10, pIrb^0'=pIrb^post10, keA^0'=keA^post10, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post10, (0 == 0 /\ -ntStatus^post10+ntStatus^0 == 0 /\ -___rho_99_^post10+ResourceIrp^post10 == 0 /\ IsochResourceData^0-IsochResourceData^post10 == 0 /\ 1-IsochResourceData^0 <= 0 /\ k4^0-k4^post10 == 0 /\ keR^0-keR^post10 == 0 /\ -keA^post10+keA^0 == 0 /\ -pIrb^post10+pIrb^0 == 0), cost: 1
  11: l8 -> l0 : k4^0'=k4^post11, ResourceIrp^0'=ResourceIrp^post11, keR^0'=keR^post11, ___rho_99_^0'=___rho_99_^post11, IsochResourceData^0'=IsochResourceData^post11, pIrb^0'=pIrb^post11, keA^0'=keA^post11, StackSize^0'=StackSize^post11, ntStatus^0'=ntStatus^post11, (ResourceIrp^0-ResourceIrp^post11 == 0 /\ k4^0 <= 0 /\ -1+keR^10 == 0 /\ -ntStatus^post11+ntStatus^0 == 0 /\ keR^post11 == 0 /\ pIrb^0-pIrb^post11 == 0 /\ k4^0-k4^post11 == 0 /\ keA^0-keA^post11 == 0 /\ -___rho_99_^post11+___rho_99_^0 == 0 /\ -StackSize^post11+StackSize^0 == 0 /\ -IsochResourceData^post11+IsochResourceData^0 == 0), cost: 1
  12: l8 -> l7 : k4^0'=k4^post12, ResourceIrp^0'=ResourceIrp^post12, keR^0'=keR^post12, ___rho_99_^0'=___rho_99_^post12, IsochResourceData^0'=IsochResourceData^post12, pIrb^0'=pIrb^post12, keA^0'=keA^post12, StackSize^0'=StackSize^post12, ntStatus^0'=ntStatus^post12, (ResourceIrp^0-ResourceIrp^post12 == 0 /\ 1-k4^0+k4^post12 == 0 /\ pIrb^0-pIrb^post12 == 0 /\ -IsochResourceData^post12+IsochResourceData^0 == 0 /\ keR^post12 == 0 /\ keA^0-keA^post12 == 0 /\ -ntStatus^post12+ntStatus^0 == 0 /\ 1-k4^0 <= 0 /\ -1+keR^11 == 0 /\ -___rho_99_^post12+___rho_99_^0 == 0 /\ -StackSize^post12+StackSize^0 == 0), cost: 1
  14: l9 -> l3 : k4^0'=k4^post14, ResourceIrp^0'=ResourceIrp^post14, keR^0'=keR^post14, ___rho_99_^0'=___rho_99_^post14, IsochResourceData^0'=IsochResourceData^post14, pIrb^0'=pIrb^post14, keA^0'=keA^post14, StackSize^0'=StackSize^post14, ntStatus^0'=ntStatus^post14, (-___rho_99_^post14+___rho_99_^0 == 0 /\ keA^post14 == 0 /\ -StackSize^post14+StackSize^0 == 0 /\ ResourceIrp^0-ResourceIrp^post14 == 0 /\ k4^0-k4^post14 == 0 /\ pIrb^0-pIrb^post14 == 0 /\ keR^post14 == 0 /\ -ntStatus^post14+ntStatus^0 == 0 /\ IsochResourceData^0-IsochResourceData^post14 == 0), cost: 1
  15: l10 -> l9 : k4^0'=k4^post15, ResourceIrp^0'=ResourceIrp^post15, keR^0'=keR^post15, ___rho_99_^0'=___rho_99_^post15, IsochResourceData^0'=IsochResourceData^post15, pIrb^0'=pIrb^post15, keA^0'=keA^post15, StackSize^0'=StackSize^post15, ntStatus^0'=ntStatus^post15, (-pIrb^post15+pIrb^0 == 0 /\ keR^0-keR^post15 == 0 /\ k4^0-k4^post15 == 0 /\ -IsochResourceData^post15+IsochResourceData^0 == 0 /\ -StackSize^post15+StackSize^0 == 0 /\ ResourceIrp^0-ResourceIrp^post15 == 0 /\ ___rho_99_^0-___rho_99_^post15 == 0 /\ -ntStatus^post15+ntStatus^0 == 0 /\ -keA^post15+keA^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : k4^0'=k4^post0, ResourceIrp^0'=ResourceIrp^post0, keR^0'=keR^post0, ___rho_99_^0'=___rho_99_^post0, IsochResourceData^0'=IsochResourceData^post0, pIrb^0'=pIrb^post0, keA^0'=keA^post0, StackSize^0'=StackSize^post0, ntStatus^0'=ntStatus^post0, (IsochResourceData^0-IsochResourceData^post0 == 0 /\ -ntStatus^post0+ntStatus^0 == 0 /\ pIrb^0-pIrb^post0 == 0 /\ keR^0-keR^post0 == 0 /\ k4^0-k4^post0 == 0 /\ ResourceIrp^0-ResourceIrp^post0 == 0 /\ -StackSize^post0+StackSize^0 == 0 /\ -keA^post0+keA^0 == 0 /\ ___rho_99_^0-___rho_99_^post0 == 0), cost: 1
New rule:
l0 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : k4^0'=k4^post1, ResourceIrp^0'=ResourceIrp^post1, keR^0'=keR^post1, ___rho_99_^0'=___rho_99_^post1, IsochResourceData^0'=IsochResourceData^post1, pIrb^0'=pIrb^post1, keA^0'=keA^post1, StackSize^0'=StackSize^post1, ntStatus^0'=ntStatus^post1, (-ntStatus^post1+ntStatus^0 == 0 /\ -StackSize^post1+StackSize^0 == 0 /\ -keA^post1+keA^0 == 0 /\ k4^0-k4^post1 == 0 /\ keR^0-keR^post1 == 0 /\ -ResourceIrp^post1+ResourceIrp^0 == 0 /\ -pIrb^post1+pIrb^0 == 0 /\ -IsochResourceData^post1+IsochResourceData^0 == 0 /\ ___rho_99_^0-___rho_99_^post1 == 0), cost: 1
New rule:
l1 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : k4^0'=k4^post2, ResourceIrp^0'=ResourceIrp^post2, keR^0'=keR^post2, ___rho_99_^0'=___rho_99_^post2, IsochResourceData^0'=IsochResourceData^post2, pIrb^0'=pIrb^post2, keA^0'=keA^post2, StackSize^0'=StackSize^post2, ntStatus^0'=ntStatus^post2, (ResourceIrp^0-ResourceIrp^post2 == 0 /\ StackSize^0-StackSize^post2 == 0 /\ -ntStatus^post2+ntStatus^0 == 0 /\ ___rho_99_^0-___rho_99_^post2 == 0 /\ -pIrb^post2+pIrb^0 == 0 /\ k4^0-k4^post2 == 0 /\ keR^0-keR^post2 == 0 /\ keA^0-keA^post2 == 0 /\ -IsochResourceData^post2+IsochResourceData^0 == 0), cost: 1
New rule:
l2 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : k4^0'=k4^post3, ResourceIrp^0'=ResourceIrp^post3, keR^0'=keR^post3, ___rho_99_^0'=___rho_99_^post3, IsochResourceData^0'=IsochResourceData^post3, pIrb^0'=pIrb^post3, keA^0'=keA^post3, StackSize^0'=StackSize^post3, ntStatus^0'=ntStatus^post3, (0 == 0 /\ -StackSize^post3+StackSize^0 == 0 /\ -keA^post3+keA^0 == 0 /\ -___rho_99_^post3+___rho_99_^0 == 0 /\ IsochResourceData^0-IsochResourceData^post3 == 0 /\ k4^0-k4^post3 == 0 /\ 1-pIrb^0 <= 0 /\ -keR^post3+keR^0 == 0 /\ ResourceIrp^0-ResourceIrp^post3 == 0 /\ -pIrb^post3+pIrb^0 == 0), cost: 1
New rule:
l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : k4^0'=k4^post4, ResourceIrp^0'=ResourceIrp^post4, keR^0'=keR^post4, ___rho_99_^0'=___rho_99_^post4, IsochResourceData^0'=IsochResourceData^post4, pIrb^0'=pIrb^post4, keA^0'=keA^post4, StackSize^0'=StackSize^post4, ntStatus^0'=ntStatus^post4, (k4^0-k4^post4 == 0 /\ -keA^post4+keA^0 == 0 /\ -keR^post4+keR^0 == 0 /\ pIrb^0-pIrb^post4 == 0 /\ -___rho_99_^post4+___rho_99_^0 == 0 /\ -StackSize^post4+StackSize^0 == 0 /\ pIrb^0 <= 0 /\ -ntStatus^post4+ntStatus^0 == 0 /\ IsochResourceData^0-IsochResourceData^post4 == 0 /\ ResourceIrp^0-ResourceIrp^post4 == 0), cost: 1
New rule:
l4 -> l2 : pIrb^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : k4^0'=k4^post5, ResourceIrp^0'=ResourceIrp^post5, keR^0'=keR^post5, ___rho_99_^0'=___rho_99_^post5, IsochResourceData^0'=IsochResourceData^post5, pIrb^0'=pIrb^post5, keA^0'=keA^post5, StackSize^0'=StackSize^post5, ntStatus^0'=ntStatus^post5, (0 == 0 /\ -___rho_99_^post5+___rho_99_^0 == 0 /\ -ResourceIrp^post5+ResourceIrp^0 == 0 /\ -ntStatus^post5+ntStatus^0 == 0 /\ -StackSize^post5+StackSize^0 == 0 /\ k4^0-k4^post5 == 0 /\ keR^0-keR^post5 == 0 /\ -keA^post5+keA^0 == 0 /\ IsochResourceData^0-IsochResourceData^post5 == 0), cost: 1
New rule:
l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : k4^0'=k4^post6, ResourceIrp^0'=ResourceIrp^post6, keR^0'=keR^post6, ___rho_99_^0'=___rho_99_^post6, IsochResourceData^0'=IsochResourceData^post6, pIrb^0'=pIrb^post6, keA^0'=keA^post6, StackSize^0'=StackSize^post6, ntStatus^0'=ntStatus^post6, (-pIrb^post6+pIrb^0 == 0 /\ keR^0-keR^post6 == 0 /\ -ntStatus^post6+ntStatus^0 == 0 /\ 1+ResourceIrp^0 <= 0 /\ StackSize^0-StackSize^post6 == 0 /\ ResourceIrp^0-ResourceIrp^post6 == 0 /\ ___rho_99_^0-___rho_99_^post6 == 0 /\ k4^0-k4^post6 == 0 /\ keA^0-keA^post6 == 0 /\ -IsochResourceData^post6+IsochResourceData^0 == 0), cost: 1
New rule:
l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : k4^0'=k4^post7, ResourceIrp^0'=ResourceIrp^post7, keR^0'=keR^post7, ___rho_99_^0'=___rho_99_^post7, IsochResourceData^0'=IsochResourceData^post7, pIrb^0'=pIrb^post7, keA^0'=keA^post7, StackSize^0'=StackSize^post7, ntStatus^0'=ntStatus^post7, (ResourceIrp^0-ResourceIrp^post7 == 0 /\ -keR^post7+keR^0 == 0 /\ -pIrb^post7+pIrb^0 == 0 /\ -IsochResourceData^post7+IsochResourceData^0 == 0 /\ keA^0-keA^post7 == 0 /\ -StackSize^post7+StackSize^0 == 0 /\ 1-ResourceIrp^0 <= 0 /\ -ntStatus^post7+ntStatus^0 == 0 /\ ___rho_99_^0-___rho_99_^post7 == 0 /\ -k4^post7+k4^0 == 0), cost: 1
New rule:
l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l2 : k4^0'=k4^post8, ResourceIrp^0'=ResourceIrp^post8, keR^0'=keR^post8, ___rho_99_^0'=___rho_99_^post8, IsochResourceData^0'=IsochResourceData^post8, pIrb^0'=pIrb^post8, keA^0'=keA^post8, StackSize^0'=StackSize^post8, ntStatus^0'=ntStatus^post8, (-StackSize^post8+StackSize^0 == 0 /\ -ntStatus^post8+ntStatus^0 == 0 /\ ResourceIrp^0 <= 0 /\ ResourceIrp^0-ResourceIrp^post8 == 0 /\ IsochResourceData^0-IsochResourceData^post8 == 0 /\ keA^0-keA^post8 == 0 /\ k4^0-k4^post8 == 0 /\ -___rho_99_^post8+___rho_99_^0 == 0 /\ -ResourceIrp^0 <= 0 /\ -keR^post8+keR^0 == 0 /\ -pIrb^post8+pIrb^0 == 0), cost: 1
New rule:
l6 -> l2 : ResourceIrp^0 == 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l2 : k4^0'=k4^post9, ResourceIrp^0'=ResourceIrp^post9, keR^0'=keR^post9, ___rho_99_^0'=___rho_99_^post9, IsochResourceData^0'=IsochResourceData^post9, pIrb^0'=pIrb^post9, keA^0'=keA^post9, StackSize^0'=StackSize^post9, ntStatus^0'=ntStatus^post9, (-ntStatus^post9+ntStatus^0 == 0 /\ -StackSize^post9+StackSize^0 == 0 /\ IsochResourceData^0-IsochResourceData^post9 == 0 /\ -keA^post9+keA^0 == 0 /\ pIrb^0-pIrb^post9 == 0 /\ keR^0-keR^post9 == 0 /\ IsochResourceData^0 <= 0 /\ -___rho_99_^post9+___rho_99_^0 == 0 /\ -ResourceIrp^post9+ResourceIrp^0 == 0 /\ k4^0-k4^post9 == 0), cost: 1
New rule:
l7 -> l2 : IsochResourceData^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l6 : k4^0'=k4^post10, ResourceIrp^0'=ResourceIrp^post10, keR^0'=keR^post10, ___rho_99_^0'=___rho_99_^post10, IsochResourceData^0'=IsochResourceData^post10, pIrb^0'=pIrb^post10, keA^0'=keA^post10, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post10, (0 == 0 /\ -ntStatus^post10+ntStatus^0 == 0 /\ -___rho_99_^post10+ResourceIrp^post10 == 0 /\ IsochResourceData^0-IsochResourceData^post10 == 0 /\ 1-IsochResourceData^0 <= 0 /\ k4^0-k4^post10 == 0 /\ keR^0-keR^post10 == 0 /\ -keA^post10+keA^0 == 0 /\ -pIrb^post10+pIrb^0 == 0), cost: 1
New rule:
l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l0 : k4^0'=k4^post11, ResourceIrp^0'=ResourceIrp^post11, keR^0'=keR^post11, ___rho_99_^0'=___rho_99_^post11, IsochResourceData^0'=IsochResourceData^post11, pIrb^0'=pIrb^post11, keA^0'=keA^post11, StackSize^0'=StackSize^post11, ntStatus^0'=ntStatus^post11, (ResourceIrp^0-ResourceIrp^post11 == 0 /\ k4^0 <= 0 /\ -1+keR^10 == 0 /\ -ntStatus^post11+ntStatus^0 == 0 /\ keR^post11 == 0 /\ pIrb^0-pIrb^post11 == 0 /\ k4^0-k4^post11 == 0 /\ keA^0-keA^post11 == 0 /\ -___rho_99_^post11+___rho_99_^0 == 0 /\ -StackSize^post11+StackSize^0 == 0 /\ -IsochResourceData^post11+IsochResourceData^0 == 0), cost: 1
New rule:
l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : k4^0'=k4^post12, ResourceIrp^0'=ResourceIrp^post12, keR^0'=keR^post12, ___rho_99_^0'=___rho_99_^post12, IsochResourceData^0'=IsochResourceData^post12, pIrb^0'=pIrb^post12, keA^0'=keA^post12, StackSize^0'=StackSize^post12, ntStatus^0'=ntStatus^post12, (ResourceIrp^0-ResourceIrp^post12 == 0 /\ 1-k4^0+k4^post12 == 0 /\ pIrb^0-pIrb^post12 == 0 /\ -IsochResourceData^post12+IsochResourceData^0 == 0 /\ keR^post12 == 0 /\ keA^0-keA^post12 == 0 /\ -ntStatus^post12+ntStatus^0 == 0 /\ 1-k4^0 <= 0 /\ -1+keR^11 == 0 /\ -___rho_99_^post12+___rho_99_^0 == 0 /\ -StackSize^post12+StackSize^0 == 0), cost: 1
New rule:
l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l8 : k4^0'=k4^post13, ResourceIrp^0'=ResourceIrp^post13, keR^0'=keR^post13, ___rho_99_^0'=___rho_99_^post13, IsochResourceData^0'=IsochResourceData^post13, pIrb^0'=pIrb^post13, keA^0'=keA^post13, StackSize^0'=StackSize^post13, ntStatus^0'=ntStatus^post13, (-IsochResourceData^post13+IsochResourceData^0 == 0 /\ k4^0-k4^post13 == 0 /\ keA^post13 == 0 /\ keR^0-keR^post13 == 0 /\ -StackSize^post13+StackSize^0 == 0 /\ -1+keA^10 == 0 /\ ___rho_99_^0-___rho_99_^post13 == 0 /\ ResourceIrp^0-ResourceIrp^post13 == 0 /\ -ntStatus^post13+ntStatus^0 == 0 /\ -pIrb^post13+pIrb^0 == 0), cost: 1
New rule:
l3 -> l8 : keA^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l9 -> l3 : k4^0'=k4^post14, ResourceIrp^0'=ResourceIrp^post14, keR^0'=keR^post14, ___rho_99_^0'=___rho_99_^post14, IsochResourceData^0'=IsochResourceData^post14, pIrb^0'=pIrb^post14, keA^0'=keA^post14, StackSize^0'=StackSize^post14, ntStatus^0'=ntStatus^post14, (-___rho_99_^post14+___rho_99_^0 == 0 /\ keA^post14 == 0 /\ -StackSize^post14+StackSize^0 == 0 /\ ResourceIrp^0-ResourceIrp^post14 == 0 /\ k4^0-k4^post14 == 0 /\ pIrb^0-pIrb^post14 == 0 /\ keR^post14 == 0 /\ -ntStatus^post14+ntStatus^0 == 0 /\ IsochResourceData^0-IsochResourceData^post14 == 0), cost: 1
New rule:
l9 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l9 : k4^0'=k4^post15, ResourceIrp^0'=ResourceIrp^post15, keR^0'=keR^post15, ___rho_99_^0'=___rho_99_^post15, IsochResourceData^0'=IsochResourceData^post15, pIrb^0'=pIrb^post15, keA^0'=keA^post15, StackSize^0'=StackSize^post15, ntStatus^0'=ntStatus^post15, (-pIrb^post15+pIrb^0 == 0 /\ keR^0-keR^post15 == 0 /\ k4^0-k4^post15 == 0 /\ -IsochResourceData^post15+IsochResourceData^0 == 0 /\ -StackSize^post15+StackSize^0 == 0 /\ ResourceIrp^0-ResourceIrp^post15 == 0 /\ ___rho_99_^0-___rho_99_^post15 == 0 /\ -ntStatus^post15+ntStatus^0 == 0 /\ -keA^post15+keA^0 == 0), cost: 1
New rule:
l10 -> l9 : TRUE, cost: 1

Simplified rules
Start location: l10
  16: l0 -> l1 : TRUE, cost: 1
  17: l1 -> l0 : TRUE, cost: 1
  18: l2 -> l3 : TRUE, cost: 1
  29: l3 -> l8 : keA^0'=0, TRUE, cost: 1
  19: l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
  20: l4 -> l2 : pIrb^0 <= 0, cost: 1
  21: l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
  22: l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
  23: l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
  24: l6 -> l2 : ResourceIrp^0 == 0, cost: 1
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  26: l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
  27: l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1
  28: l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
  30: l9 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 1
  31: l10 -> l9 : TRUE, cost: 1


Eliminating location l9 by chaining:

Applied chaining
First rule:
l10 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 1
New rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2

Applied deletion
Removed the following rules: 30 31

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : TRUE, cost: 1
Second rule:
l1 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : TRUE, cost: 2

Applied deletion
Removed the following rules: 16 17

Eliminated locations on linear paths
Start location: l10
  33: l0 -> l0 : TRUE, cost: 2
  18: l2 -> l3 : TRUE, cost: 1
  29: l3 -> l8 : keA^0'=0, TRUE, cost: 1
  19: l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
  20: l4 -> l2 : pIrb^0 <= 0, cost: 1
  21: l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
  22: l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
  23: l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
  24: l6 -> l2 : ResourceIrp^0 == 0, cost: 1
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  26: l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
  27: l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1
  28: l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied nonterm
Original rule:
l0 -> l0 : TRUE, cost: 2
New rule:
l0 -> [11] : n >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_pdhNgi.txt

Applied deletion
Removed the following rules: 33

Accelerated simple loops
Start location: l10
  34: l0 -> [11] : n >= 0, cost: NONTERM
  18: l2 -> l3 : TRUE, cost: 1
  29: l3 -> l8 : keA^0'=0, TRUE, cost: 1
  19: l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
  20: l4 -> l2 : pIrb^0 <= 0, cost: 1
  21: l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
  22: l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
  23: l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
  24: l6 -> l2 : ResourceIrp^0 == 0, cost: 1
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  26: l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
  27: l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1
  28: l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1
Second rule:
l0 -> [11] : n >= 0, cost: NONTERM
New rule:
l8 -> [11] : k4^0 <= 0, cost: NONTERM

Applied deletion
Removed the following rules: 34

Chained accelerated rules with incoming rules
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  29: l3 -> l8 : keA^0'=0, TRUE, cost: 1
  19: l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
  20: l4 -> l2 : pIrb^0 <= 0, cost: 1
  21: l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
  22: l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
  23: l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
  24: l6 -> l2 : ResourceIrp^0 == 0, cost: 1
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  26: l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
  27: l8 -> l0 : keR^0'=0, k4^0 <= 0, cost: 1
  28: l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
  35: l8 -> [11] : k4^0 <= 0, cost: NONTERM
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Removed unreachable locations and irrelevant leafs
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  29: l3 -> l8 : keA^0'=0, TRUE, cost: 1
  19: l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
  20: l4 -> l2 : pIrb^0 <= 0, cost: 1
  21: l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
  22: l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
  23: l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
  24: l6 -> l2 : ResourceIrp^0 == 0, cost: 1
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  26: l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
  28: l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
  35: l8 -> [11] : k4^0 <= 0, cost: NONTERM
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Eliminating location l8 by chaining:

Applied chaining
First rule:
l3 -> l8 : keA^0'=0, TRUE, cost: 1
Second rule:
l8 -> l7 : k4^0'=-1+k4^0, keR^0'=0, -1+k4^0 >= 0, cost: 1
New rule:
l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2

Applied chaining
First rule:
l3 -> l8 : keA^0'=0, TRUE, cost: 1
Second rule:
l8 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM

Applied deletion
Removed the following rules: 28 29 35

Eliminating location l6 by chaining:

Applied chaining
First rule:
l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
Second rule:
l6 -> l5 : 1+ResourceIrp^0 <= 0, cost: 1
New rule:
l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2

Applied chaining
First rule:
l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
Second rule:
l6 -> l5 : -1+ResourceIrp^0 >= 0, cost: 1
New rule:
l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2

Applied chaining
First rule:
l7 -> l6 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, -1+IsochResourceData^0 >= 0, cost: 1
Second rule:
l6 -> l2 : ResourceIrp^0 == 0, cost: 1
New rule:
l7 -> l2 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 22 23 24 26

Eliminating location l4 by chaining:

Applied chaining
First rule:
l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
Second rule:
l4 -> l2 : ntStatus^0'=ntStatus^post3, -1+pIrb^0 >= 0, cost: 1
New rule:
l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, (0 == 0 /\ -1+pIrb^post5 >= 0), cost: 2

Applied simplification
Original rule:
l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, (0 == 0 /\ -1+pIrb^post5 >= 0), cost: 2
New rule:
l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, -1+pIrb^post5 >= 0, cost: 2

Applied chaining
First rule:
l5 -> l4 : pIrb^0'=pIrb^post5, 0 == 0, cost: 1
Second rule:
l4 -> l2 : pIrb^0 <= 0, cost: 1
New rule:
l5 -> l2 : pIrb^0'=pIrb^post5, (0 == 0 /\ pIrb^post5 <= 0), cost: 2

Applied simplification
Original rule:
l5 -> l2 : pIrb^0'=pIrb^post5, (0 == 0 /\ pIrb^post5 <= 0), cost: 2
New rule:
l5 -> l2 : pIrb^0'=pIrb^post5, pIrb^post5 <= 0, cost: 2

Applied deletion
Removed the following rules: 19 20 21

Eliminated locations on tree-shaped paths
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  36: l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  41: l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, -1+pIrb^post5 >= 0, cost: 2
  42: l5 -> l2 : pIrb^0'=pIrb^post5, pIrb^post5 <= 0, cost: 2
  25: l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
  38: l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
  39: l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
  40: l7 -> l2 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Eliminating location l7 by chaining:

Applied chaining
First rule:
l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2
Second rule:
l7 -> l2 : IsochResourceData^0 <= 0, cost: 1
New rule:
l3 -> l2 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 3

Applied chaining
First rule:
l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2
Second rule:
l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
New rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4

Applied chaining
First rule:
l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2
Second rule:
l7 -> l5 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
New rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4

Applied chaining
First rule:
l3 -> l7 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, -1+k4^0 >= 0, cost: 2
Second rule:
l7 -> l2 : ResourceIrp^0'=ResourceIrp^post10, ___rho_99_^0'=ResourceIrp^post10, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0), cost: 2
New rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4

Applied deletion
Removed the following rules: 25 36 38 39 40

Eliminated locations on tree-shaped paths
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  43: l3 -> l2 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 3
  44: l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
  45: l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
  46: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
  41: l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, -1+pIrb^post5 >= 0, cost: 2
  42: l5 -> l2 : pIrb^0'=pIrb^post5, pIrb^post5 <= 0, cost: 2
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Eliminating location l5 by chaining:

Applied chaining
First rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
Second rule:
l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, -1+pIrb^post5 >= 0, cost: 2
New rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6

Applied chaining
First rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
Second rule:
l5 -> l2 : pIrb^0'=pIrb^post5, pIrb^post5 <= 0, cost: 2
New rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6

Applied chaining
First rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
Second rule:
l5 -> l2 : pIrb^0'=pIrb^post5, ntStatus^0'=ntStatus^post3, -1+pIrb^post5 >= 0, cost: 2
New rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+ResourceIrp^post10 >= 0 /\ -1+pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6

Applied chaining
First rule:
l3 -> l5 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
Second rule:
l5 -> l2 : pIrb^0'=pIrb^post5, pIrb^post5 <= 0, cost: 2
New rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6

Applied deletion
Removed the following rules: 41 42 44 45

Eliminated locations on tree-shaped paths
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  43: l3 -> l2 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 3
  46: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
  47: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  48: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  49: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+ResourceIrp^post10 >= 0 /\ -1+pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  50: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied pruning (of leafs and parallel rules):
Start location: l10
  18: l2 -> l3 : TRUE, cost: 1
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  43: l3 -> l2 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 3
  46: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
  47: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  48: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  50: l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l3 -> l2 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 3
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4

Applied chaining
First rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5

Applied chaining
First rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7

Applied chaining
First rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7

Applied chaining
First rule:
l3 -> l2 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 6
Second rule:
l2 -> l3 : TRUE, cost: 1
New rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7

Applied deletion
Removed the following rules: 18 43 46 47 48 50

Eliminated locations on tree-shaped paths
Start location: l10
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  51: l3 -> l3 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4
  52: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5
  53: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  54: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  55: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied simplification
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, keA^0'=0, StackSize^0'=StackSize^post10, (ResourceIrp^post10 == 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5
New rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5

Simplified simple loops
Start location: l10
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  51: l3 -> l3 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4
  53: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  54: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  55: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
  56: l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied acceleration
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4
New rule:
l3 -> l3 : k4^0'=-n0+k4^0, keR^0'=0, keA^0'=0, (-IsochResourceData^0 >= 0 /\ -n0+k4^0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_NpGHoj.txt

Applied instantiation
Original rule:
l3 -> l3 : k4^0'=-n0+k4^0, keR^0'=0, keA^0'=0, (-IsochResourceData^0 >= 0 /\ -n0+k4^0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
New rule:
l3 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (0 >= 0 /\ -IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4*k4^0

Applied acceleration
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
New rule:
l3 -> l3 : k4^0'=k4^0-n1, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -1+n1 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ k4^0-n1 >= 0), cost: 7*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_acdLlc.txt

Applied instantiation
Original rule:
l3 -> l3 : k4^0'=k4^0-n1, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -1+n1 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ k4^0-n1 >= 0), cost: 7*n1
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (0 >= 0 /\ -1+pIrb^post5 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied acceleration
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
New rule:
l3 -> l3 : k4^0'=k4^0-n2, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1-ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ k4^0-n2 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+n2 >= 0), cost: 7*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_MAgCij.txt

Applied instantiation
Original rule:
l3 -> l3 : k4^0'=k4^0-n2, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1-ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ k4^0-n2 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+n2 >= 0), cost: 7*n2
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied acceleration
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7
New rule:
l3 -> l3 : k4^0'=k4^0-n3, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ k4^0-n3 >= 0 /\ -pIrb^post5 >= 0 /\ -1+n3 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 7*n3
Sub-proof via acceration calculus written to file:///tmp/tmpnam_gpnafP.txt

Applied instantiation
Original rule:
l3 -> l3 : k4^0'=k4^0-n3, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ k4^0-n3 >= 0 /\ -pIrb^post5 >= 0 /\ -1+n3 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 7*n3
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1+ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied acceleration
Original rule:
l3 -> l3 : k4^0'=-1+k4^0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5
New rule:
l3 -> l3 : k4^0'=k4^0-n4, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+n4 >= 0 /\ k4^0-n4 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 5*n4
Sub-proof via acceration calculus written to file:///tmp/tmpnam_EnIOdF.txt

Applied instantiation
Original rule:
l3 -> l3 : k4^0'=k4^0-n4, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+n4 >= 0 /\ k4^0-n4 >= 0 /\ -1+IsochResourceData^0 >= 0), cost: 5*n4
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5*k4^0

Applied simplification
Original rule:
l3 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (0 >= 0 /\ -IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 4*k4^0
New rule:
l3 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4*k4^0

Applied simplification
Original rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (0 >= 0 /\ -1+pIrb^post5 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied simplification
Original rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1-ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied simplification
Original rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1+ResourceIrp^post10 >= 0 /\ -pIrb^post5 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0

Applied simplification
Original rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (0 >= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5*k4^0
New rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5*k4^0

Applied deletion
Removed the following rules: 51 53 54 55 56

Accelerated simple loops
Start location: l10
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  62: l3 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4*k4^0
  63: l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
  64: l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
  65: l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
  66: l3 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5*k4^0
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2


Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 4*k4^0
New rule:
l10 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 2+4*k4^0

Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0

Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0

Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 7*k4^0
New rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0

Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 5*k4^0
New rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+5*k4^0

Applied deletion
Removed the following rules: 62 63 64 65 66

Chained accelerated rules with incoming rules
Start location: l10
  37: l3 -> [11] : k4^0 <= 0, cost: NONTERM
  32: l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
  67: l10 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 2+4*k4^0
  68: l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
  69: l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
  70: l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
  71: l10 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+5*k4^0


Eliminating location l3 by chaining:

Applied chaining
First rule:
l10 -> l3 : keR^0'=0, keA^0'=0, TRUE, cost: 2
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : k4^0 <= 0, cost: NONTERM

Applied chaining
First rule:
l10 -> l3 : k4^0'=0, keR^0'=0, keA^0'=0, (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: 2+4*k4^0
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : (0 <= 0 /\ IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l10 -> [11] : (0 <= 0 /\ IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: NONTERM
New rule:
l10 -> [11] : (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, ntStatus^0'=ntStatus^post3, (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : (0 <= 0 /\ -1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l10 -> [11] : (0 <= 0 /\ -1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
New rule:
l10 -> [11] : (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : (0 <= 0 /\ 1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l10 -> [11] : (0 <= 0 /\ 1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
New rule:
l10 -> [11] : (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=ResourceIrp^post10, keR^0'=0, ___rho_99_^0'=ResourceIrp^post10, pIrb^0'=pIrb^post5, keA^0'=0, StackSize^0'=StackSize^post10, (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+7*k4^0
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : (0 <= 0 /\ -1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l10 -> [11] : (0 <= 0 /\ -1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
New rule:
l10 -> [11] : (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l10 -> l3 : k4^0'=0, ResourceIrp^0'=0, keR^0'=0, ___rho_99_^0'=0, keA^0'=0, StackSize^0'=StackSize^post10, (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: 2+5*k4^0
Second rule:
l3 -> [11] : k4^0 <= 0, cost: NONTERM
New rule:
l10 -> [11] : (0 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l10 -> [11] : (0 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
New rule:
l10 -> [11] : (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 32 37 67 68 69 70 71

Eliminated locations on tree-shaped paths
Start location: l10
  72: l10 -> [11] : k4^0 <= 0, cost: NONTERM
  73: l10 -> [11] : (IsochResourceData^0 <= 0 /\ -1+k4^0 >= 0), cost: NONTERM
  74: l10 -> [11] : (-1+pIrb^post5 >= 0 /\ 1+ResourceIrp^post10 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
  75: l10 -> [11] : (1+ResourceIrp^post10 <= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
  76: l10 -> [11] : (-1+ResourceIrp^post10 >= 0 /\ pIrb^post5 <= 0 /\ -1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM
  77: l10 -> [11] : (-1+IsochResourceData^0 >= 0 /\ -1+k4^0 >= 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 72 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  k4^0 <= 0