WORST_CASE(Omega(0),?)

Initial ITS
Start location: l6
   0: l0 -> l1 : nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, __const_8^0'=__const_8^post0, ret_nBC211^0'=ret_nBC211^post0, res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, (-tmp7^0-res5^0+res5^post0 == 0 /\ __const_8^0-__const_8^post0 == 0 /\ -nX4^post0+nX4^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ ret_nBC211^0-ret_nBC211^post0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ -res10^post0+res10^0 == 0 /\ nX^0-nX^post0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp7^0-tmp7^post0 == 0), cost: 1
   5: l1 -> l3 : nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, __const_8^0'=__const_8^post5, ret_nBC211^0'=ret_nBC211^post5, res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, (-nX4^post5+nX4^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ res5^0-res5^post5 == 0 /\ res10^0-res10^post5 == 0 /\ ret_nBC211^0-ret_nBC211^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -nX^post5+nX^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ nI6^0-nI6^post5 == 0 /\ -ret_nBC18^post5+ret_nBC18^0 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1
   1: l2 -> l0 : nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, __const_8^0'=__const_8^post1, ret_nBC211^0'=ret_nBC211^post1, res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, (-ret_nBC211^post1+ret_nBC211^0 == 0 /\ -res5^post1+res5^0 == 0 /\ nI6^0-nI6^post1 == 0 /\ -ret_nBC18^post1+ret_nBC18^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -__const_8^post1+__const_8^0 == 0 /\ -nX4^post1+nX4^0 == 0 /\ nX9^0-nX9^post1 == 0 /\ -res10^post1+res10^0 == 0 /\ nX^0-nX^post1 == 0 /\ tmp7^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1
   2: l2 -> l0 : nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, __const_8^0'=__const_8^post2, ret_nBC211^0'=ret_nBC211^post2, res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, (-tmp___0^post2+tmp___0^0 == 0 /\ nX9^0-nX9^post2 == 0 /\ nX^0-nX^post2 == 0 /\ -res5^post2+res5^0 == 0 /\ -1+tmp7^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__const_8^post2+__const_8^0 == 0 /\ -ret_nBC18^post2+ret_nBC18^0 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -nX4^post2+nX4^0 == 0 /\ nI6^0-nI6^post2 == 0), cost: 1
   3: l3 -> l4 : nX^0'=nX^post3, nI6^0'=nI6^post3, tmp7^0'=tmp7^post3, res5^0'=res5^post3, nX9^0'=nX9^post3, tmp___0^0'=tmp___0^post3, __const_8^0'=__const_8^post3, ret_nBC211^0'=ret_nBC211^post3, res10^0'=res10^post3, nX4^0'=nX4^post3, tmp^0'=tmp^post3, ret_nBC18^0'=ret_nBC18^post3, (0 == 0 /\ tmp___0^post3-ret_nBC211^post3 == 0 /\ -nX^0+nX9^post3 == 0 /\ nX^0-nX^post3 == 0 /\ res5^0-res5^post3 == 0 /\ __const_8^0-__const_8^post3 == 0 /\ -nI6^post3+nI6^0 == 0 /\ -nX4^post3+nX4^0 == 0 /\ -nI6^0+4*__const_8^0 <= 0 /\ -nX9^post3+res10^10 == 0 /\ ret_nBC211^post3-res10^post3 == 0 /\ ret_nBC18^post3-res5^0 == 0 /\ -tmp7^post3+tmp7^0 == 0 /\ -ret_nBC18^post3+tmp^post3 == 0), cost: 1
   4: l3 -> l2 : nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, __const_8^0'=__const_8^post4, ret_nBC211^0'=ret_nBC211^post4, res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, (-nX4^post4+nX4^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -res5^post4+res5^0 == 0 /\ 1+nI6^0-4*__const_8^0 <= 0 /\ nX9^0-nX9^post4 == 0 /\ nX^0-nX^post4 == 0 /\ -__const_8^post4+__const_8^0 == 0 /\ tmp7^0-tmp7^post4 == 0 /\ nI6^0-nI6^post4 == 0 /\ res10^0-res10^post4 == 0 /\ -ret_nBC18^post4+ret_nBC18^0 == 0), cost: 1
   6: l5 -> l1 : nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, __const_8^0'=__const_8^post6, ret_nBC211^0'=ret_nBC211^post6, res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, (nX^0-nX^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -res10^post6+res10^0 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res5^post6 == 0 /\ -nX^0+nX4^post6 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ ret_nBC211^0-ret_nBC211^post6 == 0 /\ nI6^post6 == 0), cost: 1
   7: l6 -> l5 : nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, __const_8^0'=__const_8^post7, ret_nBC211^0'=ret_nBC211^post7, res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, (tmp^0-tmp^post7 == 0 /\ -nX4^post7+nX4^0 == 0 /\ nX9^0-nX9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -res5^post7+res5^0 == 0 /\ nX^0-nX^post7 == 0 /\ tmp7^0-tmp7^post7 == 0 /\ nI6^0-nI6^post7 == 0 /\ -ret_nBC18^post7+ret_nBC18^0 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ res10^0-res10^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   0: l0 -> l1 : nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, __const_8^0'=__const_8^post0, ret_nBC211^0'=ret_nBC211^post0, res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, (-tmp7^0-res5^0+res5^post0 == 0 /\ __const_8^0-__const_8^post0 == 0 /\ -nX4^post0+nX4^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ ret_nBC211^0-ret_nBC211^post0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ -res10^post0+res10^0 == 0 /\ nX^0-nX^post0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp7^0-tmp7^post0 == 0), cost: 1
   5: l1 -> l3 : nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, __const_8^0'=__const_8^post5, ret_nBC211^0'=ret_nBC211^post5, res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, (-nX4^post5+nX4^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ res5^0-res5^post5 == 0 /\ res10^0-res10^post5 == 0 /\ ret_nBC211^0-ret_nBC211^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -nX^post5+nX^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ nI6^0-nI6^post5 == 0 /\ -ret_nBC18^post5+ret_nBC18^0 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1
   1: l2 -> l0 : nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, __const_8^0'=__const_8^post1, ret_nBC211^0'=ret_nBC211^post1, res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, (-ret_nBC211^post1+ret_nBC211^0 == 0 /\ -res5^post1+res5^0 == 0 /\ nI6^0-nI6^post1 == 0 /\ -ret_nBC18^post1+ret_nBC18^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -__const_8^post1+__const_8^0 == 0 /\ -nX4^post1+nX4^0 == 0 /\ nX9^0-nX9^post1 == 0 /\ -res10^post1+res10^0 == 0 /\ nX^0-nX^post1 == 0 /\ tmp7^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1
   2: l2 -> l0 : nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, __const_8^0'=__const_8^post2, ret_nBC211^0'=ret_nBC211^post2, res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, (-tmp___0^post2+tmp___0^0 == 0 /\ nX9^0-nX9^post2 == 0 /\ nX^0-nX^post2 == 0 /\ -res5^post2+res5^0 == 0 /\ -1+tmp7^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__const_8^post2+__const_8^0 == 0 /\ -ret_nBC18^post2+ret_nBC18^0 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -nX4^post2+nX4^0 == 0 /\ nI6^0-nI6^post2 == 0), cost: 1
   4: l3 -> l2 : nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, __const_8^0'=__const_8^post4, ret_nBC211^0'=ret_nBC211^post4, res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, (-nX4^post4+nX4^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -res5^post4+res5^0 == 0 /\ 1+nI6^0-4*__const_8^0 <= 0 /\ nX9^0-nX9^post4 == 0 /\ nX^0-nX^post4 == 0 /\ -__const_8^post4+__const_8^0 == 0 /\ tmp7^0-tmp7^post4 == 0 /\ nI6^0-nI6^post4 == 0 /\ res10^0-res10^post4 == 0 /\ -ret_nBC18^post4+ret_nBC18^0 == 0), cost: 1
   6: l5 -> l1 : nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, __const_8^0'=__const_8^post6, ret_nBC211^0'=ret_nBC211^post6, res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, (nX^0-nX^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -res10^post6+res10^0 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res5^post6 == 0 /\ -nX^0+nX4^post6 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ ret_nBC211^0-ret_nBC211^post6 == 0 /\ nI6^post6 == 0), cost: 1
   7: l6 -> l5 : nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, __const_8^0'=__const_8^post7, ret_nBC211^0'=ret_nBC211^post7, res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, (tmp^0-tmp^post7 == 0 /\ -nX4^post7+nX4^0 == 0 /\ nX9^0-nX9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -res5^post7+res5^0 == 0 /\ nX^0-nX^post7 == 0 /\ tmp7^0-tmp7^post7 == 0 /\ nI6^0-nI6^post7 == 0 /\ -ret_nBC18^post7+ret_nBC18^0 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ res10^0-res10^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : nX^0'=nX^post0, nI6^0'=nI6^post0, tmp7^0'=tmp7^post0, res5^0'=res5^post0, nX9^0'=nX9^post0, tmp___0^0'=tmp___0^post0, __const_8^0'=__const_8^post0, ret_nBC211^0'=ret_nBC211^post0, res10^0'=res10^post0, nX4^0'=nX4^post0, tmp^0'=tmp^post0, ret_nBC18^0'=ret_nBC18^post0, (-tmp7^0-res5^0+res5^post0 == 0 /\ __const_8^0-__const_8^post0 == 0 /\ -nX4^post0+nX4^0 == 0 /\ -nX9^post0+nX9^0 == 0 /\ ret_nBC211^0-ret_nBC211^post0 == 0 /\ tmp___0^0-tmp___0^post0 == 0 /\ -1-nI6^0+nI6^post0 == 0 /\ -res10^post0+res10^0 == 0 /\ nX^0-nX^post0 == 0 /\ -ret_nBC18^post0+ret_nBC18^0 == 0 /\ -tmp^post0+tmp^0 == 0 /\ tmp7^0-tmp7^post0 == 0), cost: 1
New rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : nX^0'=nX^post1, nI6^0'=nI6^post1, tmp7^0'=tmp7^post1, res5^0'=res5^post1, nX9^0'=nX9^post1, tmp___0^0'=tmp___0^post1, __const_8^0'=__const_8^post1, ret_nBC211^0'=ret_nBC211^post1, res10^0'=res10^post1, nX4^0'=nX4^post1, tmp^0'=tmp^post1, ret_nBC18^0'=ret_nBC18^post1, (-ret_nBC211^post1+ret_nBC211^0 == 0 /\ -res5^post1+res5^0 == 0 /\ nI6^0-nI6^post1 == 0 /\ -ret_nBC18^post1+ret_nBC18^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -__const_8^post1+__const_8^0 == 0 /\ -nX4^post1+nX4^0 == 0 /\ nX9^0-nX9^post1 == 0 /\ -res10^post1+res10^0 == 0 /\ nX^0-nX^post1 == 0 /\ tmp7^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0), cost: 1
New rule:
l2 -> l0 : tmp7^0'=0, TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : nX^0'=nX^post2, nI6^0'=nI6^post2, tmp7^0'=tmp7^post2, res5^0'=res5^post2, nX9^0'=nX9^post2, tmp___0^0'=tmp___0^post2, __const_8^0'=__const_8^post2, ret_nBC211^0'=ret_nBC211^post2, res10^0'=res10^post2, nX4^0'=nX4^post2, tmp^0'=tmp^post2, ret_nBC18^0'=ret_nBC18^post2, (-tmp___0^post2+tmp___0^0 == 0 /\ nX9^0-nX9^post2 == 0 /\ nX^0-nX^post2 == 0 /\ -res5^post2+res5^0 == 0 /\ -1+tmp7^post2 == 0 /\ res10^0-res10^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__const_8^post2+__const_8^0 == 0 /\ -ret_nBC18^post2+ret_nBC18^0 == 0 /\ -ret_nBC211^post2+ret_nBC211^0 == 0 /\ -nX4^post2+nX4^0 == 0 /\ nI6^0-nI6^post2 == 0), cost: 1
New rule:
l2 -> l0 : tmp7^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l2 : nX^0'=nX^post4, nI6^0'=nI6^post4, tmp7^0'=tmp7^post4, res5^0'=res5^post4, nX9^0'=nX9^post4, tmp___0^0'=tmp___0^post4, __const_8^0'=__const_8^post4, ret_nBC211^0'=ret_nBC211^post4, res10^0'=res10^post4, nX4^0'=nX4^post4, tmp^0'=tmp^post4, ret_nBC18^0'=ret_nBC18^post4, (-nX4^post4+nX4^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -ret_nBC211^post4+ret_nBC211^0 == 0 /\ -res5^post4+res5^0 == 0 /\ 1+nI6^0-4*__const_8^0 <= 0 /\ nX9^0-nX9^post4 == 0 /\ nX^0-nX^post4 == 0 /\ -__const_8^post4+__const_8^0 == 0 /\ tmp7^0-tmp7^post4 == 0 /\ nI6^0-nI6^post4 == 0 /\ res10^0-res10^post4 == 0 /\ -ret_nBC18^post4+ret_nBC18^0 == 0), cost: 1
New rule:
l3 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l3 : nX^0'=nX^post5, nI6^0'=nI6^post5, tmp7^0'=tmp7^post5, res5^0'=res5^post5, nX9^0'=nX9^post5, tmp___0^0'=tmp___0^post5, __const_8^0'=__const_8^post5, ret_nBC211^0'=ret_nBC211^post5, res10^0'=res10^post5, nX4^0'=nX4^post5, tmp^0'=tmp^post5, ret_nBC18^0'=ret_nBC18^post5, (-nX4^post5+nX4^0 == 0 /\ __const_8^0-__const_8^post5 == 0 /\ res5^0-res5^post5 == 0 /\ res10^0-res10^post5 == 0 /\ ret_nBC211^0-ret_nBC211^post5 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ tmp7^0-tmp7^post5 == 0 /\ -nX^post5+nX^0 == 0 /\ -nX9^post5+nX9^0 == 0 /\ nI6^0-nI6^post5 == 0 /\ -ret_nBC18^post5+ret_nBC18^0 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1
New rule:
l1 -> l3 : TRUE, cost: 1

Applied preprocessing
Original rule:
l5 -> l1 : nX^0'=nX^post6, nI6^0'=nI6^post6, tmp7^0'=tmp7^post6, res5^0'=res5^post6, nX9^0'=nX9^post6, tmp___0^0'=tmp___0^post6, __const_8^0'=__const_8^post6, ret_nBC211^0'=ret_nBC211^post6, res10^0'=res10^post6, nX4^0'=nX4^post6, tmp^0'=tmp^post6, ret_nBC18^0'=ret_nBC18^post6, (nX^0-nX^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ -res10^post6+res10^0 == 0 /\ -nX9^post6+nX9^0 == 0 /\ -__const_8^post6+__const_8^0 == 0 /\ -tmp7^post6+tmp7^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ res5^post6 == 0 /\ -nX^0+nX4^post6 == 0 /\ -ret_nBC18^post6+ret_nBC18^0 == 0 /\ ret_nBC211^0-ret_nBC211^post6 == 0 /\ nI6^post6 == 0), cost: 1
New rule:
l5 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l6 -> l5 : nX^0'=nX^post7, nI6^0'=nI6^post7, tmp7^0'=tmp7^post7, res5^0'=res5^post7, nX9^0'=nX9^post7, tmp___0^0'=tmp___0^post7, __const_8^0'=__const_8^post7, ret_nBC211^0'=ret_nBC211^post7, res10^0'=res10^post7, nX4^0'=nX4^post7, tmp^0'=tmp^post7, ret_nBC18^0'=ret_nBC18^post7, (tmp^0-tmp^post7 == 0 /\ -nX4^post7+nX4^0 == 0 /\ nX9^0-nX9^post7 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -res5^post7+res5^0 == 0 /\ nX^0-nX^post7 == 0 /\ tmp7^0-tmp7^post7 == 0 /\ nI6^0-nI6^post7 == 0 /\ -ret_nBC18^post7+ret_nBC18^0 == 0 /\ -ret_nBC211^post7+ret_nBC211^0 == 0 /\ res10^0-res10^post7 == 0 /\ -__const_8^post7+__const_8^0 == 0), cost: 1
New rule:
l6 -> l5 : TRUE, cost: 1

Simplified rules
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  12: l1 -> l3 : TRUE, cost: 1
   9: l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
  10: l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
  11: l3 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 1
  13: l5 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 1
  14: l6 -> l5 : TRUE, cost: 1


Eliminating location l5 by chaining:

Applied chaining
First rule:
l6 -> l5 : TRUE, cost: 1
Second rule:
l5 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 1
New rule:
l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 13 14

Eliminating location l3 by chaining:

Applied chaining
First rule:
l1 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 1
New rule:
l1 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 11 12

Eliminated locations on linear paths
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  16: l1 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 2
   9: l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
  10: l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2


Eliminating location l2 by chaining:

Applied chaining
First rule:
l1 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 2
Second rule:
l2 -> l0 : tmp7^0'=0, TRUE, cost: 1
New rule:
l1 -> l0 : tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 3

Applied chaining
First rule:
l1 -> l2 : 1+nI6^0-4*__const_8^0 <= 0, cost: 2
Second rule:
l2 -> l0 : tmp7^0'=1, TRUE, cost: 1
New rule:
l1 -> l0 : tmp7^0'=1, 1+nI6^0-4*__const_8^0 <= 0, cost: 3

Applied deletion
Removed the following rules: 9 10 16

Eliminated locations on tree-shaped paths
Start location: l6
   8: l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
  17: l1 -> l0 : tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 3
  18: l1 -> l0 : tmp7^0'=1, 1+nI6^0-4*__const_8^0 <= 0, cost: 3
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l1 -> l0 : tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 3
Second rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4

Applied chaining
First rule:
l1 -> l0 : tmp7^0'=1, 1+nI6^0-4*__const_8^0 <= 0, cost: 3
Second rule:
l0 -> l1 : nI6^0'=1+nI6^0, res5^0'=tmp7^0+res5^0, TRUE, cost: 1
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 8 17 18

Eliminated locations on tree-shaped paths
Start location: l6
  19: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
  20: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2


Applied simplification
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, res5^0'=res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4

Simplified simple loops
Start location: l6
  20: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
  21: l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2


Applied acceleration
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=1, res5^0'=1+res5^0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=nI6^0+n, tmp7^0'=1, res5^0'=res5^0+n, (-nI6^0+4*__const_8^0-n >= 0 /\ -1+n >= 0), cost: 4*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jIDnDH.txt

Applied instantiation
Original rule:
l1 -> l1 : nI6^0'=nI6^0+n, tmp7^0'=1, res5^0'=res5^0+n, (-nI6^0+4*__const_8^0-n >= 0 /\ -1+n >= 0), cost: 4*n
New rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=-nI6^0+res5^0+4*__const_8^0, (0 >= 0 /\ -1-nI6^0+4*__const_8^0 >= 0), cost: -4*nI6^0+16*__const_8^0

Applied acceleration
Original rule:
l1 -> l1 : nI6^0'=1+nI6^0, tmp7^0'=0, 1+nI6^0-4*__const_8^0 <= 0, cost: 4
New rule:
l1 -> l1 : nI6^0'=nI6^0+n0, tmp7^0'=0, (-nI6^0+4*__const_8^0-n0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ncmmoP.txt

Applied instantiation
Original rule:
l1 -> l1 : nI6^0'=nI6^0+n0, tmp7^0'=0, (-nI6^0+4*__const_8^0-n0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
New rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, (0 >= 0 /\ -1-nI6^0+4*__const_8^0 >= 0), cost: -4*nI6^0+16*__const_8^0

Applied simplification
Original rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=-nI6^0+res5^0+4*__const_8^0, (0 >= 0 /\ -1-nI6^0+4*__const_8^0 >= 0), cost: -4*nI6^0+16*__const_8^0
New rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=-nI6^0+res5^0+4*__const_8^0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0

Applied simplification
Original rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, (0 >= 0 /\ -1-nI6^0+4*__const_8^0 >= 0), cost: -4*nI6^0+16*__const_8^0
New rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0

Applied deletion
Removed the following rules: 20 21

Accelerated simple loops
Start location: l6
  24: l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=-nI6^0+res5^0+4*__const_8^0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0
  25: l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2


Applied chaining
First rule:
l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2
Second rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=-nI6^0+res5^0+4*__const_8^0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0
New rule:
l6 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=4*__const_8^0, nX4^0'=nX^0, -1+__const_8^0 >= 0, cost: 2+16*__const_8^0

Applied chaining
First rule:
l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2
Second rule:
l1 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, -1-nI6^0+4*__const_8^0 >= 0, cost: -4*nI6^0+16*__const_8^0
New rule:
l6 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, res5^0'=0, nX4^0'=nX^0, -1+__const_8^0 >= 0, cost: 2+16*__const_8^0

Applied deletion
Removed the following rules: 24 25

Chained accelerated rules with incoming rules
Start location: l6
  15: l6 -> l1 : nI6^0'=0, res5^0'=0, nX4^0'=nX^0, TRUE, cost: 2
  26: l6 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=1, res5^0'=4*__const_8^0, nX4^0'=nX^0, -1+__const_8^0 >= 0, cost: 2+16*__const_8^0
  27: l6 -> l1 : nI6^0'=4*__const_8^0, tmp7^0'=0, res5^0'=0, nX4^0'=nX^0, -1+__const_8^0 >= 0, cost: 2+16*__const_8^0


Removed unreachable locations and irrelevant leafs
Start location: l6
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0