WORST_CASE(Omega(0),?)

Initial ITS
Start location: l7
   0: l0 -> l1 : a_243^0'=a_243^post0, prev_17^0'=prev_17^post0, length_7^0'=length_7^post0, y_80^0'=y_80^post0, _^0'=_^post0, lt_19^0'=lt_19^post0, k_296^0'=k_296^post0, y_158^0'=y_158^post0, x_23^0'=x_23^post0, elem_16^0'=elem_16^post0, a_128^0'=a_128^post0, lt_21^0'=lt_21^post0, len_48^0'=len_48^post0, y_309^0'=y_309^post0, y_14^0'=y_14^post0, Result_6^0'=Result_6^post0, i_8^0'=i_8^post0, c_15^0'=c_15^post0, x_13^0'=x_13^post0, lt_18^0'=lt_18^post0, __const_17^0'=__const_17^post0, lt_20^0'=lt_20^post0, len_246^0'=len_246^post0, y_259^0'=y_259^post0, y_110^0'=y_110^post0, head_9^0'=head_9^post0, (0 == 0 /\ y_14^10-c_15^10 == 0 /\ 1-len_48^0 <= 0 /\ elem_16^10 <= 0 /\ c_15^30-lt_21^30 == 0 /\ y_14^post0-c_15^30 == 0 /\ Result_6^post0-head_9^0 == 0 /\ 2+a_128^post0-len_48^0 == 0 /\ -len_48^0 <= 0 /\ 1-a_128^post0-_^0+a_243^post0 == 0 /\ -y_158^0+lt_21^50 == 0 /\ -y_110^post0+y_110^0 == 0 /\ -prev_17^20 <= 0 /\ y_80^0-y_80^post0 == 0 /\ elem_16^20-x_13^30 == 0 /\ -y_80^0+lt_21^10 == 0 /\ y_14^20-c_15^20 == 0 /\ -lt_21^10+c_15^20 == 0 /\ prev_17^20 <= 0 /\ prev_17^20 == 0 /\ c_15^post0-lt_21^50 == 0 /\ y_309^0-y_309^post0 == 0 /\ x_13^20 == 0 /\ i_8^0-i_8^post0 == 0 /\ -head_9^post0+head_9^0 == 0 /\ prev_17^10 <= 0 /\ prev_17^10 == 0 /\ -lt_18^post0+lt_18^0 == 0 /\ -y_158^post0+y_158^0 == 0 /\ elem_16^10-x_13^20 == 0 /\ -x_13^10+c_15^10 == 0 /\ -__const_17^post0+__const_17^0 == 0 /\ lt_20^10-lt_19^10 <= 0 /\ -y_259^post0+y_259^0 == 0 /\ k_296^0-k_296^post0 == 0 /\ elem_16^post0-x_13^post0 == 0 /\ -elem_16^10 <= 0 /\ -a_128^post0 <= 0 /\ -Result_6^post0+x_13^10 == 0 /\ prev_17^post0 == 0 /\ x_13^30-y_14^10 == 0 /\ -x_23^post0+x_23^0 == 0 /\ -1+len_246^post0 == 0 /\ lt_21^30-y_110^0 == 0 /\ _^0-_^post0 == 0 /\ length_7^0-i_8^0 <= 0 /\ -y_14^20+x_13^post0 == 0 /\ length_7^0-length_7^post0 == 0 /\ -prev_17^10 <= 0 /\ -len_48^post0+len_48^0 == 0), cost: 1
   1: l0 -> l2 : a_243^0'=a_243^post1, prev_17^0'=prev_17^post1, length_7^0'=length_7^post1, y_80^0'=y_80^post1, _^0'=_^post1, lt_19^0'=lt_19^post1, k_296^0'=k_296^post1, y_158^0'=y_158^post1, x_23^0'=x_23^post1, elem_16^0'=elem_16^post1, a_128^0'=a_128^post1, lt_21^0'=lt_21^post1, len_48^0'=len_48^post1, y_309^0'=y_309^post1, y_14^0'=y_14^post1, Result_6^0'=Result_6^post1, i_8^0'=i_8^post1, c_15^0'=c_15^post1, x_13^0'=x_13^post1, lt_18^0'=lt_18^post1, __const_17^0'=__const_17^post1, lt_20^0'=lt_20^post1, len_246^0'=len_246^post1, y_259^0'=y_259^post1, y_110^0'=y_110^post1, head_9^0'=head_9^post1, (0 == 0 /\ a_128^0-a_128^post1 == 0 /\ y_158^0-y_158^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -x_13^post1+x_13^0 == 0 /\ a_243^0-a_243^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ -len_48^0 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_23^0-x_23^post1 == 0 /\ -y_259^post1+y_259^0 == 0 /\ -y_110^post1+y_110^0 == 0 /\ _^0-_^post1 == 0 /\ -__const_17^post1+__const_17^0 == 0 /\ -len_246^post1+len_246^0 == 0 /\ Result_6^0-Result_6^post1 == 0 /\ -1+i_8^post1-i_8^0 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ k_296^0-k_296^post1 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ -lt_19^post1+lt_19^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ elem_16^0-elem_16^post1 == 0 /\ -c_15^post1+c_15^0 == 0 /\ prev_17^0-prev_17^post1 == 0 /\ -1+len_48^post1-len_48^0 == 0 /\ y_80^0-y_80^post1 == 0), cost: 1
   4: l1 -> l4 : a_243^0'=a_243^post4, prev_17^0'=prev_17^post4, length_7^0'=length_7^post4, y_80^0'=y_80^post4, _^0'=_^post4, lt_19^0'=lt_19^post4, k_296^0'=k_296^post4, y_158^0'=y_158^post4, x_23^0'=x_23^post4, elem_16^0'=elem_16^post4, a_128^0'=a_128^post4, lt_21^0'=lt_21^post4, len_48^0'=len_48^post4, y_309^0'=y_309^post4, y_14^0'=y_14^post4, Result_6^0'=Result_6^post4, i_8^0'=i_8^post4, c_15^0'=c_15^post4, x_13^0'=x_13^post4, lt_18^0'=lt_18^post4, __const_17^0'=__const_17^post4, lt_20^0'=lt_20^post4, len_246^0'=len_246^post4, y_259^0'=y_259^post4, y_110^0'=y_110^post4, head_9^0'=head_9^post4, (0 == 0 /\ prev_17^0 <= 0 /\ y_80^0-y_80^post4 == 0 /\ lt_18^0-lt_18^post4 == 0 /\ a_243^0-a_243^post4 == 0 /\ -y_14^post4+y_14^0 == 0 /\ -y_309^post4+y_309^0 == 0 /\ i_8^0-i_8^post4 == 0 /\ -y_259^post4+y_259^0 == 0 /\ -len_246^0+k_296^post4 == 0 /\ -len_246^post4+len_246^0 == 0 /\ -len_246^0 <= 0 /\ -elem_16^post4+elem_16^0 == 0 /\ -Result_6^post4+Result_6^0 == 0 /\ -y_158^post4+y_158^0 == 0 /\ len_48^0-len_48^post4 == 0 /\ _^0-_^post4 == 0 /\ -a_128^post4+a_128^0 == 0 /\ -y_14^0+x_13^post4 == 0 /\ x_23^0-x_23^post4 == 0 /\ -y_110^post4+y_110^0 == 0 /\ lt_20^110-lt_19^11 <= 0 /\ prev_17^0-prev_17^post4 == 0 /\ -a_243^0 <= 0 /\ -__const_17^post4+__const_17^0 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -head_9^post4+head_9^0 == 0 /\ -c_15^post4+c_15^0 == 0 /\ length_7^0-length_7^post4 == 0 /\ -prev_17^0 <= 0), cost: 1
   5: l1 -> l5 : a_243^0'=a_243^post5, prev_17^0'=prev_17^post5, length_7^0'=length_7^post5, y_80^0'=y_80^post5, _^0'=_^post5, lt_19^0'=lt_19^post5, k_296^0'=k_296^post5, y_158^0'=y_158^post5, x_23^0'=x_23^post5, elem_16^0'=elem_16^post5, a_128^0'=a_128^post5, lt_21^0'=lt_21^post5, len_48^0'=len_48^post5, y_309^0'=y_309^post5, y_14^0'=y_14^post5, Result_6^0'=Result_6^post5, i_8^0'=i_8^post5, c_15^0'=c_15^post5, x_13^0'=x_13^post5, lt_18^0'=lt_18^post5, __const_17^0'=__const_17^post5, lt_20^0'=lt_20^post5, len_246^0'=len_246^post5, y_259^0'=y_259^post5, y_110^0'=y_110^post5, head_9^0'=head_9^post5, (0 == 0 /\ prev_17^post5-elem_16^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ a_243^0-a_243^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ y_309^0-y_309^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ lt_18^10-y_259^0 == 0 /\ 1-len_246^0 <= 0 /\ -y_110^post5+y_110^0 == 0 /\ -head_9^post5+head_9^0 == 0 /\ -__const_17^post5+__const_17^0 == 0 /\ len_48^0-len_48^post5 == 0 /\ -len_246^0 <= 0 /\ 1-lt_20^120+lt_19^120 <= 0 /\ k_296^0-k_296^post5 == 0 /\ length_7^0-length_7^post5 == 0 /\ -_^post5+_^0 == 0 /\ -y_14^post5+y_14^0 == 0 /\ a_128^0-a_128^post5 == 0 /\ -x_13^post5+x_13^0 == 0 /\ -a_243^0 <= 0 /\ -x_23^post5+x_23^0 == 0 /\ -lt_18^10+elem_16^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -y_259^post5+y_259^0 == 0 /\ y_80^0-y_80^post5 == 0 /\ -Result_6^post5+Result_6^0 == 0), cost: 1
   2: l2 -> l0 : a_243^0'=a_243^post2, prev_17^0'=prev_17^post2, length_7^0'=length_7^post2, y_80^0'=y_80^post2, _^0'=_^post2, lt_19^0'=lt_19^post2, k_296^0'=k_296^post2, y_158^0'=y_158^post2, x_23^0'=x_23^post2, elem_16^0'=elem_16^post2, a_128^0'=a_128^post2, lt_21^0'=lt_21^post2, len_48^0'=len_48^post2, y_309^0'=y_309^post2, y_14^0'=y_14^post2, Result_6^0'=Result_6^post2, i_8^0'=i_8^post2, c_15^0'=c_15^post2, x_13^0'=x_13^post2, lt_18^0'=lt_18^post2, __const_17^0'=__const_17^post2, lt_20^0'=lt_20^post2, len_246^0'=len_246^post2, y_259^0'=y_259^post2, y_110^0'=y_110^post2, head_9^0'=head_9^post2, (-y_259^post2+y_259^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ Result_6^0-Result_6^post2 == 0 /\ __const_17^0-__const_17^post2 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_23^0-x_23^post2 == 0 /\ -len_48^post2+len_48^0 == 0 /\ _^0-_^post2 == 0 /\ y_158^0-y_158^post2 == 0 /\ k_296^0-k_296^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -c_15^post2+c_15^0 == 0 /\ y_80^0-y_80^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -len_246^post2+len_246^0 == 0 /\ prev_17^0-prev_17^post2 == 0 /\ -head_9^post2+head_9^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -a_243^post2+a_243^0 == 0 /\ -i_8^post2+i_8^0 == 0 /\ elem_16^0-elem_16^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -lt_21^post2+lt_21^0 == 0), cost: 1
   3: l3 -> l0 : a_243^0'=a_243^post3, prev_17^0'=prev_17^post3, length_7^0'=length_7^post3, y_80^0'=y_80^post3, _^0'=_^post3, lt_19^0'=lt_19^post3, k_296^0'=k_296^post3, y_158^0'=y_158^post3, x_23^0'=x_23^post3, elem_16^0'=elem_16^post3, a_128^0'=a_128^post3, lt_21^0'=lt_21^post3, len_48^0'=len_48^post3, y_309^0'=y_309^post3, y_14^0'=y_14^post3, Result_6^0'=Result_6^post3, i_8^0'=i_8^post3, c_15^0'=c_15^post3, x_13^0'=x_13^post3, lt_18^0'=lt_18^post3, __const_17^0'=__const_17^post3, lt_20^0'=lt_20^post3, len_246^0'=len_246^post3, y_259^0'=y_259^post3, y_110^0'=y_110^post3, head_9^0'=head_9^post3, (0 == 0 /\ -c_15^post3+c_15^0 == 0 /\ -Result_6^post3+Result_6^0 == 0 /\ -len_246^post3+len_246^0 == 0 /\ y_158^0-y_158^post3 == 0 /\ lt_20^0-lt_20^post3 == 0 /\ x_13^110 == 0 /\ 1-length_7^post3+i_8^10 <= 0 /\ a_243^0-a_243^post3 == 0 /\ -x_23^0+x_13^post3 == 0 /\ k_296^0-k_296^post3 == 0 /\ -1-i_8^10+i_8^post3 == 0 /\ x_23^0-x_23^post3 == 0 /\ prev_17^0-prev_17^post3 == 0 /\ -i_8^10+len_48^post3 == 0 /\ i_8^10 == 0 /\ -_^post3+_^0 == 0 /\ head_9^10 == 0 /\ -y_14^post3+y_14^0 == 0 /\ -a_128^post3+a_128^0 == 0 /\ y_80^0-y_80^post3 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ length_7^post3-__const_17^0 == 0 /\ elem_16^0-elem_16^post3 == 0 /\ -y_309^post3+y_309^0 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -y_259^post3+y_259^0 == 0 /\ -y_110^post3+y_110^0 == 0 /\ -__const_17^post3+__const_17^0 == 0), cost: 1
   6: l4 -> l6 : a_243^0'=a_243^post6, prev_17^0'=prev_17^post6, length_7^0'=length_7^post6, y_80^0'=y_80^post6, _^0'=_^post6, lt_19^0'=lt_19^post6, k_296^0'=k_296^post6, y_158^0'=y_158^post6, x_23^0'=x_23^post6, elem_16^0'=elem_16^post6, a_128^0'=a_128^post6, lt_21^0'=lt_21^post6, len_48^0'=len_48^post6, y_309^0'=y_309^post6, y_14^0'=y_14^post6, Result_6^0'=Result_6^post6, i_8^0'=i_8^post6, c_15^0'=c_15^post6, x_13^0'=x_13^post6, lt_18^0'=lt_18^post6, __const_17^0'=__const_17^post6, lt_20^0'=lt_20^post6, len_246^0'=len_246^post6, y_259^0'=y_259^post6, y_110^0'=y_110^post6, head_9^0'=head_9^post6, (0 == 0 /\ -len_48^post6+len_48^0 == 0 /\ -y_110^post6+y_110^0 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ a_243^0-a_243^post6 == 0 /\ -y_259^post6+y_259^0 == 0 /\ _^0-_^post6 == 0 /\ -elem_16^post6+elem_16^0 == 0 /\ x_23^0-x_23^post6 == 0 /\ -len_246^post6+len_246^0 == 0 /\ -head_9^post6+head_9^0 == 0 /\ -a_128^post6+a_128^0 == 0 /\ -c_15^0 <= 0 /\ -i_8^post6+i_8^0 == 0 /\ c_15^0 <= 0 /\ -k_296^0 <= 0 /\ y_309^0-y_309^post6 == 0 /\ lt_19^0-lt_19^post6 == 0 /\ -__const_17^post6+__const_17^0 == 0 /\ -lt_20^post6+lt_20^0 == 0 /\ k_296^0-k_296^post6 == 0 /\ lt_18^0-lt_18^post6 == 0 /\ -prev_17^post6+prev_17^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ -a_243^0 <= 0 /\ -c_15^post6+c_15^0 == 0 /\ length_7^0-length_7^post6 == 0 /\ y_158^0-y_158^post6 == 0 /\ y_80^0-y_80^post6 == 0 /\ x_13^0-x_13^post6 == 0), cost: 1
   7: l4 -> l1 : a_243^0'=a_243^post7, prev_17^0'=prev_17^post7, length_7^0'=length_7^post7, y_80^0'=y_80^post7, _^0'=_^post7, lt_19^0'=lt_19^post7, k_296^0'=k_296^post7, y_158^0'=y_158^post7, x_23^0'=x_23^post7, elem_16^0'=elem_16^post7, a_128^0'=a_128^post7, lt_21^0'=lt_21^post7, len_48^0'=len_48^post7, y_309^0'=y_309^post7, y_14^0'=y_14^post7, Result_6^0'=Result_6^post7, i_8^0'=i_8^post7, c_15^0'=c_15^post7, x_13^0'=x_13^post7, lt_18^0'=lt_18^post7, __const_17^0'=__const_17^post7, lt_20^0'=lt_20^post7, len_246^0'=len_246^post7, y_259^0'=y_259^post7, y_110^0'=y_110^post7, head_9^0'=head_9^post7, (0 == 0 /\ -1-k_296^0+len_246^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ prev_17^post7 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ y_158^0-y_158^post7 == 0 /\ y_80^0-y_80^post7 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -y_110^post7+y_110^0 == 0 /\ elem_16^post7-x_13^0 == 0 /\ _^0-_^post7 == 0 /\ y_14^post7-c_15^0 == 0 /\ x_23^0-x_23^post7 == 0 /\ -len_48^post7+len_48^0 == 0 /\ Result_6^0-Result_6^post7 == 0 /\ lt_21^11-y_309^0 == 0 /\ 1-a_243^0+a_243^post7 == 0 /\ k_296^0-k_296^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ length_7^0-length_7^post7 == 0 /\ a_128^0-a_128^post7 == 0 /\ -k_296^0 <= 0 /\ -lt_21^11+c_15^post7 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_309^0-y_309^post7 == 0 /\ -__const_17^post7+__const_17^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ -a_243^0 <= 0 /\ -x_13^post7+x_13^0 == 0), cost: 1
   8: l7 -> l3 : a_243^0'=a_243^post8, prev_17^0'=prev_17^post8, length_7^0'=length_7^post8, y_80^0'=y_80^post8, _^0'=_^post8, lt_19^0'=lt_19^post8, k_296^0'=k_296^post8, y_158^0'=y_158^post8, x_23^0'=x_23^post8, elem_16^0'=elem_16^post8, a_128^0'=a_128^post8, lt_21^0'=lt_21^post8, len_48^0'=len_48^post8, y_309^0'=y_309^post8, y_14^0'=y_14^post8, Result_6^0'=Result_6^post8, i_8^0'=i_8^post8, c_15^0'=c_15^post8, x_13^0'=x_13^post8, lt_18^0'=lt_18^post8, __const_17^0'=__const_17^post8, lt_20^0'=lt_20^post8, len_246^0'=len_246^post8, y_259^0'=y_259^post8, y_110^0'=y_110^post8, head_9^0'=head_9^post8, (elem_16^0-elem_16^post8 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ lt_19^0-lt_19^post8 == 0 /\ y_309^0-y_309^post8 == 0 /\ k_296^0-k_296^post8 == 0 /\ -__const_17^post8+__const_17^0 == 0 /\ a_243^0-a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ y_158^0-y_158^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ c_15^0-c_15^post8 == 0 /\ len_48^0-len_48^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ prev_17^0-prev_17^post8 == 0 /\ a_128^0-a_128^post8 == 0 /\ -y_14^post8+y_14^0 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -Result_6^post8+Result_6^0 == 0 /\ -len_246^post8+len_246^0 == 0 /\ y_259^0-y_259^post8 == 0 /\ _^0-_^post8 == 0 /\ -x_23^post8+x_23^0 == 0 /\ -lt_18^post8+lt_18^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l7
   0: l0 -> l1 : a_243^0'=a_243^post0, prev_17^0'=prev_17^post0, length_7^0'=length_7^post0, y_80^0'=y_80^post0, _^0'=_^post0, lt_19^0'=lt_19^post0, k_296^0'=k_296^post0, y_158^0'=y_158^post0, x_23^0'=x_23^post0, elem_16^0'=elem_16^post0, a_128^0'=a_128^post0, lt_21^0'=lt_21^post0, len_48^0'=len_48^post0, y_309^0'=y_309^post0, y_14^0'=y_14^post0, Result_6^0'=Result_6^post0, i_8^0'=i_8^post0, c_15^0'=c_15^post0, x_13^0'=x_13^post0, lt_18^0'=lt_18^post0, __const_17^0'=__const_17^post0, lt_20^0'=lt_20^post0, len_246^0'=len_246^post0, y_259^0'=y_259^post0, y_110^0'=y_110^post0, head_9^0'=head_9^post0, (0 == 0 /\ y_14^10-c_15^10 == 0 /\ 1-len_48^0 <= 0 /\ elem_16^10 <= 0 /\ c_15^30-lt_21^30 == 0 /\ y_14^post0-c_15^30 == 0 /\ Result_6^post0-head_9^0 == 0 /\ 2+a_128^post0-len_48^0 == 0 /\ -len_48^0 <= 0 /\ 1-a_128^post0-_^0+a_243^post0 == 0 /\ -y_158^0+lt_21^50 == 0 /\ -y_110^post0+y_110^0 == 0 /\ -prev_17^20 <= 0 /\ y_80^0-y_80^post0 == 0 /\ elem_16^20-x_13^30 == 0 /\ -y_80^0+lt_21^10 == 0 /\ y_14^20-c_15^20 == 0 /\ -lt_21^10+c_15^20 == 0 /\ prev_17^20 <= 0 /\ prev_17^20 == 0 /\ c_15^post0-lt_21^50 == 0 /\ y_309^0-y_309^post0 == 0 /\ x_13^20 == 0 /\ i_8^0-i_8^post0 == 0 /\ -head_9^post0+head_9^0 == 0 /\ prev_17^10 <= 0 /\ prev_17^10 == 0 /\ -lt_18^post0+lt_18^0 == 0 /\ -y_158^post0+y_158^0 == 0 /\ elem_16^10-x_13^20 == 0 /\ -x_13^10+c_15^10 == 0 /\ -__const_17^post0+__const_17^0 == 0 /\ lt_20^10-lt_19^10 <= 0 /\ -y_259^post0+y_259^0 == 0 /\ k_296^0-k_296^post0 == 0 /\ elem_16^post0-x_13^post0 == 0 /\ -elem_16^10 <= 0 /\ -a_128^post0 <= 0 /\ -Result_6^post0+x_13^10 == 0 /\ prev_17^post0 == 0 /\ x_13^30-y_14^10 == 0 /\ -x_23^post0+x_23^0 == 0 /\ -1+len_246^post0 == 0 /\ lt_21^30-y_110^0 == 0 /\ _^0-_^post0 == 0 /\ length_7^0-i_8^0 <= 0 /\ -y_14^20+x_13^post0 == 0 /\ length_7^0-length_7^post0 == 0 /\ -prev_17^10 <= 0 /\ -len_48^post0+len_48^0 == 0), cost: 1
   1: l0 -> l2 : a_243^0'=a_243^post1, prev_17^0'=prev_17^post1, length_7^0'=length_7^post1, y_80^0'=y_80^post1, _^0'=_^post1, lt_19^0'=lt_19^post1, k_296^0'=k_296^post1, y_158^0'=y_158^post1, x_23^0'=x_23^post1, elem_16^0'=elem_16^post1, a_128^0'=a_128^post1, lt_21^0'=lt_21^post1, len_48^0'=len_48^post1, y_309^0'=y_309^post1, y_14^0'=y_14^post1, Result_6^0'=Result_6^post1, i_8^0'=i_8^post1, c_15^0'=c_15^post1, x_13^0'=x_13^post1, lt_18^0'=lt_18^post1, __const_17^0'=__const_17^post1, lt_20^0'=lt_20^post1, len_246^0'=len_246^post1, y_259^0'=y_259^post1, y_110^0'=y_110^post1, head_9^0'=head_9^post1, (0 == 0 /\ a_128^0-a_128^post1 == 0 /\ y_158^0-y_158^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -x_13^post1+x_13^0 == 0 /\ a_243^0-a_243^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ -len_48^0 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_23^0-x_23^post1 == 0 /\ -y_259^post1+y_259^0 == 0 /\ -y_110^post1+y_110^0 == 0 /\ _^0-_^post1 == 0 /\ -__const_17^post1+__const_17^0 == 0 /\ -len_246^post1+len_246^0 == 0 /\ Result_6^0-Result_6^post1 == 0 /\ -1+i_8^post1-i_8^0 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ k_296^0-k_296^post1 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ -lt_19^post1+lt_19^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ elem_16^0-elem_16^post1 == 0 /\ -c_15^post1+c_15^0 == 0 /\ prev_17^0-prev_17^post1 == 0 /\ -1+len_48^post1-len_48^0 == 0 /\ y_80^0-y_80^post1 == 0), cost: 1
   4: l1 -> l4 : a_243^0'=a_243^post4, prev_17^0'=prev_17^post4, length_7^0'=length_7^post4, y_80^0'=y_80^post4, _^0'=_^post4, lt_19^0'=lt_19^post4, k_296^0'=k_296^post4, y_158^0'=y_158^post4, x_23^0'=x_23^post4, elem_16^0'=elem_16^post4, a_128^0'=a_128^post4, lt_21^0'=lt_21^post4, len_48^0'=len_48^post4, y_309^0'=y_309^post4, y_14^0'=y_14^post4, Result_6^0'=Result_6^post4, i_8^0'=i_8^post4, c_15^0'=c_15^post4, x_13^0'=x_13^post4, lt_18^0'=lt_18^post4, __const_17^0'=__const_17^post4, lt_20^0'=lt_20^post4, len_246^0'=len_246^post4, y_259^0'=y_259^post4, y_110^0'=y_110^post4, head_9^0'=head_9^post4, (0 == 0 /\ prev_17^0 <= 0 /\ y_80^0-y_80^post4 == 0 /\ lt_18^0-lt_18^post4 == 0 /\ a_243^0-a_243^post4 == 0 /\ -y_14^post4+y_14^0 == 0 /\ -y_309^post4+y_309^0 == 0 /\ i_8^0-i_8^post4 == 0 /\ -y_259^post4+y_259^0 == 0 /\ -len_246^0+k_296^post4 == 0 /\ -len_246^post4+len_246^0 == 0 /\ -len_246^0 <= 0 /\ -elem_16^post4+elem_16^0 == 0 /\ -Result_6^post4+Result_6^0 == 0 /\ -y_158^post4+y_158^0 == 0 /\ len_48^0-len_48^post4 == 0 /\ _^0-_^post4 == 0 /\ -a_128^post4+a_128^0 == 0 /\ -y_14^0+x_13^post4 == 0 /\ x_23^0-x_23^post4 == 0 /\ -y_110^post4+y_110^0 == 0 /\ lt_20^110-lt_19^11 <= 0 /\ prev_17^0-prev_17^post4 == 0 /\ -a_243^0 <= 0 /\ -__const_17^post4+__const_17^0 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -head_9^post4+head_9^0 == 0 /\ -c_15^post4+c_15^0 == 0 /\ length_7^0-length_7^post4 == 0 /\ -prev_17^0 <= 0), cost: 1
   2: l2 -> l0 : a_243^0'=a_243^post2, prev_17^0'=prev_17^post2, length_7^0'=length_7^post2, y_80^0'=y_80^post2, _^0'=_^post2, lt_19^0'=lt_19^post2, k_296^0'=k_296^post2, y_158^0'=y_158^post2, x_23^0'=x_23^post2, elem_16^0'=elem_16^post2, a_128^0'=a_128^post2, lt_21^0'=lt_21^post2, len_48^0'=len_48^post2, y_309^0'=y_309^post2, y_14^0'=y_14^post2, Result_6^0'=Result_6^post2, i_8^0'=i_8^post2, c_15^0'=c_15^post2, x_13^0'=x_13^post2, lt_18^0'=lt_18^post2, __const_17^0'=__const_17^post2, lt_20^0'=lt_20^post2, len_246^0'=len_246^post2, y_259^0'=y_259^post2, y_110^0'=y_110^post2, head_9^0'=head_9^post2, (-y_259^post2+y_259^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ Result_6^0-Result_6^post2 == 0 /\ __const_17^0-__const_17^post2 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_23^0-x_23^post2 == 0 /\ -len_48^post2+len_48^0 == 0 /\ _^0-_^post2 == 0 /\ y_158^0-y_158^post2 == 0 /\ k_296^0-k_296^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -c_15^post2+c_15^0 == 0 /\ y_80^0-y_80^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -len_246^post2+len_246^0 == 0 /\ prev_17^0-prev_17^post2 == 0 /\ -head_9^post2+head_9^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -a_243^post2+a_243^0 == 0 /\ -i_8^post2+i_8^0 == 0 /\ elem_16^0-elem_16^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -lt_21^post2+lt_21^0 == 0), cost: 1
   3: l3 -> l0 : a_243^0'=a_243^post3, prev_17^0'=prev_17^post3, length_7^0'=length_7^post3, y_80^0'=y_80^post3, _^0'=_^post3, lt_19^0'=lt_19^post3, k_296^0'=k_296^post3, y_158^0'=y_158^post3, x_23^0'=x_23^post3, elem_16^0'=elem_16^post3, a_128^0'=a_128^post3, lt_21^0'=lt_21^post3, len_48^0'=len_48^post3, y_309^0'=y_309^post3, y_14^0'=y_14^post3, Result_6^0'=Result_6^post3, i_8^0'=i_8^post3, c_15^0'=c_15^post3, x_13^0'=x_13^post3, lt_18^0'=lt_18^post3, __const_17^0'=__const_17^post3, lt_20^0'=lt_20^post3, len_246^0'=len_246^post3, y_259^0'=y_259^post3, y_110^0'=y_110^post3, head_9^0'=head_9^post3, (0 == 0 /\ -c_15^post3+c_15^0 == 0 /\ -Result_6^post3+Result_6^0 == 0 /\ -len_246^post3+len_246^0 == 0 /\ y_158^0-y_158^post3 == 0 /\ lt_20^0-lt_20^post3 == 0 /\ x_13^110 == 0 /\ 1-length_7^post3+i_8^10 <= 0 /\ a_243^0-a_243^post3 == 0 /\ -x_23^0+x_13^post3 == 0 /\ k_296^0-k_296^post3 == 0 /\ -1-i_8^10+i_8^post3 == 0 /\ x_23^0-x_23^post3 == 0 /\ prev_17^0-prev_17^post3 == 0 /\ -i_8^10+len_48^post3 == 0 /\ i_8^10 == 0 /\ -_^post3+_^0 == 0 /\ head_9^10 == 0 /\ -y_14^post3+y_14^0 == 0 /\ -a_128^post3+a_128^0 == 0 /\ y_80^0-y_80^post3 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ length_7^post3-__const_17^0 == 0 /\ elem_16^0-elem_16^post3 == 0 /\ -y_309^post3+y_309^0 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -y_259^post3+y_259^0 == 0 /\ -y_110^post3+y_110^0 == 0 /\ -__const_17^post3+__const_17^0 == 0), cost: 1
   7: l4 -> l1 : a_243^0'=a_243^post7, prev_17^0'=prev_17^post7, length_7^0'=length_7^post7, y_80^0'=y_80^post7, _^0'=_^post7, lt_19^0'=lt_19^post7, k_296^0'=k_296^post7, y_158^0'=y_158^post7, x_23^0'=x_23^post7, elem_16^0'=elem_16^post7, a_128^0'=a_128^post7, lt_21^0'=lt_21^post7, len_48^0'=len_48^post7, y_309^0'=y_309^post7, y_14^0'=y_14^post7, Result_6^0'=Result_6^post7, i_8^0'=i_8^post7, c_15^0'=c_15^post7, x_13^0'=x_13^post7, lt_18^0'=lt_18^post7, __const_17^0'=__const_17^post7, lt_20^0'=lt_20^post7, len_246^0'=len_246^post7, y_259^0'=y_259^post7, y_110^0'=y_110^post7, head_9^0'=head_9^post7, (0 == 0 /\ -1-k_296^0+len_246^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ prev_17^post7 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ y_158^0-y_158^post7 == 0 /\ y_80^0-y_80^post7 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -y_110^post7+y_110^0 == 0 /\ elem_16^post7-x_13^0 == 0 /\ _^0-_^post7 == 0 /\ y_14^post7-c_15^0 == 0 /\ x_23^0-x_23^post7 == 0 /\ -len_48^post7+len_48^0 == 0 /\ Result_6^0-Result_6^post7 == 0 /\ lt_21^11-y_309^0 == 0 /\ 1-a_243^0+a_243^post7 == 0 /\ k_296^0-k_296^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ length_7^0-length_7^post7 == 0 /\ a_128^0-a_128^post7 == 0 /\ -k_296^0 <= 0 /\ -lt_21^11+c_15^post7 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_309^0-y_309^post7 == 0 /\ -__const_17^post7+__const_17^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ -a_243^0 <= 0 /\ -x_13^post7+x_13^0 == 0), cost: 1
   8: l7 -> l3 : a_243^0'=a_243^post8, prev_17^0'=prev_17^post8, length_7^0'=length_7^post8, y_80^0'=y_80^post8, _^0'=_^post8, lt_19^0'=lt_19^post8, k_296^0'=k_296^post8, y_158^0'=y_158^post8, x_23^0'=x_23^post8, elem_16^0'=elem_16^post8, a_128^0'=a_128^post8, lt_21^0'=lt_21^post8, len_48^0'=len_48^post8, y_309^0'=y_309^post8, y_14^0'=y_14^post8, Result_6^0'=Result_6^post8, i_8^0'=i_8^post8, c_15^0'=c_15^post8, x_13^0'=x_13^post8, lt_18^0'=lt_18^post8, __const_17^0'=__const_17^post8, lt_20^0'=lt_20^post8, len_246^0'=len_246^post8, y_259^0'=y_259^post8, y_110^0'=y_110^post8, head_9^0'=head_9^post8, (elem_16^0-elem_16^post8 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ lt_19^0-lt_19^post8 == 0 /\ y_309^0-y_309^post8 == 0 /\ k_296^0-k_296^post8 == 0 /\ -__const_17^post8+__const_17^0 == 0 /\ a_243^0-a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ y_158^0-y_158^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ c_15^0-c_15^post8 == 0 /\ len_48^0-len_48^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ prev_17^0-prev_17^post8 == 0 /\ a_128^0-a_128^post8 == 0 /\ -y_14^post8+y_14^0 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -Result_6^post8+Result_6^0 == 0 /\ -len_246^post8+len_246^0 == 0 /\ y_259^0-y_259^post8 == 0 /\ _^0-_^post8 == 0 /\ -x_23^post8+x_23^0 == 0 /\ -lt_18^post8+lt_18^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : a_243^0'=a_243^post0, prev_17^0'=prev_17^post0, length_7^0'=length_7^post0, y_80^0'=y_80^post0, _^0'=_^post0, lt_19^0'=lt_19^post0, k_296^0'=k_296^post0, y_158^0'=y_158^post0, x_23^0'=x_23^post0, elem_16^0'=elem_16^post0, a_128^0'=a_128^post0, lt_21^0'=lt_21^post0, len_48^0'=len_48^post0, y_309^0'=y_309^post0, y_14^0'=y_14^post0, Result_6^0'=Result_6^post0, i_8^0'=i_8^post0, c_15^0'=c_15^post0, x_13^0'=x_13^post0, lt_18^0'=lt_18^post0, __const_17^0'=__const_17^post0, lt_20^0'=lt_20^post0, len_246^0'=len_246^post0, y_259^0'=y_259^post0, y_110^0'=y_110^post0, head_9^0'=head_9^post0, (0 == 0 /\ y_14^10-c_15^10 == 0 /\ 1-len_48^0 <= 0 /\ elem_16^10 <= 0 /\ c_15^30-lt_21^30 == 0 /\ y_14^post0-c_15^30 == 0 /\ Result_6^post0-head_9^0 == 0 /\ 2+a_128^post0-len_48^0 == 0 /\ -len_48^0 <= 0 /\ 1-a_128^post0-_^0+a_243^post0 == 0 /\ -y_158^0+lt_21^50 == 0 /\ -y_110^post0+y_110^0 == 0 /\ -prev_17^20 <= 0 /\ y_80^0-y_80^post0 == 0 /\ elem_16^20-x_13^30 == 0 /\ -y_80^0+lt_21^10 == 0 /\ y_14^20-c_15^20 == 0 /\ -lt_21^10+c_15^20 == 0 /\ prev_17^20 <= 0 /\ prev_17^20 == 0 /\ c_15^post0-lt_21^50 == 0 /\ y_309^0-y_309^post0 == 0 /\ x_13^20 == 0 /\ i_8^0-i_8^post0 == 0 /\ -head_9^post0+head_9^0 == 0 /\ prev_17^10 <= 0 /\ prev_17^10 == 0 /\ -lt_18^post0+lt_18^0 == 0 /\ -y_158^post0+y_158^0 == 0 /\ elem_16^10-x_13^20 == 0 /\ -x_13^10+c_15^10 == 0 /\ -__const_17^post0+__const_17^0 == 0 /\ lt_20^10-lt_19^10 <= 0 /\ -y_259^post0+y_259^0 == 0 /\ k_296^0-k_296^post0 == 0 /\ elem_16^post0-x_13^post0 == 0 /\ -elem_16^10 <= 0 /\ -a_128^post0 <= 0 /\ -Result_6^post0+x_13^10 == 0 /\ prev_17^post0 == 0 /\ x_13^30-y_14^10 == 0 /\ -x_23^post0+x_23^0 == 0 /\ -1+len_246^post0 == 0 /\ lt_21^30-y_110^0 == 0 /\ _^0-_^post0 == 0 /\ length_7^0-i_8^0 <= 0 /\ -y_14^20+x_13^post0 == 0 /\ length_7^0-length_7^post0 == 0 /\ -prev_17^10 <= 0 /\ -len_48^post0+len_48^0 == 0), cost: 1
New rule:
l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : a_243^0'=a_243^post1, prev_17^0'=prev_17^post1, length_7^0'=length_7^post1, y_80^0'=y_80^post1, _^0'=_^post1, lt_19^0'=lt_19^post1, k_296^0'=k_296^post1, y_158^0'=y_158^post1, x_23^0'=x_23^post1, elem_16^0'=elem_16^post1, a_128^0'=a_128^post1, lt_21^0'=lt_21^post1, len_48^0'=len_48^post1, y_309^0'=y_309^post1, y_14^0'=y_14^post1, Result_6^0'=Result_6^post1, i_8^0'=i_8^post1, c_15^0'=c_15^post1, x_13^0'=x_13^post1, lt_18^0'=lt_18^post1, __const_17^0'=__const_17^post1, lt_20^0'=lt_20^post1, len_246^0'=len_246^post1, y_259^0'=y_259^post1, y_110^0'=y_110^post1, head_9^0'=head_9^post1, (0 == 0 /\ a_128^0-a_128^post1 == 0 /\ y_158^0-y_158^post1 == 0 /\ -lt_20^post1+lt_20^0 == 0 /\ -x_13^post1+x_13^0 == 0 /\ a_243^0-a_243^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ -len_48^0 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_23^0-x_23^post1 == 0 /\ -y_259^post1+y_259^0 == 0 /\ -y_110^post1+y_110^0 == 0 /\ _^0-_^post1 == 0 /\ -__const_17^post1+__const_17^0 == 0 /\ -len_246^post1+len_246^0 == 0 /\ Result_6^0-Result_6^post1 == 0 /\ -1+i_8^post1-i_8^0 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ k_296^0-k_296^post1 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ -lt_19^post1+lt_19^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ elem_16^0-elem_16^post1 == 0 /\ -c_15^post1+c_15^0 == 0 /\ prev_17^0-prev_17^post1 == 0 /\ -1+len_48^post1-len_48^0 == 0 /\ y_80^0-y_80^post1 == 0), cost: 1
New rule:
l0 -> l2 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1

Applied preprocessing
Original rule:
l2 -> l0 : a_243^0'=a_243^post2, prev_17^0'=prev_17^post2, length_7^0'=length_7^post2, y_80^0'=y_80^post2, _^0'=_^post2, lt_19^0'=lt_19^post2, k_296^0'=k_296^post2, y_158^0'=y_158^post2, x_23^0'=x_23^post2, elem_16^0'=elem_16^post2, a_128^0'=a_128^post2, lt_21^0'=lt_21^post2, len_48^0'=len_48^post2, y_309^0'=y_309^post2, y_14^0'=y_14^post2, Result_6^0'=Result_6^post2, i_8^0'=i_8^post2, c_15^0'=c_15^post2, x_13^0'=x_13^post2, lt_18^0'=lt_18^post2, __const_17^0'=__const_17^post2, lt_20^0'=lt_20^post2, len_246^0'=len_246^post2, y_259^0'=y_259^post2, y_110^0'=y_110^post2, head_9^0'=head_9^post2, (-y_259^post2+y_259^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ Result_6^0-Result_6^post2 == 0 /\ __const_17^0-__const_17^post2 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_23^0-x_23^post2 == 0 /\ -len_48^post2+len_48^0 == 0 /\ _^0-_^post2 == 0 /\ y_158^0-y_158^post2 == 0 /\ k_296^0-k_296^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -c_15^post2+c_15^0 == 0 /\ y_80^0-y_80^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -len_246^post2+len_246^0 == 0 /\ prev_17^0-prev_17^post2 == 0 /\ -head_9^post2+head_9^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -a_243^post2+a_243^0 == 0 /\ -i_8^post2+i_8^0 == 0 /\ elem_16^0-elem_16^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -lt_21^post2+lt_21^0 == 0), cost: 1
New rule:
l2 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l0 : a_243^0'=a_243^post3, prev_17^0'=prev_17^post3, length_7^0'=length_7^post3, y_80^0'=y_80^post3, _^0'=_^post3, lt_19^0'=lt_19^post3, k_296^0'=k_296^post3, y_158^0'=y_158^post3, x_23^0'=x_23^post3, elem_16^0'=elem_16^post3, a_128^0'=a_128^post3, lt_21^0'=lt_21^post3, len_48^0'=len_48^post3, y_309^0'=y_309^post3, y_14^0'=y_14^post3, Result_6^0'=Result_6^post3, i_8^0'=i_8^post3, c_15^0'=c_15^post3, x_13^0'=x_13^post3, lt_18^0'=lt_18^post3, __const_17^0'=__const_17^post3, lt_20^0'=lt_20^post3, len_246^0'=len_246^post3, y_259^0'=y_259^post3, y_110^0'=y_110^post3, head_9^0'=head_9^post3, (0 == 0 /\ -c_15^post3+c_15^0 == 0 /\ -Result_6^post3+Result_6^0 == 0 /\ -len_246^post3+len_246^0 == 0 /\ y_158^0-y_158^post3 == 0 /\ lt_20^0-lt_20^post3 == 0 /\ x_13^110 == 0 /\ 1-length_7^post3+i_8^10 <= 0 /\ a_243^0-a_243^post3 == 0 /\ -x_23^0+x_13^post3 == 0 /\ k_296^0-k_296^post3 == 0 /\ -1-i_8^10+i_8^post3 == 0 /\ x_23^0-x_23^post3 == 0 /\ prev_17^0-prev_17^post3 == 0 /\ -i_8^10+len_48^post3 == 0 /\ i_8^10 == 0 /\ -_^post3+_^0 == 0 /\ head_9^10 == 0 /\ -y_14^post3+y_14^0 == 0 /\ -a_128^post3+a_128^0 == 0 /\ y_80^0-y_80^post3 == 0 /\ lt_18^0-lt_18^post3 == 0 /\ length_7^post3-__const_17^0 == 0 /\ elem_16^0-elem_16^post3 == 0 /\ -y_309^post3+y_309^0 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ lt_19^0-lt_19^post3 == 0 /\ -y_259^post3+y_259^0 == 0 /\ -y_110^post3+y_110^0 == 0 /\ -__const_17^post3+__const_17^0 == 0), cost: 1
New rule:
l3 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l4 : a_243^0'=a_243^post4, prev_17^0'=prev_17^post4, length_7^0'=length_7^post4, y_80^0'=y_80^post4, _^0'=_^post4, lt_19^0'=lt_19^post4, k_296^0'=k_296^post4, y_158^0'=y_158^post4, x_23^0'=x_23^post4, elem_16^0'=elem_16^post4, a_128^0'=a_128^post4, lt_21^0'=lt_21^post4, len_48^0'=len_48^post4, y_309^0'=y_309^post4, y_14^0'=y_14^post4, Result_6^0'=Result_6^post4, i_8^0'=i_8^post4, c_15^0'=c_15^post4, x_13^0'=x_13^post4, lt_18^0'=lt_18^post4, __const_17^0'=__const_17^post4, lt_20^0'=lt_20^post4, len_246^0'=len_246^post4, y_259^0'=y_259^post4, y_110^0'=y_110^post4, head_9^0'=head_9^post4, (0 == 0 /\ prev_17^0 <= 0 /\ y_80^0-y_80^post4 == 0 /\ lt_18^0-lt_18^post4 == 0 /\ a_243^0-a_243^post4 == 0 /\ -y_14^post4+y_14^0 == 0 /\ -y_309^post4+y_309^0 == 0 /\ i_8^0-i_8^post4 == 0 /\ -y_259^post4+y_259^0 == 0 /\ -len_246^0+k_296^post4 == 0 /\ -len_246^post4+len_246^0 == 0 /\ -len_246^0 <= 0 /\ -elem_16^post4+elem_16^0 == 0 /\ -Result_6^post4+Result_6^0 == 0 /\ -y_158^post4+y_158^0 == 0 /\ len_48^0-len_48^post4 == 0 /\ _^0-_^post4 == 0 /\ -a_128^post4+a_128^0 == 0 /\ -y_14^0+x_13^post4 == 0 /\ x_23^0-x_23^post4 == 0 /\ -y_110^post4+y_110^0 == 0 /\ lt_20^110-lt_19^11 <= 0 /\ prev_17^0-prev_17^post4 == 0 /\ -a_243^0 <= 0 /\ -__const_17^post4+__const_17^0 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -head_9^post4+head_9^0 == 0 /\ -c_15^post4+c_15^0 == 0 /\ length_7^0-length_7^post4 == 0 /\ -prev_17^0 <= 0), cost: 1
New rule:
l1 -> l4 : lt_19^0'=lt_19^post4, k_296^0'=len_246^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l4 -> l1 : a_243^0'=a_243^post7, prev_17^0'=prev_17^post7, length_7^0'=length_7^post7, y_80^0'=y_80^post7, _^0'=_^post7, lt_19^0'=lt_19^post7, k_296^0'=k_296^post7, y_158^0'=y_158^post7, x_23^0'=x_23^post7, elem_16^0'=elem_16^post7, a_128^0'=a_128^post7, lt_21^0'=lt_21^post7, len_48^0'=len_48^post7, y_309^0'=y_309^post7, y_14^0'=y_14^post7, Result_6^0'=Result_6^post7, i_8^0'=i_8^post7, c_15^0'=c_15^post7, x_13^0'=x_13^post7, lt_18^0'=lt_18^post7, __const_17^0'=__const_17^post7, lt_20^0'=lt_20^post7, len_246^0'=len_246^post7, y_259^0'=y_259^post7, y_110^0'=y_110^post7, head_9^0'=head_9^post7, (0 == 0 /\ -1-k_296^0+len_246^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ prev_17^post7 == 0 /\ -lt_20^post7+lt_20^0 == 0 /\ y_158^0-y_158^post7 == 0 /\ y_80^0-y_80^post7 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -y_110^post7+y_110^0 == 0 /\ elem_16^post7-x_13^0 == 0 /\ _^0-_^post7 == 0 /\ y_14^post7-c_15^0 == 0 /\ x_23^0-x_23^post7 == 0 /\ -len_48^post7+len_48^0 == 0 /\ Result_6^0-Result_6^post7 == 0 /\ lt_21^11-y_309^0 == 0 /\ 1-a_243^0+a_243^post7 == 0 /\ k_296^0-k_296^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ length_7^0-length_7^post7 == 0 /\ a_128^0-a_128^post7 == 0 /\ -k_296^0 <= 0 /\ -lt_21^11+c_15^post7 == 0 /\ -lt_19^post7+lt_19^0 == 0 /\ y_309^0-y_309^post7 == 0 /\ -__const_17^post7+__const_17^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ -a_243^0 <= 0 /\ -x_13^post7+x_13^0 == 0), cost: 1
New rule:
l4 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, elem_16^0'=x_13^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, len_246^0'=1+k_296^0, (a_243^0 >= 0 /\ k_296^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l7 -> l3 : a_243^0'=a_243^post8, prev_17^0'=prev_17^post8, length_7^0'=length_7^post8, y_80^0'=y_80^post8, _^0'=_^post8, lt_19^0'=lt_19^post8, k_296^0'=k_296^post8, y_158^0'=y_158^post8, x_23^0'=x_23^post8, elem_16^0'=elem_16^post8, a_128^0'=a_128^post8, lt_21^0'=lt_21^post8, len_48^0'=len_48^post8, y_309^0'=y_309^post8, y_14^0'=y_14^post8, Result_6^0'=Result_6^post8, i_8^0'=i_8^post8, c_15^0'=c_15^post8, x_13^0'=x_13^post8, lt_18^0'=lt_18^post8, __const_17^0'=__const_17^post8, lt_20^0'=lt_20^post8, len_246^0'=len_246^post8, y_259^0'=y_259^post8, y_110^0'=y_110^post8, head_9^0'=head_9^post8, (elem_16^0-elem_16^post8 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ lt_19^0-lt_19^post8 == 0 /\ y_309^0-y_309^post8 == 0 /\ k_296^0-k_296^post8 == 0 /\ -__const_17^post8+__const_17^0 == 0 /\ a_243^0-a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ y_158^0-y_158^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ c_15^0-c_15^post8 == 0 /\ len_48^0-len_48^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ prev_17^0-prev_17^post8 == 0 /\ a_128^0-a_128^post8 == 0 /\ -y_14^post8+y_14^0 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -Result_6^post8+Result_6^0 == 0 /\ -len_246^post8+len_246^0 == 0 /\ y_259^0-y_259^post8 == 0 /\ _^0-_^post8 == 0 /\ -x_23^post8+x_23^0 == 0 /\ -lt_18^post8+lt_18^0 == 0), cost: 1
New rule:
l7 -> l3 : TRUE, cost: 1

Simplified rules
Start location: l7
   9: l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
  10: l0 -> l2 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1
  13: l1 -> l4 : lt_19^0'=lt_19^post4, k_296^0'=len_246^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 1
  11: l2 -> l0 : TRUE, cost: 1
  12: l3 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 1
  14: l4 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, elem_16^0'=x_13^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, len_246^0'=1+k_296^0, (a_243^0 >= 0 /\ k_296^0 >= 0), cost: 1
  15: l7 -> l3 : TRUE, cost: 1


Eliminating location l3 by chaining:

Applied chaining
First rule:
l7 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 1
New rule:
l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 12 15

Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1
Second rule:
l2 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 10 11

Eliminating location l4 by chaining:

Applied chaining
First rule:
l1 -> l4 : lt_19^0'=lt_19^post4, k_296^0'=len_246^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 1
Second rule:
l4 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, elem_16^0'=x_13^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, len_246^0'=1+k_296^0, (a_243^0 >= 0 /\ k_296^0 >= 0), cost: 1
New rule:
l1 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=len_246^0, elem_16^0'=y_14^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, len_246^0'=1+len_246^0, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 13 14

Eliminated locations on linear paths
Start location: l7
   9: l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
  17: l0 -> l0 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 2
  18: l1 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=len_246^0, elem_16^0'=y_14^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, len_246^0'=1+len_246^0, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 2
  16: l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 2


Applied acceleration
Original rule:
l0 -> l0 : len_48^0'=1+len_48^0, i_8^0'=1+i_8^0, head_9^0'=head_9^post1, (len_48^0 >= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 2
New rule:
l0 -> l0 : len_48^0'=n+len_48^0, i_8^0'=n+i_8^0, head_9^0'=head_9^post1, (-1+n >= 0 /\ len_48^0 >= 0 /\ length_7^0-n-i_8^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_bPhoJG.txt

Applied instantiation
Original rule:
l0 -> l0 : len_48^0'=n+len_48^0, i_8^0'=n+i_8^0, head_9^0'=head_9^post1, (-1+n >= 0 /\ len_48^0 >= 0 /\ length_7^0-n-i_8^0 >= 0), cost: 2*n
New rule:
l0 -> l0 : len_48^0'=length_7^0+len_48^0-i_8^0, i_8^0'=length_7^0, head_9^0'=head_9^post1, (0 >= 0 /\ -1+length_7^0-i_8^0 >= 0 /\ len_48^0 >= 0), cost: 2*length_7^0-2*i_8^0

Applied simplification
Original rule:
l0 -> l0 : len_48^0'=length_7^0+len_48^0-i_8^0, i_8^0'=length_7^0, head_9^0'=head_9^post1, (0 >= 0 /\ -1+length_7^0-i_8^0 >= 0 /\ len_48^0 >= 0), cost: 2*length_7^0-2*i_8^0
New rule:
l0 -> l0 : len_48^0'=length_7^0+len_48^0-i_8^0, i_8^0'=length_7^0, head_9^0'=head_9^post1, (-1+length_7^0-i_8^0 >= 0 /\ len_48^0 >= 0), cost: 2*length_7^0-2*i_8^0

Applied deletion
Removed the following rules: 17

Applied acceleration
Original rule:
l1 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=len_246^0, elem_16^0'=y_14^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, len_246^0'=1+len_246^0, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 2
New rule:
l1 -> l1 : a_243^0'=a_243^0-n0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=-1+n0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=n0+len_246^0, (prev_17^0 >= 0 /\ 1+a_243^0-n0 >= 0 /\ -3+n0 >= 0 /\ len_246^0 >= 0 /\ -prev_17^0 >= 0), cost: 2*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_MbdgDO.txt

Applied instantiation
Original rule:
l1 -> l1 : a_243^0'=a_243^0-n0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=-1+n0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=n0+len_246^0, (prev_17^0 >= 0 /\ 1+a_243^0-n0 >= 0 /\ -3+n0 >= 0 /\ len_246^0 >= 0 /\ -prev_17^0 >= 0), cost: 2*n0
New rule:
l1 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=a_243^0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=1+a_243^0+len_246^0, (0 >= 0 /\ prev_17^0 >= 0 /\ -2+a_243^0 >= 0 /\ len_246^0 >= 0 /\ -prev_17^0 >= 0), cost: 2+2*a_243^0

Applied simplification
Original rule:
l1 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=a_243^0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=1+a_243^0+len_246^0, (0 >= 0 /\ prev_17^0 >= 0 /\ -2+a_243^0 >= 0 /\ len_246^0 >= 0 /\ -prev_17^0 >= 0), cost: 2+2*a_243^0
New rule:
l1 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=a_243^0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=1+a_243^0+len_246^0, (prev_17^0 <= 0 /\ prev_17^0 >= 0 /\ -2+a_243^0 >= 0 /\ len_246^0 >= 0), cost: 2+2*a_243^0

Accelerated simple loops
Start location: l7
   9: l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
  20: l0 -> l0 : len_48^0'=length_7^0+len_48^0-i_8^0, i_8^0'=length_7^0, head_9^0'=head_9^post1, (-1+length_7^0-i_8^0 >= 0 /\ len_48^0 >= 0), cost: 2*length_7^0-2*i_8^0
  18: l1 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=len_246^0, elem_16^0'=y_14^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, len_246^0'=1+len_246^0, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 2
  22: l1 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=a_243^0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=1+a_243^0+len_246^0, (prev_17^0 <= 0 /\ prev_17^0 >= 0 /\ -2+a_243^0 >= 0 /\ len_246^0 >= 0), cost: 2+2*a_243^0
  16: l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 2


Applied chaining
First rule:
l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 2
Second rule:
l0 -> l0 : len_48^0'=length_7^0+len_48^0-i_8^0, i_8^0'=length_7^0, head_9^0'=head_9^post1, (-1+length_7^0-i_8^0 >= 0 /\ len_48^0 >= 0), cost: 2*length_7^0-2*i_8^0
New rule:
l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=-1+__const_17^0, i_8^0'=__const_17^0, x_13^0'=x_23^0, head_9^0'=head_9^post1, -2+__const_17^0 >= 0, cost: 2*__const_17^0

Applied deletion
Removed the following rules: 20

Applied chaining
First rule:
l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
Second rule:
l1 -> l1 : a_243^0'=-1+a_243^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=len_246^0, elem_16^0'=y_14^0, lt_21^0'=lt_21^post7, y_14^0'=c_15^0, c_15^0'=y_309^0, x_13^0'=y_14^0, lt_20^0'=lt_20^post4, len_246^0'=1+len_246^0, (a_243^0 >= 0 /\ prev_17^0 == 0 /\ len_246^0 >= 0), cost: 2
New rule:
l0 -> l1 : a_243^0'=-4+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=1, elem_16^0'=y_110^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post7, y_14^0'=y_158^0, Result_6^0'=head_9^0, c_15^0'=y_309^0, x_13^0'=y_110^0, lt_20^0'=lt_20^post4, len_246^0'=2, (-3+_^0+len_48^0 >= 0 /\ length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 3

Applied chaining
First rule:
l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
Second rule:
l1 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=a_243^0+len_246^0, elem_16^0'=y_309^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=1+a_243^0+len_246^0, (prev_17^0 <= 0 /\ prev_17^0 >= 0 /\ -2+a_243^0 >= 0 /\ len_246^0 >= 0), cost: 2+2*a_243^0
New rule:
l0 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=-2+_^0+len_48^0, elem_16^0'=y_309^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, Result_6^0'=head_9^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=-1+_^0+len_48^0, (-5+_^0+len_48^0 >= 0 /\ length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: -3+2*_^0+2*len_48^0

Applied deletion
Removed the following rules: 18 22

Chained accelerated rules with incoming rules
Start location: l7
   9: l0 -> l1 : a_243^0'=-3+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post0, elem_16^0'=y_80^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post0, y_14^0'=y_110^0, Result_6^0'=head_9^0, c_15^0'=y_158^0, x_13^0'=y_80^0, lt_20^0'=lt_20^post0, len_246^0'=1, (length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 1
  24: l0 -> l1 : a_243^0'=-4+_^0+len_48^0, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=1, elem_16^0'=y_110^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post7, y_14^0'=y_158^0, Result_6^0'=head_9^0, c_15^0'=y_309^0, x_13^0'=y_110^0, lt_20^0'=lt_20^post4, len_246^0'=2, (-3+_^0+len_48^0 >= 0 /\ length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: 3
  25: l0 -> l1 : a_243^0'=-1, prev_17^0'=0, lt_19^0'=lt_19^post4, k_296^0'=-2+_^0+len_48^0, elem_16^0'=y_309^0, a_128^0'=-2+len_48^0, lt_21^0'=lt_21^post7, y_14^0'=y_309^0, Result_6^0'=head_9^0, c_15^0'=y_309^0, x_13^0'=y_309^0, lt_20^0'=lt_20^post4, len_246^0'=-1+_^0+len_48^0, (-5+_^0+len_48^0 >= 0 /\ length_7^0-i_8^0 <= 0 /\ -2+len_48^0 >= 0), cost: -3+2*_^0+2*len_48^0
  16: l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=0, i_8^0'=1, x_13^0'=x_23^0, head_9^0'=head_9^post3, -1+__const_17^0 >= 0, cost: 2
  23: l7 -> l0 : length_7^0'=__const_17^0, len_48^0'=-1+__const_17^0, i_8^0'=__const_17^0, x_13^0'=x_23^0, head_9^0'=head_9^post1, -2+__const_17^0 >= 0, cost: 2*__const_17^0


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


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0