unknown Initial ITS Start location: l7 Program variables: _^0 a_128^0 a_243^0 c_15^0 elem_16^0 head_9^0 i_8^0 k_296^0 len_246^0 len_48^0 length_7^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 prev_17^0 result_6^0 x_13^0 x_23^0 y_110^0 y_14^0 y_158^0 y_259^0 y_309^0 y_80^0 0: l0 -> l1 : _^0'=_^post1, a_128^0'=a_128^post1, a_243^0'=a_243^post1, c_15^0'=c_15^post1, elem_16^0'=elem_16^post1, head_9^0'=head_9^post1, i_8^0'=i_8^post1, k_296^0'=k_296^post1, len_246^0'=len_246^post1, len_48^0'=len_48^post1, length_7^0'=length_7^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=prev_17^post1, result_6^0'=result_6^post1, x_13^0'=x_13^post1, x_23^0'=x_23^post1, y_110^0'=y_110^post1, y_14^0'=y_14^post1, y_158^0'=y_158^post1, y_259^0'=y_259^post1, y_309^0'=y_309^post1, y_80^0'=y_80^post1, (0 == 0 /\ 1-a_128^post1-_^0+a_243^post1 == 0 /\ -y_80^post1+y_80^0 == 0 /\ -a_128^post1 <= 0 /\ _^0-_^post1 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ x_13^1-result_6^post1 == 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -y_259^post1+y_259^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ -y_14^2+x_13^post1 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ y_158^0-y_158^post1 == 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ c_15^post1-lt_21^5 == 0 /\ 2+a_128^post1-len_48^0 == 0 /\ -k_296^post1+k_296^0 == 0 /\ prev_17^post1 == 0 /\ result_6^post1-head_9^0 == 0 /\ y_110^0-y_110^post1 == 0 /\ -elem_16^1 <= 0 /\ y_14^post1-c_15^3 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -1+len_246^post1 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^3+c_15^3 == 0 /\ -x_23^post1+x_23^0 == 0 /\ -x_13^post1+elem_16^post1 == 0 /\ length_7^0-i_8^0 <= 0 /\ -i_8^post1+i_8^0 == 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_13^2 == 0 /\ -head_9^post1+head_9^0 == 0 /\ -len_48^post1+len_48^0 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 1: l0 -> l2 : _^0'=_^post2, a_128^0'=a_128^post2, a_243^0'=a_243^post2, c_15^0'=c_15^post2, elem_16^0'=elem_16^post2, head_9^0'=head_9^post2, i_8^0'=i_8^post2, k_296^0'=k_296^post2, len_246^0'=len_246^post2, len_48^0'=len_48^post2, length_7^0'=length_7^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, prev_17^0'=prev_17^post2, result_6^0'=result_6^post2, x_13^0'=x_13^post2, x_23^0'=x_23^post2, y_110^0'=y_110^post2, y_14^0'=y_14^post2, y_158^0'=y_158^post2, y_259^0'=y_259^post2, y_309^0'=y_309^post2, y_80^0'=y_80^post2, (0 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ a_243^0-a_243^post2 == 0 /\ -len_48^0 <= 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ result_6^0-result_6^post2 == 0), cost: 1 4: l1 -> l4 : _^0'=_^post5, a_128^0'=a_128^post5, a_243^0'=a_243^post5, c_15^0'=c_15^post5, elem_16^0'=elem_16^post5, head_9^0'=head_9^post5, i_8^0'=i_8^post5, k_296^0'=k_296^post5, len_246^0'=len_246^post5, len_48^0'=len_48^post5, length_7^0'=length_7^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, prev_17^0'=prev_17^post5, result_6^0'=result_6^post5, x_13^0'=x_13^post5, x_23^0'=x_23^post5, y_110^0'=y_110^post5, y_14^0'=y_14^post5, y_158^0'=y_158^post5, y_259^0'=y_259^post5, y_309^0'=y_309^post5, y_80^0'=y_80^post5, (0 == 0 /\ _^0-_^post5 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -len_48^post5+len_48^0 == 0 /\ -lt_18^post5+lt_18^0 == 0 /\ y_14^0-y_14^post5 == 0 /\ x_23^0-x_23^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ -y_14^0+x_13^post5 == 0 /\ -y_110^post5+y_110^0 == 0 /\ result_6^0-result_6^post5 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ a_243^0-a_243^post5 == 0 /\ -head_9^post5+head_9^0 == 0 /\ length_7^0-length_7^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -a_128^post5+a_128^0 == 0 /\ -y_309^post5+y_309^0 == 0 /\ -len_246^0+k_296^post5 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ y_259^0-y_259^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -y_80^post5+y_80^0 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -elem_16^post5+elem_16^0 == 0 /\ -prev_17^post5+prev_17^0 == 0), cost: 1 5: l1 -> l5 : _^0'=_^post6, a_128^0'=a_128^post6, a_243^0'=a_243^post6, c_15^0'=c_15^post6, elem_16^0'=elem_16^post6, head_9^0'=head_9^post6, i_8^0'=i_8^post6, k_296^0'=k_296^post6, len_246^0'=len_246^post6, len_48^0'=len_48^post6, length_7^0'=length_7^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, prev_17^0'=prev_17^post6, result_6^0'=result_6^post6, x_13^0'=x_13^post6, x_23^0'=x_23^post6, y_110^0'=y_110^post6, y_14^0'=y_14^post6, y_158^0'=y_158^post6, y_259^0'=y_259^post6, y_309^0'=y_309^post6, y_80^0'=y_80^post6, (0 == 0 /\ -head_9^post6+head_9^0 == 0 /\ -a_243^0 <= 0 /\ y_14^0-y_14^post6 == 0 /\ elem_16^post6-lt_18^1 == 0 /\ -len_48^post6+len_48^0 == 0 /\ y_158^0-y_158^post6 == 0 /\ prev_17^post6-elem_16^0 == 0 /\ -a_128^post6+a_128^0 == 0 /\ -_^post6+_^0 == 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ length_7^0-length_7^post6 == 0 /\ -k_296^post6+k_296^0 == 0 /\ -y_259^0+lt_18^1 == 0 /\ x_23^0-x_23^post6 == 0 /\ 1+lt_19^1-lt_20^1 <= 0 /\ -x_13^post6+x_13^0 == 0 /\ -y_80^post6+y_80^0 == 0 /\ -y_110^post6+y_110^0 == 0 /\ -i_8^post6+i_8^0 == 0 /\ -y_309^post6+y_309^0 == 0 /\ -result_6^post6+result_6^0 == 0 /\ len_246^0-len_246^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ a_243^0-a_243^post6 == 0 /\ -y_259^post6+y_259^0 == 0 /\ -c_15^post6+c_15^0 == 0), cost: 1 2: l2 -> l0 : _^0'=_^post3, a_128^0'=a_128^post3, a_243^0'=a_243^post3, c_15^0'=c_15^post3, elem_16^0'=elem_16^post3, head_9^0'=head_9^post3, i_8^0'=i_8^post3, k_296^0'=k_296^post3, len_246^0'=len_246^post3, len_48^0'=len_48^post3, length_7^0'=length_7^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, prev_17^0'=prev_17^post3, result_6^0'=result_6^post3, x_13^0'=x_13^post3, x_23^0'=x_23^post3, y_110^0'=y_110^post3, y_14^0'=y_14^post3, y_158^0'=y_158^post3, y_259^0'=y_259^post3, y_309^0'=y_309^post3, y_80^0'=y_80^post3, (-y_80^post3+y_80^0 == 0 /\ -i_8^post3+i_8^0 == 0 /\ -head_9^post3+head_9^0 == 0 /\ -a_128^post3+a_128^0 == 0 /\ length_7^0-length_7^post3 == 0 /\ y_309^0-y_309^post3 == 0 /\ -prev_17^post3+prev_17^0 == 0 /\ y_14^0-y_14^post3 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ k_296^0-k_296^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -c_15^post3+c_15^0 == 0 /\ -y_110^post3+y_110^0 == 0 /\ -y_259^post3+y_259^0 == 0 /\ y_158^0-y_158^post3 == 0 /\ a_243^0-a_243^post3 == 0 /\ -len_48^post3+len_48^0 == 0 /\ -x_23^post3+x_23^0 == 0 /\ -len_246^post3+len_246^0 == 0 /\ result_6^0-result_6^post3 == 0 /\ x_13^0-x_13^post3 == 0 /\ -lt_18^post3+lt_18^0 == 0 /\ _^0-_^post3 == 0 /\ -elem_16^post3+elem_16^0 == 0), cost: 1 3: l3 -> l0 : _^0'=_^post4, a_128^0'=a_128^post4, a_243^0'=a_243^post4, c_15^0'=c_15^post4, elem_16^0'=elem_16^post4, head_9^0'=head_9^post4, i_8^0'=i_8^post4, k_296^0'=k_296^post4, len_246^0'=len_246^post4, len_48^0'=len_48^post4, length_7^0'=length_7^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, prev_17^0'=prev_17^post4, result_6^0'=result_6^post4, x_13^0'=x_13^post4, x_23^0'=x_23^post4, y_110^0'=y_110^post4, y_14^0'=y_14^post4, y_158^0'=y_158^post4, y_259^0'=y_259^post4, y_309^0'=y_309^post4, y_80^0'=y_80^post4, (0 == 0 /\ a_243^0-a_243^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ y_158^0-y_158^post4 == 0 /\ -x_23^post4+x_23^0 == 0 /\ result_6^0-result_6^post4 == 0 /\ -1-i_8^1+i_8^post4 == 0 /\ x_13^1 == 0 /\ -y_80^post4+y_80^0 == 0 /\ y_110^0-y_110^post4 == 0 /\ -lt_18^post4+lt_18^0 == 0 /\ prev_17^0-prev_17^post4 == 0 /\ lt_19^0-lt_19^post4 == 0 /\ len_246^0-len_246^post4 == 0 /\ -k_296^post4+k_296^0 == 0 /\ head_9^1 == 0 /\ -elem_16^post4+elem_16^0 == 0 /\ -c_15^post4+c_15^0 == 0 /\ x_13^post4-x_23^0 == 0 /\ -y_309^post4+y_309^0 == 0 /\ y_14^0-y_14^post4 == 0 /\ -y_259^post4+y_259^0 == 0 /\ -17+length_7^post4 == 0 /\ -_^post4+_^0 == 0 /\ i_8^1 == 0 /\ -i_8^1+len_48^post4 == 0 /\ -lt_20^post4+lt_20^0 == 0 /\ -a_128^post4+a_128^0 == 0 /\ 1-length_7^post4+i_8^1 <= 0), cost: 1 6: l4 -> l6 : _^0'=_^post7, a_128^0'=a_128^post7, a_243^0'=a_243^post7, c_15^0'=c_15^post7, elem_16^0'=elem_16^post7, head_9^0'=head_9^post7, i_8^0'=i_8^post7, k_296^0'=k_296^post7, len_246^0'=len_246^post7, len_48^0'=len_48^post7, length_7^0'=length_7^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, prev_17^0'=prev_17^post7, result_6^0'=result_6^post7, x_13^0'=x_13^post7, x_23^0'=x_23^post7, y_110^0'=y_110^post7, y_14^0'=y_14^post7, y_158^0'=y_158^post7, y_259^0'=y_259^post7, y_309^0'=y_309^post7, y_80^0'=y_80^post7, (0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -a_243^0 <= 0 /\ lt_20^0-lt_20^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ y_110^0-y_110^post7 == 0 /\ -k_296^post7+k_296^0 == 0 /\ prev_17^0-prev_17^post7 == 0 /\ -x_23^post7+x_23^0 == 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ -elem_16^post7+elem_16^0 == 0 /\ -y_309^post7+y_309^0 == 0 /\ -y_80^post7+y_80^0 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ a_243^0-a_243^post7 == 0 /\ y_14^0-y_14^post7 == 0 /\ c_15^0-c_15^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -a_128^post7+a_128^0 == 0 /\ -c_15^0 <= 0 /\ len_48^0-len_48^post7 == 0 /\ _^0-_^post7 == 0 /\ len_246^0-len_246^post7 == 0 /\ -length_7^post7+length_7^0 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ y_158^0-y_158^post7 == 0), cost: 1 7: l4 -> l1 : _^0'=_^post8, a_128^0'=a_128^post8, a_243^0'=a_243^post8, c_15^0'=c_15^post8, elem_16^0'=elem_16^post8, head_9^0'=head_9^post8, i_8^0'=i_8^post8, k_296^0'=k_296^post8, len_246^0'=len_246^post8, len_48^0'=len_48^post8, length_7^0'=length_7^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, prev_17^0'=prev_17^post8, result_6^0'=result_6^post8, x_13^0'=x_13^post8, x_23^0'=x_23^post8, y_110^0'=y_110^post8, y_14^0'=y_14^post8, y_158^0'=y_158^post8, y_259^0'=y_259^post8, y_309^0'=y_309^post8, y_80^0'=y_80^post8, (0 == 0 /\ y_158^0-y_158^post8 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -a_128^post8+a_128^0 == 0 /\ -a_243^0 <= 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -len_48^post8+len_48^0 == 0 /\ -k_296^0 <= 0 /\ -y_259^post8+y_259^0 == 0 /\ lt_21^1-y_309^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ 1-a_243^0+a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ -k_296^post8+k_296^0 == 0 /\ y_309^0-y_309^post8 == 0 /\ -x_13^0+elem_16^post8 == 0 /\ -c_15^0+y_14^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ x_23^0-x_23^post8 == 0 /\ -lt_21^1+c_15^post8 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ _^0-_^post8 == 0 /\ -1-k_296^0+len_246^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ prev_17^post8 == 0), cost: 1 8: l7 -> l3 : _^0'=_^post9, a_128^0'=a_128^post9, a_243^0'=a_243^post9, c_15^0'=c_15^post9, elem_16^0'=elem_16^post9, head_9^0'=head_9^post9, i_8^0'=i_8^post9, k_296^0'=k_296^post9, len_246^0'=len_246^post9, len_48^0'=len_48^post9, length_7^0'=length_7^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, prev_17^0'=prev_17^post9, result_6^0'=result_6^post9, x_13^0'=x_13^post9, x_23^0'=x_23^post9, y_110^0'=y_110^post9, y_14^0'=y_14^post9, y_158^0'=y_158^post9, y_259^0'=y_259^post9, y_309^0'=y_309^post9, y_80^0'=y_80^post9, (result_6^0-result_6^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ -x_23^post9+x_23^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post9+y_259^0 == 0 /\ -c_15^post9+c_15^0 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0), cost: 1 Chained Linear Paths Start location: l7 Program variables: _^0 a_128^0 a_243^0 c_15^0 elem_16^0 head_9^0 i_8^0 k_296^0 len_246^0 len_48^0 length_7^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 prev_17^0 result_6^0 x_13^0 x_23^0 y_110^0 y_14^0 y_158^0 y_259^0 y_309^0 y_80^0 0: l0 -> l1 : _^0'=_^post1, a_128^0'=a_128^post1, a_243^0'=a_243^post1, c_15^0'=c_15^post1, elem_16^0'=elem_16^post1, head_9^0'=head_9^post1, i_8^0'=i_8^post1, k_296^0'=k_296^post1, len_246^0'=len_246^post1, len_48^0'=len_48^post1, length_7^0'=length_7^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=prev_17^post1, result_6^0'=result_6^post1, x_13^0'=x_13^post1, x_23^0'=x_23^post1, y_110^0'=y_110^post1, y_14^0'=y_14^post1, y_158^0'=y_158^post1, y_259^0'=y_259^post1, y_309^0'=y_309^post1, y_80^0'=y_80^post1, (0 == 0 /\ 1-a_128^post1-_^0+a_243^post1 == 0 /\ -y_80^post1+y_80^0 == 0 /\ -a_128^post1 <= 0 /\ _^0-_^post1 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ x_13^1-result_6^post1 == 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -y_259^post1+y_259^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ -y_14^2+x_13^post1 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ y_158^0-y_158^post1 == 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ c_15^post1-lt_21^5 == 0 /\ 2+a_128^post1-len_48^0 == 0 /\ -k_296^post1+k_296^0 == 0 /\ prev_17^post1 == 0 /\ result_6^post1-head_9^0 == 0 /\ y_110^0-y_110^post1 == 0 /\ -elem_16^1 <= 0 /\ y_14^post1-c_15^3 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -1+len_246^post1 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^3+c_15^3 == 0 /\ -x_23^post1+x_23^0 == 0 /\ -x_13^post1+elem_16^post1 == 0 /\ length_7^0-i_8^0 <= 0 /\ -i_8^post1+i_8^0 == 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_13^2 == 0 /\ -head_9^post1+head_9^0 == 0 /\ -len_48^post1+len_48^0 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 10: l0 -> l0 : _^0'=_^post3, a_128^0'=a_128^post3, a_243^0'=a_243^post3, c_15^0'=c_15^post3, elem_16^0'=elem_16^post3, head_9^0'=head_9^post3, i_8^0'=i_8^post3, k_296^0'=k_296^post3, len_246^0'=len_246^post3, len_48^0'=len_48^post3, length_7^0'=length_7^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, prev_17^0'=prev_17^post3, result_6^0'=result_6^post3, x_13^0'=x_13^post3, x_23^0'=x_23^post3, y_110^0'=y_110^post3, y_14^0'=y_14^post3, y_158^0'=y_158^post3, y_259^0'=y_259^post3, y_309^0'=y_309^post3, y_80^0'=y_80^post3, (0 == 0 /\ prev_17^post2-prev_17^post3 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ head_9^post2-head_9^post3 == 0 /\ -c_15^post3+c_15^post2 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ y_309^post2-y_309^post3 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ lt_21^post2-lt_21^post3 == 0 /\ y_80^post2-y_80^post3 == 0 /\ a_243^0-a_243^post2 == 0 /\ result_6^post2-result_6^post3 == 0 /\ y_158^post2-y_158^post3 == 0 /\ -len_48^0 <= 0 /\ length_7^post2-length_7^post3 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ lt_19^post2-lt_19^post3 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ k_296^post2-k_296^post3 == 0 /\ -elem_16^post3+elem_16^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ x_23^post2-x_23^post3 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_18^post3+lt_18^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ len_48^post2-len_48^post3 == 0 /\ -len_246^post3+len_246^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ y_110^post2-y_110^post3 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ lt_20^post2-lt_20^post3 == 0 /\ -a_128^post3+a_128^post2 == 0 /\ y_14^post2-y_14^post3 == 0 /\ i_8^post2-i_8^post3 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ a_243^post2-a_243^post3 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ -_^post3+_^post2 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ x_13^post2-x_13^post3 == 0 /\ y_259^post2-y_259^post3 == 0 /\ result_6^0-result_6^post2 == 0), cost: 1 4: l1 -> l4 : _^0'=_^post5, a_128^0'=a_128^post5, a_243^0'=a_243^post5, c_15^0'=c_15^post5, elem_16^0'=elem_16^post5, head_9^0'=head_9^post5, i_8^0'=i_8^post5, k_296^0'=k_296^post5, len_246^0'=len_246^post5, len_48^0'=len_48^post5, length_7^0'=length_7^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, prev_17^0'=prev_17^post5, result_6^0'=result_6^post5, x_13^0'=x_13^post5, x_23^0'=x_23^post5, y_110^0'=y_110^post5, y_14^0'=y_14^post5, y_158^0'=y_158^post5, y_259^0'=y_259^post5, y_309^0'=y_309^post5, y_80^0'=y_80^post5, (0 == 0 /\ _^0-_^post5 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -len_48^post5+len_48^0 == 0 /\ -lt_18^post5+lt_18^0 == 0 /\ y_14^0-y_14^post5 == 0 /\ x_23^0-x_23^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ -y_14^0+x_13^post5 == 0 /\ -y_110^post5+y_110^0 == 0 /\ result_6^0-result_6^post5 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ a_243^0-a_243^post5 == 0 /\ -head_9^post5+head_9^0 == 0 /\ length_7^0-length_7^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -a_128^post5+a_128^0 == 0 /\ -y_309^post5+y_309^0 == 0 /\ -len_246^0+k_296^post5 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ y_259^0-y_259^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -y_80^post5+y_80^0 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -elem_16^post5+elem_16^0 == 0 /\ -prev_17^post5+prev_17^0 == 0), cost: 1 5: l1 -> l5 : _^0'=_^post6, a_128^0'=a_128^post6, a_243^0'=a_243^post6, c_15^0'=c_15^post6, elem_16^0'=elem_16^post6, head_9^0'=head_9^post6, i_8^0'=i_8^post6, k_296^0'=k_296^post6, len_246^0'=len_246^post6, len_48^0'=len_48^post6, length_7^0'=length_7^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, prev_17^0'=prev_17^post6, result_6^0'=result_6^post6, x_13^0'=x_13^post6, x_23^0'=x_23^post6, y_110^0'=y_110^post6, y_14^0'=y_14^post6, y_158^0'=y_158^post6, y_259^0'=y_259^post6, y_309^0'=y_309^post6, y_80^0'=y_80^post6, (0 == 0 /\ -head_9^post6+head_9^0 == 0 /\ -a_243^0 <= 0 /\ y_14^0-y_14^post6 == 0 /\ elem_16^post6-lt_18^1 == 0 /\ -len_48^post6+len_48^0 == 0 /\ y_158^0-y_158^post6 == 0 /\ prev_17^post6-elem_16^0 == 0 /\ -a_128^post6+a_128^0 == 0 /\ -_^post6+_^0 == 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ length_7^0-length_7^post6 == 0 /\ -k_296^post6+k_296^0 == 0 /\ -y_259^0+lt_18^1 == 0 /\ x_23^0-x_23^post6 == 0 /\ 1+lt_19^1-lt_20^1 <= 0 /\ -x_13^post6+x_13^0 == 0 /\ -y_80^post6+y_80^0 == 0 /\ -y_110^post6+y_110^0 == 0 /\ -i_8^post6+i_8^0 == 0 /\ -y_309^post6+y_309^0 == 0 /\ -result_6^post6+result_6^0 == 0 /\ len_246^0-len_246^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ a_243^0-a_243^post6 == 0 /\ -y_259^post6+y_259^0 == 0 /\ -c_15^post6+c_15^0 == 0), cost: 1 6: l4 -> l6 : _^0'=_^post7, a_128^0'=a_128^post7, a_243^0'=a_243^post7, c_15^0'=c_15^post7, elem_16^0'=elem_16^post7, head_9^0'=head_9^post7, i_8^0'=i_8^post7, k_296^0'=k_296^post7, len_246^0'=len_246^post7, len_48^0'=len_48^post7, length_7^0'=length_7^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, prev_17^0'=prev_17^post7, result_6^0'=result_6^post7, x_13^0'=x_13^post7, x_23^0'=x_23^post7, y_110^0'=y_110^post7, y_14^0'=y_14^post7, y_158^0'=y_158^post7, y_259^0'=y_259^post7, y_309^0'=y_309^post7, y_80^0'=y_80^post7, (0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -a_243^0 <= 0 /\ lt_20^0-lt_20^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ y_110^0-y_110^post7 == 0 /\ -k_296^post7+k_296^0 == 0 /\ prev_17^0-prev_17^post7 == 0 /\ -x_23^post7+x_23^0 == 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ -elem_16^post7+elem_16^0 == 0 /\ -y_309^post7+y_309^0 == 0 /\ -y_80^post7+y_80^0 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ a_243^0-a_243^post7 == 0 /\ y_14^0-y_14^post7 == 0 /\ c_15^0-c_15^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -a_128^post7+a_128^0 == 0 /\ -c_15^0 <= 0 /\ len_48^0-len_48^post7 == 0 /\ _^0-_^post7 == 0 /\ len_246^0-len_246^post7 == 0 /\ -length_7^post7+length_7^0 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ y_158^0-y_158^post7 == 0), cost: 1 7: l4 -> l1 : _^0'=_^post8, a_128^0'=a_128^post8, a_243^0'=a_243^post8, c_15^0'=c_15^post8, elem_16^0'=elem_16^post8, head_9^0'=head_9^post8, i_8^0'=i_8^post8, k_296^0'=k_296^post8, len_246^0'=len_246^post8, len_48^0'=len_48^post8, length_7^0'=length_7^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, prev_17^0'=prev_17^post8, result_6^0'=result_6^post8, x_13^0'=x_13^post8, x_23^0'=x_23^post8, y_110^0'=y_110^post8, y_14^0'=y_14^post8, y_158^0'=y_158^post8, y_259^0'=y_259^post8, y_309^0'=y_309^post8, y_80^0'=y_80^post8, (0 == 0 /\ y_158^0-y_158^post8 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -a_128^post8+a_128^0 == 0 /\ -a_243^0 <= 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -len_48^post8+len_48^0 == 0 /\ -k_296^0 <= 0 /\ -y_259^post8+y_259^0 == 0 /\ lt_21^1-y_309^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ 1-a_243^0+a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ -k_296^post8+k_296^0 == 0 /\ y_309^0-y_309^post8 == 0 /\ -x_13^0+elem_16^post8 == 0 /\ -c_15^0+y_14^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ x_23^0-x_23^post8 == 0 /\ -lt_21^1+c_15^post8 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ _^0-_^post8 == 0 /\ -1-k_296^0+len_246^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ prev_17^post8 == 0), cost: 1 9: l7 -> l0 : _^0'=_^post4, a_128^0'=a_128^post4, a_243^0'=a_243^post4, c_15^0'=c_15^post4, elem_16^0'=elem_16^post4, head_9^0'=head_9^post4, i_8^0'=i_8^post4, k_296^0'=k_296^post4, len_246^0'=len_246^post4, len_48^0'=len_48^post4, length_7^0'=length_7^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, prev_17^0'=prev_17^post4, result_6^0'=result_6^post4, x_13^0'=x_13^post4, x_23^0'=x_23^post4, y_110^0'=y_110^post4, y_14^0'=y_14^post4, y_158^0'=y_158^post4, y_259^0'=y_259^post4, y_309^0'=y_309^post4, y_80^0'=y_80^post4, (0 == 0 /\ -y_309^post4+y_309^post9 == 0 /\ result_6^0-result_6^post9 == 0 /\ -_^post4+_^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ -prev_17^post4+prev_17^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -c_15^post4+c_15^post9 == 0 /\ -x_23^post4+x_23^post9 == 0 /\ -1-i_8^1+i_8^post4 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ x_13^1 == 0 /\ -lt_20^post4+lt_20^post9 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -len_246^post4+len_246^post9 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -y_80^post4+y_80^post9 == 0 /\ -result_6^post4+result_6^post9 == 0 /\ -a_128^post4+a_128^post9 == 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ head_9^1 == 0 /\ -x_23^post9+x_23^0 == 0 /\ -a_243^post4+a_243^post9 == 0 /\ y_14^0-y_14^post9 == 0 /\ -lt_19^post4+lt_19^post9 == 0 /\ -y_110^post4+y_110^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ x_13^post4-x_23^post9 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post4+y_259^post9 == 0 /\ -k_296^post4+k_296^post9 == 0 /\ -elem_16^post4+elem_16^post9 == 0 /\ -lt_18^post4+lt_18^post9 == 0 /\ -17+length_7^post4 == 0 /\ -y_259^post9+y_259^0 == 0 /\ -y_158^post4+y_158^post9 == 0 /\ i_8^1 == 0 /\ -c_15^post9+c_15^0 == 0 /\ -i_8^1+len_48^post4 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ -lt_21^post4+lt_21^post9 == 0 /\ -y_14^post4+y_14^post9 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0 /\ 1-length_7^post4+i_8^1 <= 0), cost: 1 Eliminating location l3 by chaining: Applied chaining First rule: l7 -> l3 : _^0'=_^post9, a_128^0'=a_128^post9, a_243^0'=a_243^post9, c_15^0'=c_15^post9, elem_16^0'=elem_16^post9, head_9^0'=head_9^post9, i_8^0'=i_8^post9, k_296^0'=k_296^post9, len_246^0'=len_246^post9, len_48^0'=len_48^post9, length_7^0'=length_7^post9, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, prev_17^0'=prev_17^post9, result_6^0'=result_6^post9, x_13^0'=x_13^post9, x_23^0'=x_23^post9, y_110^0'=y_110^post9, y_14^0'=y_14^post9, y_158^0'=y_158^post9, y_259^0'=y_259^post9, y_309^0'=y_309^post9, y_80^0'=y_80^post9, (result_6^0-result_6^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ -x_23^post9+x_23^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post9+y_259^0 == 0 /\ -c_15^post9+c_15^0 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0), cost: 1 Second rule: l3 -> l0 : _^0'=_^post4, a_128^0'=a_128^post4, a_243^0'=a_243^post4, c_15^0'=c_15^post4, elem_16^0'=elem_16^post4, head_9^0'=head_9^post4, i_8^0'=i_8^post4, k_296^0'=k_296^post4, len_246^0'=len_246^post4, len_48^0'=len_48^post4, length_7^0'=length_7^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, prev_17^0'=prev_17^post4, result_6^0'=result_6^post4, x_13^0'=x_13^post4, x_23^0'=x_23^post4, y_110^0'=y_110^post4, y_14^0'=y_14^post4, y_158^0'=y_158^post4, y_259^0'=y_259^post4, y_309^0'=y_309^post4, y_80^0'=y_80^post4, (0 == 0 /\ a_243^0-a_243^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ y_158^0-y_158^post4 == 0 /\ -x_23^post4+x_23^0 == 0 /\ result_6^0-result_6^post4 == 0 /\ -1-i_8^1+i_8^post4 == 0 /\ x_13^1 == 0 /\ -y_80^post4+y_80^0 == 0 /\ y_110^0-y_110^post4 == 0 /\ -lt_18^post4+lt_18^0 == 0 /\ prev_17^0-prev_17^post4 == 0 /\ lt_19^0-lt_19^post4 == 0 /\ len_246^0-len_246^post4 == 0 /\ -k_296^post4+k_296^0 == 0 /\ head_9^1 == 0 /\ -elem_16^post4+elem_16^0 == 0 /\ -c_15^post4+c_15^0 == 0 /\ x_13^post4-x_23^0 == 0 /\ -y_309^post4+y_309^0 == 0 /\ y_14^0-y_14^post4 == 0 /\ -y_259^post4+y_259^0 == 0 /\ -17+length_7^post4 == 0 /\ -_^post4+_^0 == 0 /\ i_8^1 == 0 /\ -i_8^1+len_48^post4 == 0 /\ -lt_20^post4+lt_20^0 == 0 /\ -a_128^post4+a_128^0 == 0 /\ 1-length_7^post4+i_8^1 <= 0), cost: 1 New rule: l7 -> l0 : _^0'=_^post4, a_128^0'=a_128^post4, a_243^0'=a_243^post4, c_15^0'=c_15^post4, elem_16^0'=elem_16^post4, head_9^0'=head_9^post4, i_8^0'=i_8^post4, k_296^0'=k_296^post4, len_246^0'=len_246^post4, len_48^0'=len_48^post4, length_7^0'=length_7^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, prev_17^0'=prev_17^post4, result_6^0'=result_6^post4, x_13^0'=x_13^post4, x_23^0'=x_23^post4, y_110^0'=y_110^post4, y_14^0'=y_14^post4, y_158^0'=y_158^post4, y_259^0'=y_259^post4, y_309^0'=y_309^post4, y_80^0'=y_80^post4, (0 == 0 /\ -y_309^post4+y_309^post9 == 0 /\ result_6^0-result_6^post9 == 0 /\ -_^post4+_^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ -prev_17^post4+prev_17^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -c_15^post4+c_15^post9 == 0 /\ -x_23^post4+x_23^post9 == 0 /\ -1-i_8^1+i_8^post4 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ x_13^1 == 0 /\ -lt_20^post4+lt_20^post9 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -len_246^post4+len_246^post9 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -y_80^post4+y_80^post9 == 0 /\ -result_6^post4+result_6^post9 == 0 /\ -a_128^post4+a_128^post9 == 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ head_9^1 == 0 /\ -x_23^post9+x_23^0 == 0 /\ -a_243^post4+a_243^post9 == 0 /\ y_14^0-y_14^post9 == 0 /\ -lt_19^post4+lt_19^post9 == 0 /\ -y_110^post4+y_110^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ x_13^post4-x_23^post9 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post4+y_259^post9 == 0 /\ -k_296^post4+k_296^post9 == 0 /\ -elem_16^post4+elem_16^post9 == 0 /\ -lt_18^post4+lt_18^post9 == 0 /\ -17+length_7^post4 == 0 /\ -y_259^post9+y_259^0 == 0 /\ -y_158^post4+y_158^post9 == 0 /\ i_8^1 == 0 /\ -c_15^post9+c_15^0 == 0 /\ -i_8^1+len_48^post4 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ -lt_21^post4+lt_21^post9 == 0 /\ -y_14^post4+y_14^post9 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0 /\ 1-length_7^post4+i_8^1 <= 0), cost: 1 Applied deletion Removed the following rules: 3 8 Eliminating location l2 by chaining: Applied chaining First rule: l0 -> l2 : _^0'=_^post2, a_128^0'=a_128^post2, a_243^0'=a_243^post2, c_15^0'=c_15^post2, elem_16^0'=elem_16^post2, head_9^0'=head_9^post2, i_8^0'=i_8^post2, k_296^0'=k_296^post2, len_246^0'=len_246^post2, len_48^0'=len_48^post2, length_7^0'=length_7^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, prev_17^0'=prev_17^post2, result_6^0'=result_6^post2, x_13^0'=x_13^post2, x_23^0'=x_23^post2, y_110^0'=y_110^post2, y_14^0'=y_14^post2, y_158^0'=y_158^post2, y_259^0'=y_259^post2, y_309^0'=y_309^post2, y_80^0'=y_80^post2, (0 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ a_243^0-a_243^post2 == 0 /\ -len_48^0 <= 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ result_6^0-result_6^post2 == 0), cost: 1 Second rule: l2 -> l0 : _^0'=_^post3, a_128^0'=a_128^post3, a_243^0'=a_243^post3, c_15^0'=c_15^post3, elem_16^0'=elem_16^post3, head_9^0'=head_9^post3, i_8^0'=i_8^post3, k_296^0'=k_296^post3, len_246^0'=len_246^post3, len_48^0'=len_48^post3, length_7^0'=length_7^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, prev_17^0'=prev_17^post3, result_6^0'=result_6^post3, x_13^0'=x_13^post3, x_23^0'=x_23^post3, y_110^0'=y_110^post3, y_14^0'=y_14^post3, y_158^0'=y_158^post3, y_259^0'=y_259^post3, y_309^0'=y_309^post3, y_80^0'=y_80^post3, (-y_80^post3+y_80^0 == 0 /\ -i_8^post3+i_8^0 == 0 /\ -head_9^post3+head_9^0 == 0 /\ -a_128^post3+a_128^0 == 0 /\ length_7^0-length_7^post3 == 0 /\ y_309^0-y_309^post3 == 0 /\ -prev_17^post3+prev_17^0 == 0 /\ y_14^0-y_14^post3 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ -lt_20^post3+lt_20^0 == 0 /\ k_296^0-k_296^post3 == 0 /\ -lt_19^post3+lt_19^0 == 0 /\ -c_15^post3+c_15^0 == 0 /\ -y_110^post3+y_110^0 == 0 /\ -y_259^post3+y_259^0 == 0 /\ y_158^0-y_158^post3 == 0 /\ a_243^0-a_243^post3 == 0 /\ -len_48^post3+len_48^0 == 0 /\ -x_23^post3+x_23^0 == 0 /\ -len_246^post3+len_246^0 == 0 /\ result_6^0-result_6^post3 == 0 /\ x_13^0-x_13^post3 == 0 /\ -lt_18^post3+lt_18^0 == 0 /\ _^0-_^post3 == 0 /\ -elem_16^post3+elem_16^0 == 0), cost: 1 New rule: l0 -> l0 : _^0'=_^post3, a_128^0'=a_128^post3, a_243^0'=a_243^post3, c_15^0'=c_15^post3, elem_16^0'=elem_16^post3, head_9^0'=head_9^post3, i_8^0'=i_8^post3, k_296^0'=k_296^post3, len_246^0'=len_246^post3, len_48^0'=len_48^post3, length_7^0'=length_7^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, prev_17^0'=prev_17^post3, result_6^0'=result_6^post3, x_13^0'=x_13^post3, x_23^0'=x_23^post3, y_110^0'=y_110^post3, y_14^0'=y_14^post3, y_158^0'=y_158^post3, y_259^0'=y_259^post3, y_309^0'=y_309^post3, y_80^0'=y_80^post3, (0 == 0 /\ prev_17^post2-prev_17^post3 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ head_9^post2-head_9^post3 == 0 /\ -c_15^post3+c_15^post2 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ y_309^post2-y_309^post3 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ lt_21^post2-lt_21^post3 == 0 /\ y_80^post2-y_80^post3 == 0 /\ a_243^0-a_243^post2 == 0 /\ result_6^post2-result_6^post3 == 0 /\ y_158^post2-y_158^post3 == 0 /\ -len_48^0 <= 0 /\ length_7^post2-length_7^post3 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ lt_19^post2-lt_19^post3 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ k_296^post2-k_296^post3 == 0 /\ -elem_16^post3+elem_16^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ x_23^post2-x_23^post3 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_18^post3+lt_18^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ len_48^post2-len_48^post3 == 0 /\ -len_246^post3+len_246^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ y_110^post2-y_110^post3 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ lt_20^post2-lt_20^post3 == 0 /\ -a_128^post3+a_128^post2 == 0 /\ y_14^post2-y_14^post3 == 0 /\ i_8^post2-i_8^post3 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ a_243^post2-a_243^post3 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ -_^post3+_^post2 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ x_13^post2-x_13^post3 == 0 /\ y_259^post2-y_259^post3 == 0 /\ result_6^0-result_6^post2 == 0), cost: 1 Applied deletion Removed the following rules: 1 2 Simplified Transitions Start location: l7 Program variables: _^0 a_128^0 a_243^0 c_15^0 elem_16^0 head_9^0 i_8^0 k_296^0 len_246^0 len_48^0 length_7^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 prev_17^0 result_6^0 x_13^0 x_23^0 y_110^0 y_14^0 y_158^0 y_259^0 y_309^0 y_80^0 11: l0 -> l1 : a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, len_246^0'=1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, y_14^0'=y_110^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 17: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=1+i_8^0, len_48^0'=1+len_48^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 12: l1 -> l4 : k_296^0'=len_246^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, x_13^0'=y_14^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 13: l1 -> l5 : elem_16^0'=y_259^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, prev_17^0'=elem_16^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 14: l4 -> l6 : result_6^0'=result_6^post7, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 15: l4 -> l1 : a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, len_246^0'=1+k_296^0, lt_21^0'=lt_21^post8, prev_17^0'=0, y_14^0'=c_15^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 16: l7 -> l0 : head_9^0'=head_9^post4, i_8^0'=1, len_48^0'=0, length_7^0'=17, x_13^0'=x_23^0, T, cost: 1 made implied equalities explicit Original rule: l0 -> l1 : _^0'=_^post1, a_128^0'=a_128^post1, a_243^0'=a_243^post1, c_15^0'=c_15^post1, elem_16^0'=elem_16^post1, head_9^0'=head_9^post1, i_8^0'=i_8^post1, k_296^0'=k_296^post1, len_246^0'=len_246^post1, len_48^0'=len_48^post1, length_7^0'=length_7^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=prev_17^post1, result_6^0'=result_6^post1, x_13^0'=x_13^post1, x_23^0'=x_23^post1, y_110^0'=y_110^post1, y_14^0'=y_14^post1, y_158^0'=y_158^post1, y_259^0'=y_259^post1, y_309^0'=y_309^post1, y_80^0'=y_80^post1, (0 == 0 /\ 1-a_128^post1-_^0+a_243^post1 == 0 /\ -y_80^post1+y_80^0 == 0 /\ -a_128^post1 <= 0 /\ _^0-_^post1 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ x_13^1-result_6^post1 == 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -y_259^post1+y_259^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ -y_14^2+x_13^post1 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ y_158^0-y_158^post1 == 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ c_15^post1-lt_21^5 == 0 /\ 2+a_128^post1-len_48^0 == 0 /\ -k_296^post1+k_296^0 == 0 /\ prev_17^post1 == 0 /\ result_6^post1-head_9^0 == 0 /\ y_110^0-y_110^post1 == 0 /\ -elem_16^1 <= 0 /\ y_14^post1-c_15^3 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -1+len_246^post1 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^3+c_15^3 == 0 /\ -x_23^post1+x_23^0 == 0 /\ -x_13^post1+elem_16^post1 == 0 /\ length_7^0-i_8^0 <= 0 /\ -i_8^post1+i_8^0 == 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_13^2 == 0 /\ -head_9^post1+head_9^0 == 0 /\ -len_48^post1+len_48^0 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 New rule: l0 -> l1 : _^0'=_^post1, a_128^0'=a_128^post1, a_243^0'=a_243^post1, c_15^0'=c_15^post1, elem_16^0'=elem_16^post1, head_9^0'=head_9^post1, i_8^0'=i_8^post1, k_296^0'=k_296^post1, len_246^0'=len_246^post1, len_48^0'=len_48^post1, length_7^0'=length_7^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=prev_17^post1, result_6^0'=result_6^post1, x_13^0'=x_13^post1, x_23^0'=x_23^post1, y_110^0'=y_110^post1, y_14^0'=y_14^post1, y_158^0'=y_158^post1, y_259^0'=y_259^post1, y_309^0'=y_309^post1, y_80^0'=y_80^post1, (0 == 0 /\ 1-a_128^post1-_^0+a_243^post1 == 0 /\ -y_80^post1+y_80^0 == 0 /\ -a_128^post1 <= 0 /\ _^0-_^post1 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ x_13^1-result_6^post1 == 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -y_259^post1+y_259^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ -y_14^2+x_13^post1 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ y_158^0-y_158^post1 == 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ c_15^post1-lt_21^5 == 0 /\ 2+a_128^post1-len_48^0 == 0 /\ -k_296^post1+k_296^0 == 0 /\ prev_17^post1 == 0 /\ result_6^post1-head_9^0 == 0 /\ y_110^0-y_110^post1 == 0 /\ -elem_16^1 <= 0 /\ -elem_16^1 == 0 /\ y_14^post1-c_15^3 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -1+len_246^post1 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^3+c_15^3 == 0 /\ -x_23^post1+x_23^0 == 0 /\ -x_13^post1+elem_16^post1 == 0 /\ length_7^0-i_8^0 <= 0 /\ -i_8^post1+i_8^0 == 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -prev_17^2 == 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_13^2 == 0 /\ -head_9^post1+head_9^0 == 0 /\ -len_48^post1+len_48^0 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : _^0'=_^post1, a_128^0'=a_128^post1, a_243^0'=a_243^post1, c_15^0'=c_15^post1, elem_16^0'=elem_16^post1, head_9^0'=head_9^post1, i_8^0'=i_8^post1, k_296^0'=k_296^post1, len_246^0'=len_246^post1, len_48^0'=len_48^post1, length_7^0'=length_7^post1, lt_18^0'=lt_18^post1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=prev_17^post1, result_6^0'=result_6^post1, x_13^0'=x_13^post1, x_23^0'=x_23^post1, y_110^0'=y_110^post1, y_14^0'=y_14^post1, y_158^0'=y_158^post1, y_259^0'=y_259^post1, y_309^0'=y_309^post1, y_80^0'=y_80^post1, (0 == 0 /\ 1-a_128^post1-_^0+a_243^post1 == 0 /\ -y_80^post1+y_80^0 == 0 /\ -a_128^post1 <= 0 /\ _^0-_^post1 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ x_13^1-result_6^post1 == 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -y_259^post1+y_259^0 == 0 /\ y_309^0-y_309^post1 == 0 /\ -y_14^2+x_13^post1 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ y_158^0-y_158^post1 == 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ c_15^post1-lt_21^5 == 0 /\ 2+a_128^post1-len_48^0 == 0 /\ -k_296^post1+k_296^0 == 0 /\ prev_17^post1 == 0 /\ result_6^post1-head_9^0 == 0 /\ y_110^0-y_110^post1 == 0 /\ -elem_16^1 <= 0 /\ -elem_16^1 == 0 /\ y_14^post1-c_15^3 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -1+len_246^post1 == 0 /\ length_7^0-length_7^post1 == 0 /\ -lt_21^3+c_15^3 == 0 /\ -x_23^post1+x_23^0 == 0 /\ -x_13^post1+elem_16^post1 == 0 /\ length_7^0-i_8^0 <= 0 /\ -i_8^post1+i_8^0 == 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -prev_17^2 == 0 /\ -lt_18^post1+lt_18^0 == 0 /\ x_13^2 == 0 /\ -head_9^post1+head_9^0 == 0 /\ -len_48^post1+len_48^0 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 New rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=lt_21^5, elem_16^0'=y_14^2, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=x_13^1, x_13^0'=y_14^2, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^3, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ 2-len_48^0 <= 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ x_13^1-head_9^0 == 0 /\ -elem_16^1 <= 0 /\ -elem_16^1 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -lt_21^3+c_15^3 == 0 /\ length_7^0-i_8^0 <= 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -prev_17^2 == 0 /\ x_13^2 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 propagated equality a_128^post1 = 1-_^0+a_243^post1 propagated equality y_80^post1 = y_80^0 propagated equality _^post1 = _^0 propagated equality result_6^post1 = x_13^1 propagated equality y_259^post1 = y_259^0 propagated equality y_309^post1 = y_309^0 propagated equality x_13^post1 = y_14^2 propagated equality y_158^post1 = y_158^0 propagated equality c_15^post1 = lt_21^5 propagated equality a_243^post1 = -3+_^0+len_48^0 propagated equality k_296^post1 = k_296^0 propagated equality prev_17^post1 = 0 propagated equality y_110^post1 = y_110^0 propagated equality y_14^post1 = c_15^3 propagated equality len_246^post1 = 1 propagated equality length_7^post1 = length_7^0 propagated equality x_23^post1 = x_23^0 propagated equality elem_16^post1 = y_14^2 propagated equality i_8^post1 = i_8^0 propagated equality lt_18^post1 = lt_18^0 propagated equality head_9^post1 = head_9^0 propagated equality len_48^post1 = len_48^0 Propagated Equalities Original rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=lt_21^5, elem_16^0'=y_14^2, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=x_13^1, x_13^0'=y_14^2, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^3, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ prev_17^1 <= 0 /\ prev_17^1 == 0 /\ 2-len_48^0 <= 0 /\ lt_21^1-y_80^0 == 0 /\ -y_158^0+lt_21^5 == 0 /\ -prev_17^1 <= 0 /\ lt_21^3-y_110^0 == 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ -y_14^1+x_13^3 == 0 /\ y_14^2-c_15^2 == 0 /\ x_13^1-head_9^0 == 0 /\ -elem_16^1 <= 0 /\ -elem_16^1 == 0 /\ -x_13^3+elem_16^2 == 0 /\ -lt_21^3+c_15^3 == 0 /\ length_7^0-i_8^0 <= 0 /\ c_15^2-lt_21^1 == 0 /\ elem_16^1 <= 0 /\ -prev_17^2 <= 0 /\ -prev_17^2 == 0 /\ x_13^2 == 0 /\ prev_17^2 <= 0 /\ prev_17^2 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -x_13^1+c_15^1 == 0 /\ y_14^1-c_15^1 == 0 /\ elem_16^1-x_13^2 == 0), cost: 1 New rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 <= 0 /\ 0 == 0 /\ 2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 propagated equality prev_17^1 = 0 propagated equality lt_21^1 = y_80^0 propagated equality lt_21^5 = y_158^0 propagated equality lt_21^3 = y_110^0 propagated equality x_13^3 = y_14^1 propagated equality c_15^2 = y_14^2 propagated equality x_13^1 = head_9^0 propagated equality elem_16^1 = 0 propagated equality elem_16^2 = y_14^1 propagated equality c_15^3 = y_110^0 propagated equality y_14^2 = y_80^0 propagated equality prev_17^2 = 0 propagated equality x_13^2 = 0 propagated equality c_15^1 = head_9^0 propagated equality y_14^1 = head_9^0 Simplified Guard Original rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 <= 0 /\ 0 == 0 /\ 2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 New rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 New rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : _^0'=_^0, a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_110^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 New rule: l0 -> l1 : a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, len_246^0'=1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, y_14^0'=y_110^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 made implied equalities explicit Original rule: l1 -> l4 : _^0'=_^post5, a_128^0'=a_128^post5, a_243^0'=a_243^post5, c_15^0'=c_15^post5, elem_16^0'=elem_16^post5, head_9^0'=head_9^post5, i_8^0'=i_8^post5, k_296^0'=k_296^post5, len_246^0'=len_246^post5, len_48^0'=len_48^post5, length_7^0'=length_7^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, prev_17^0'=prev_17^post5, result_6^0'=result_6^post5, x_13^0'=x_13^post5, x_23^0'=x_23^post5, y_110^0'=y_110^post5, y_14^0'=y_14^post5, y_158^0'=y_158^post5, y_259^0'=y_259^post5, y_309^0'=y_309^post5, y_80^0'=y_80^post5, (0 == 0 /\ _^0-_^post5 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -len_48^post5+len_48^0 == 0 /\ -lt_18^post5+lt_18^0 == 0 /\ y_14^0-y_14^post5 == 0 /\ x_23^0-x_23^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ -y_14^0+x_13^post5 == 0 /\ -y_110^post5+y_110^0 == 0 /\ result_6^0-result_6^post5 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ a_243^0-a_243^post5 == 0 /\ -head_9^post5+head_9^0 == 0 /\ length_7^0-length_7^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -a_128^post5+a_128^0 == 0 /\ -y_309^post5+y_309^0 == 0 /\ -len_246^0+k_296^post5 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ y_259^0-y_259^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -y_80^post5+y_80^0 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -elem_16^post5+elem_16^0 == 0 /\ -prev_17^post5+prev_17^0 == 0), cost: 1 New rule: l1 -> l4 : _^0'=_^post5, a_128^0'=a_128^post5, a_243^0'=a_243^post5, c_15^0'=c_15^post5, elem_16^0'=elem_16^post5, head_9^0'=head_9^post5, i_8^0'=i_8^post5, k_296^0'=k_296^post5, len_246^0'=len_246^post5, len_48^0'=len_48^post5, length_7^0'=length_7^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, prev_17^0'=prev_17^post5, result_6^0'=result_6^post5, x_13^0'=x_13^post5, x_23^0'=x_23^post5, y_110^0'=y_110^post5, y_14^0'=y_14^post5, y_158^0'=y_158^post5, y_259^0'=y_259^post5, y_309^0'=y_309^post5, y_80^0'=y_80^post5, (0 == 0 /\ _^0-_^post5 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ -len_48^post5+len_48^0 == 0 /\ -lt_18^post5+lt_18^0 == 0 /\ y_14^0-y_14^post5 == 0 /\ x_23^0-x_23^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ -y_14^0+x_13^post5 == 0 /\ -y_110^post5+y_110^0 == 0 /\ result_6^0-result_6^post5 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ a_243^0-a_243^post5 == 0 /\ -head_9^post5+head_9^0 == 0 /\ length_7^0-length_7^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -a_128^post5+a_128^0 == 0 /\ -y_309^post5+y_309^0 == 0 /\ -len_246^0+k_296^post5 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ y_259^0-y_259^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -y_80^post5+y_80^0 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -elem_16^post5+elem_16^0 == 0 /\ -prev_17^post5+prev_17^0 == 0), cost: 1 Propagated Equalities Original rule: l1 -> l4 : _^0'=_^post5, a_128^0'=a_128^post5, a_243^0'=a_243^post5, c_15^0'=c_15^post5, elem_16^0'=elem_16^post5, head_9^0'=head_9^post5, i_8^0'=i_8^post5, k_296^0'=k_296^post5, len_246^0'=len_246^post5, len_48^0'=len_48^post5, length_7^0'=length_7^post5, lt_18^0'=lt_18^post5, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^post5, prev_17^0'=prev_17^post5, result_6^0'=result_6^post5, x_13^0'=x_13^post5, x_23^0'=x_23^post5, y_110^0'=y_110^post5, y_14^0'=y_14^post5, y_158^0'=y_158^post5, y_259^0'=y_259^post5, y_309^0'=y_309^post5, y_80^0'=y_80^post5, (0 == 0 /\ _^0-_^post5 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ -len_48^post5+len_48^0 == 0 /\ -lt_18^post5+lt_18^0 == 0 /\ y_14^0-y_14^post5 == 0 /\ x_23^0-x_23^post5 == 0 /\ -i_8^post5+i_8^0 == 0 /\ -y_14^0+x_13^post5 == 0 /\ -y_110^post5+y_110^0 == 0 /\ result_6^0-result_6^post5 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ a_243^0-a_243^post5 == 0 /\ -head_9^post5+head_9^0 == 0 /\ length_7^0-length_7^post5 == 0 /\ y_158^0-y_158^post5 == 0 /\ c_15^0-c_15^post5 == 0 /\ -a_128^post5+a_128^0 == 0 /\ -y_309^post5+y_309^0 == 0 /\ -len_246^0+k_296^post5 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ y_259^0-y_259^post5 == 0 /\ len_246^0-len_246^post5 == 0 /\ -y_80^post5+y_80^0 == 0 /\ -lt_19^1+lt_20^1 <= 0 /\ -elem_16^post5+elem_16^0 == 0 /\ -prev_17^post5+prev_17^0 == 0), cost: 1 New rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 propagated equality _^post5 = _^0 propagated equality len_48^post5 = len_48^0 propagated equality lt_18^post5 = lt_18^0 propagated equality y_14^post5 = y_14^0 propagated equality x_23^post5 = x_23^0 propagated equality i_8^post5 = i_8^0 propagated equality x_13^post5 = y_14^0 propagated equality y_110^post5 = y_110^0 propagated equality result_6^post5 = result_6^0 propagated equality a_243^post5 = a_243^0 propagated equality head_9^post5 = head_9^0 propagated equality length_7^post5 = length_7^0 propagated equality y_158^post5 = y_158^0 propagated equality c_15^post5 = c_15^0 propagated equality a_128^post5 = a_128^0 propagated equality y_309^post5 = y_309^0 propagated equality k_296^post5 = len_246^0 propagated equality lt_21^post5 = lt_21^0 propagated equality y_259^post5 = y_259^0 propagated equality len_246^post5 = len_246^0 propagated equality y_80^post5 = y_80^0 propagated equality elem_16^post5 = elem_16^0 propagated equality prev_17^post5 = prev_17^0 Simplified Guard Original rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 New rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -lt_19^1+lt_20^1 <= 0), cost: 1 New rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 made implied equalities explicit Original rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 New rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=len_246^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=y_14^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 New rule: l1 -> l4 : k_296^0'=len_246^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, x_13^0'=y_14^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l5 : _^0'=_^post6, a_128^0'=a_128^post6, a_243^0'=a_243^post6, c_15^0'=c_15^post6, elem_16^0'=elem_16^post6, head_9^0'=head_9^post6, i_8^0'=i_8^post6, k_296^0'=k_296^post6, len_246^0'=len_246^post6, len_48^0'=len_48^post6, length_7^0'=length_7^post6, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^post6, prev_17^0'=prev_17^post6, result_6^0'=result_6^post6, x_13^0'=x_13^post6, x_23^0'=x_23^post6, y_110^0'=y_110^post6, y_14^0'=y_14^post6, y_158^0'=y_158^post6, y_259^0'=y_259^post6, y_309^0'=y_309^post6, y_80^0'=y_80^post6, (0 == 0 /\ -head_9^post6+head_9^0 == 0 /\ -a_243^0 <= 0 /\ y_14^0-y_14^post6 == 0 /\ elem_16^post6-lt_18^1 == 0 /\ -len_48^post6+len_48^0 == 0 /\ y_158^0-y_158^post6 == 0 /\ prev_17^post6-elem_16^0 == 0 /\ -a_128^post6+a_128^0 == 0 /\ -_^post6+_^0 == 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ length_7^0-length_7^post6 == 0 /\ -k_296^post6+k_296^0 == 0 /\ -y_259^0+lt_18^1 == 0 /\ x_23^0-x_23^post6 == 0 /\ 1+lt_19^1-lt_20^1 <= 0 /\ -x_13^post6+x_13^0 == 0 /\ -y_80^post6+y_80^0 == 0 /\ -y_110^post6+y_110^0 == 0 /\ -i_8^post6+i_8^0 == 0 /\ -y_309^post6+y_309^0 == 0 /\ -result_6^post6+result_6^0 == 0 /\ len_246^0-len_246^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ a_243^0-a_243^post6 == 0 /\ -y_259^post6+y_259^0 == 0 /\ -c_15^post6+c_15^0 == 0), cost: 1 New rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=lt_18^1, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ -y_259^0+lt_18^1 == 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 propagated equality head_9^post6 = head_9^0 propagated equality y_14^post6 = y_14^0 propagated equality elem_16^post6 = lt_18^1 propagated equality len_48^post6 = len_48^0 propagated equality y_158^post6 = y_158^0 propagated equality prev_17^post6 = elem_16^0 propagated equality a_128^post6 = a_128^0 propagated equality _^post6 = _^0 propagated equality length_7^post6 = length_7^0 propagated equality k_296^post6 = k_296^0 propagated equality x_23^post6 = x_23^0 propagated equality x_13^post6 = x_13^0 propagated equality y_80^post6 = y_80^0 propagated equality y_110^post6 = y_110^0 propagated equality i_8^post6 = i_8^0 propagated equality y_309^post6 = y_309^0 propagated equality result_6^post6 = result_6^0 propagated equality len_246^post6 = len_246^0 propagated equality lt_21^post6 = lt_21^0 propagated equality a_243^post6 = a_243^0 propagated equality y_259^post6 = y_259^0 propagated equality c_15^post6 = c_15^0 Propagated Equalities Original rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=lt_18^1, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ -y_259^0+lt_18^1 == 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 New rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 propagated equality lt_18^1 = y_259^0 Simplified Guard Original rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 New rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0 /\ 1+lt_19^1-lt_20^1 <= 0), cost: 1 New rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=y_259^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, lt_21^0'=lt_21^0, prev_17^0'=elem_16^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 New rule: l1 -> l5 : elem_16^0'=y_259^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, prev_17^0'=elem_16^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l6 : _^0'=_^post7, a_128^0'=a_128^post7, a_243^0'=a_243^post7, c_15^0'=c_15^post7, elem_16^0'=elem_16^post7, head_9^0'=head_9^post7, i_8^0'=i_8^post7, k_296^0'=k_296^post7, len_246^0'=len_246^post7, len_48^0'=len_48^post7, length_7^0'=length_7^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, prev_17^0'=prev_17^post7, result_6^0'=result_6^post7, x_13^0'=x_13^post7, x_23^0'=x_23^post7, y_110^0'=y_110^post7, y_14^0'=y_14^post7, y_158^0'=y_158^post7, y_259^0'=y_259^post7, y_309^0'=y_309^post7, y_80^0'=y_80^post7, (0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -a_243^0 <= 0 /\ lt_20^0-lt_20^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ y_110^0-y_110^post7 == 0 /\ -k_296^post7+k_296^0 == 0 /\ prev_17^0-prev_17^post7 == 0 /\ -x_23^post7+x_23^0 == 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ -elem_16^post7+elem_16^0 == 0 /\ -y_309^post7+y_309^0 == 0 /\ -y_80^post7+y_80^0 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ a_243^0-a_243^post7 == 0 /\ y_14^0-y_14^post7 == 0 /\ c_15^0-c_15^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -a_128^post7+a_128^0 == 0 /\ -c_15^0 <= 0 /\ len_48^0-len_48^post7 == 0 /\ _^0-_^post7 == 0 /\ len_246^0-len_246^post7 == 0 /\ -length_7^post7+length_7^0 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ y_158^0-y_158^post7 == 0), cost: 1 New rule: l4 -> l6 : _^0'=_^post7, a_128^0'=a_128^post7, a_243^0'=a_243^post7, c_15^0'=c_15^post7, elem_16^0'=elem_16^post7, head_9^0'=head_9^post7, i_8^0'=i_8^post7, k_296^0'=k_296^post7, len_246^0'=len_246^post7, len_48^0'=len_48^post7, length_7^0'=length_7^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, prev_17^0'=prev_17^post7, result_6^0'=result_6^post7, x_13^0'=x_13^post7, x_23^0'=x_23^post7, y_110^0'=y_110^post7, y_14^0'=y_14^post7, y_158^0'=y_158^post7, y_259^0'=y_259^post7, y_309^0'=y_309^post7, y_80^0'=y_80^post7, (0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -a_243^0 <= 0 /\ lt_20^0-lt_20^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ y_110^0-y_110^post7 == 0 /\ -k_296^post7+k_296^0 == 0 /\ prev_17^0-prev_17^post7 == 0 /\ -x_23^post7+x_23^0 == 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -elem_16^post7+elem_16^0 == 0 /\ -y_309^post7+y_309^0 == 0 /\ -y_80^post7+y_80^0 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ a_243^0-a_243^post7 == 0 /\ y_14^0-y_14^post7 == 0 /\ c_15^0-c_15^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -a_128^post7+a_128^0 == 0 /\ -c_15^0 <= 0 /\ len_48^0-len_48^post7 == 0 /\ _^0-_^post7 == 0 /\ len_246^0-len_246^post7 == 0 /\ -length_7^post7+length_7^0 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ y_158^0-y_158^post7 == 0), cost: 1 Propagated Equalities Original rule: l4 -> l6 : _^0'=_^post7, a_128^0'=a_128^post7, a_243^0'=a_243^post7, c_15^0'=c_15^post7, elem_16^0'=elem_16^post7, head_9^0'=head_9^post7, i_8^0'=i_8^post7, k_296^0'=k_296^post7, len_246^0'=len_246^post7, len_48^0'=len_48^post7, length_7^0'=length_7^post7, lt_18^0'=lt_18^post7, lt_19^0'=lt_19^post7, lt_20^0'=lt_20^post7, lt_21^0'=lt_21^post7, prev_17^0'=prev_17^post7, result_6^0'=result_6^post7, x_13^0'=x_13^post7, x_23^0'=x_23^post7, y_110^0'=y_110^post7, y_14^0'=y_14^post7, y_158^0'=y_158^post7, y_259^0'=y_259^post7, y_309^0'=y_309^post7, y_80^0'=y_80^post7, (0 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -a_243^0 <= 0 /\ lt_20^0-lt_20^post7 == 0 /\ -head_9^post7+head_9^0 == 0 /\ y_110^0-y_110^post7 == 0 /\ -k_296^post7+k_296^0 == 0 /\ prev_17^0-prev_17^post7 == 0 /\ -x_23^post7+x_23^0 == 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -elem_16^post7+elem_16^0 == 0 /\ -y_309^post7+y_309^0 == 0 /\ -y_80^post7+y_80^0 == 0 /\ lt_19^0-lt_19^post7 == 0 /\ a_243^0-a_243^post7 == 0 /\ y_14^0-y_14^post7 == 0 /\ c_15^0-c_15^post7 == 0 /\ -lt_18^post7+lt_18^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -a_128^post7+a_128^0 == 0 /\ -c_15^0 <= 0 /\ len_48^0-len_48^post7 == 0 /\ _^0-_^post7 == 0 /\ len_246^0-len_246^post7 == 0 /\ -length_7^post7+length_7^0 == 0 /\ -y_259^post7+y_259^0 == 0 /\ -i_8^post7+i_8^0 == 0 /\ y_158^0-y_158^post7 == 0), cost: 1 New rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 propagated equality lt_21^post7 = lt_21^0 propagated equality lt_20^post7 = lt_20^0 propagated equality head_9^post7 = head_9^0 propagated equality y_110^post7 = y_110^0 propagated equality k_296^post7 = k_296^0 propagated equality prev_17^post7 = prev_17^0 propagated equality x_23^post7 = x_23^0 propagated equality elem_16^post7 = elem_16^0 propagated equality y_309^post7 = y_309^0 propagated equality y_80^post7 = y_80^0 propagated equality lt_19^post7 = lt_19^0 propagated equality a_243^post7 = a_243^0 propagated equality y_14^post7 = y_14^0 propagated equality c_15^post7 = c_15^0 propagated equality lt_18^post7 = lt_18^0 propagated equality x_13^post7 = x_13^0 propagated equality a_128^post7 = a_128^0 propagated equality len_48^post7 = len_48^0 propagated equality _^post7 = _^0 propagated equality len_246^post7 = len_246^0 propagated equality length_7^post7 = length_7^0 propagated equality y_259^post7 = y_259^0 propagated equality i_8^post7 = i_8^0 propagated equality y_158^post7 = y_158^0 Simplified Guard Original rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 New rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 New rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l6 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^post7, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 New rule: l4 -> l6 : result_6^0'=result_6^post7, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l1 : _^0'=_^post8, a_128^0'=a_128^post8, a_243^0'=a_243^post8, c_15^0'=c_15^post8, elem_16^0'=elem_16^post8, head_9^0'=head_9^post8, i_8^0'=i_8^post8, k_296^0'=k_296^post8, len_246^0'=len_246^post8, len_48^0'=len_48^post8, length_7^0'=length_7^post8, lt_18^0'=lt_18^post8, lt_19^0'=lt_19^post8, lt_20^0'=lt_20^post8, lt_21^0'=lt_21^post8, prev_17^0'=prev_17^post8, result_6^0'=result_6^post8, x_13^0'=x_13^post8, x_23^0'=x_23^post8, y_110^0'=y_110^post8, y_14^0'=y_14^post8, y_158^0'=y_158^post8, y_259^0'=y_259^post8, y_309^0'=y_309^post8, y_80^0'=y_80^post8, (0 == 0 /\ y_158^0-y_158^post8 == 0 /\ -lt_18^post8+lt_18^0 == 0 /\ -a_128^post8+a_128^0 == 0 /\ -a_243^0 <= 0 /\ -lt_19^post8+lt_19^0 == 0 /\ -len_48^post8+len_48^0 == 0 /\ -k_296^0 <= 0 /\ -y_259^post8+y_259^0 == 0 /\ lt_21^1-y_309^0 == 0 /\ -i_8^post8+i_8^0 == 0 /\ 1-a_243^0+a_243^post8 == 0 /\ length_7^0-length_7^post8 == 0 /\ -k_296^post8+k_296^0 == 0 /\ y_309^0-y_309^post8 == 0 /\ -x_13^0+elem_16^post8 == 0 /\ -c_15^0+y_14^post8 == 0 /\ -head_9^post8+head_9^0 == 0 /\ -lt_20^post8+lt_20^0 == 0 /\ x_23^0-x_23^post8 == 0 /\ -lt_21^1+c_15^post8 == 0 /\ -x_13^post8+x_13^0 == 0 /\ y_80^0-y_80^post8 == 0 /\ -y_110^post8+y_110^0 == 0 /\ _^0-_^post8 == 0 /\ -1-k_296^0+len_246^post8 == 0 /\ -result_6^post8+result_6^0 == 0 /\ prev_17^post8 == 0), cost: 1 New rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=lt_21^1, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0 /\ lt_21^1-y_309^0 == 0), cost: 1 propagated equality y_158^post8 = y_158^0 propagated equality lt_18^post8 = lt_18^0 propagated equality a_128^post8 = a_128^0 propagated equality lt_19^post8 = lt_19^0 propagated equality len_48^post8 = len_48^0 propagated equality y_259^post8 = y_259^0 propagated equality i_8^post8 = i_8^0 propagated equality a_243^post8 = -1+a_243^0 propagated equality length_7^post8 = length_7^0 propagated equality k_296^post8 = k_296^0 propagated equality y_309^post8 = y_309^0 propagated equality elem_16^post8 = x_13^0 propagated equality y_14^post8 = c_15^0 propagated equality head_9^post8 = head_9^0 propagated equality lt_20^post8 = lt_20^0 propagated equality x_23^post8 = x_23^0 propagated equality c_15^post8 = lt_21^1 propagated equality x_13^post8 = x_13^0 propagated equality y_80^post8 = y_80^0 propagated equality y_110^post8 = y_110^0 propagated equality _^post8 = _^0 propagated equality len_246^post8 = 1+k_296^0 propagated equality result_6^post8 = result_6^0 propagated equality prev_17^post8 = 0 Propagated Equalities Original rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=lt_21^1, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0 /\ lt_21^1-y_309^0 == 0), cost: 1 New rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 propagated equality lt_21^1 = y_309^0 Simplified Guard Original rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 New rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l1 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, head_9^0'=head_9^0, i_8^0'=i_8^0, k_296^0'=k_296^0, len_246^0'=1+k_296^0, len_48^0'=len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^post8, prev_17^0'=0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=c_15^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 New rule: l4 -> l1 : a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, len_246^0'=1+k_296^0, lt_21^0'=lt_21^post8, prev_17^0'=0, y_14^0'=c_15^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 Propagated Equalities Original rule: l7 -> l0 : _^0'=_^post4, a_128^0'=a_128^post4, a_243^0'=a_243^post4, c_15^0'=c_15^post4, elem_16^0'=elem_16^post4, head_9^0'=head_9^post4, i_8^0'=i_8^post4, k_296^0'=k_296^post4, len_246^0'=len_246^post4, len_48^0'=len_48^post4, length_7^0'=length_7^post4, lt_18^0'=lt_18^post4, lt_19^0'=lt_19^post4, lt_20^0'=lt_20^post4, lt_21^0'=lt_21^post4, prev_17^0'=prev_17^post4, result_6^0'=result_6^post4, x_13^0'=x_13^post4, x_23^0'=x_23^post4, y_110^0'=y_110^post4, y_14^0'=y_14^post4, y_158^0'=y_158^post4, y_259^0'=y_259^post4, y_309^0'=y_309^post4, y_80^0'=y_80^post4, (0 == 0 /\ -y_309^post4+y_309^post9 == 0 /\ result_6^0-result_6^post9 == 0 /\ -_^post4+_^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ -prev_17^post4+prev_17^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -c_15^post4+c_15^post9 == 0 /\ -x_23^post4+x_23^post9 == 0 /\ -1-i_8^1+i_8^post4 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ x_13^1 == 0 /\ -lt_20^post4+lt_20^post9 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -len_246^post4+len_246^post9 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -y_80^post4+y_80^post9 == 0 /\ -result_6^post4+result_6^post9 == 0 /\ -a_128^post4+a_128^post9 == 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ head_9^1 == 0 /\ -x_23^post9+x_23^0 == 0 /\ -a_243^post4+a_243^post9 == 0 /\ y_14^0-y_14^post9 == 0 /\ -lt_19^post4+lt_19^post9 == 0 /\ -y_110^post4+y_110^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ x_13^post4-x_23^post9 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post4+y_259^post9 == 0 /\ -k_296^post4+k_296^post9 == 0 /\ -elem_16^post4+elem_16^post9 == 0 /\ -lt_18^post4+lt_18^post9 == 0 /\ -17+length_7^post4 == 0 /\ -y_259^post9+y_259^0 == 0 /\ -y_158^post4+y_158^post9 == 0 /\ i_8^1 == 0 /\ -c_15^post9+c_15^0 == 0 /\ -i_8^1+len_48^post4 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ -lt_21^post4+lt_21^post9 == 0 /\ -y_14^post4+y_14^post9 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0 /\ 1-length_7^post4+i_8^1 <= 0), cost: 1 New rule: l7 -> l0 : _^0'=_^post9, a_128^0'=a_128^post9, a_243^0'=a_243^post9, c_15^0'=c_15^post9, elem_16^0'=elem_16^post9, head_9^0'=head_9^post4, i_8^0'=1+i_8^1, k_296^0'=k_296^post9, len_246^0'=len_246^post9, len_48^0'=i_8^1, length_7^0'=17, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, prev_17^0'=prev_17^post9, result_6^0'=result_6^post9, x_13^0'=x_23^post9, x_23^0'=x_23^post9, y_110^0'=y_110^post9, y_14^0'=y_14^post9, y_158^0'=y_158^post9, y_259^0'=y_259^post9, y_309^0'=y_309^post9, y_80^0'=y_80^post9, (0 == 0 /\ result_6^0-result_6^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ x_13^1 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -16+i_8^1 <= 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ head_9^1 == 0 /\ -x_23^post9+x_23^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post9+y_259^0 == 0 /\ i_8^1 == 0 /\ -c_15^post9+c_15^0 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0), cost: 1 propagated equality y_309^post4 = y_309^post9 propagated equality _^post4 = _^post9 propagated equality prev_17^post4 = prev_17^post9 propagated equality c_15^post4 = c_15^post9 propagated equality x_23^post4 = x_23^post9 propagated equality i_8^post4 = 1+i_8^1 propagated equality lt_20^post4 = lt_20^post9 propagated equality len_246^post4 = len_246^post9 propagated equality y_80^post4 = y_80^post9 propagated equality result_6^post4 = result_6^post9 propagated equality a_128^post4 = a_128^post9 propagated equality a_243^post4 = a_243^post9 propagated equality lt_19^post4 = lt_19^post9 propagated equality y_110^post4 = y_110^post9 propagated equality x_13^post4 = x_23^post9 propagated equality y_259^post4 = y_259^post9 propagated equality k_296^post4 = k_296^post9 propagated equality elem_16^post4 = elem_16^post9 propagated equality lt_18^post4 = lt_18^post9 propagated equality length_7^post4 = 17 propagated equality y_158^post4 = y_158^post9 propagated equality len_48^post4 = i_8^1 propagated equality lt_21^post4 = lt_21^post9 propagated equality y_14^post4 = y_14^post9 Propagated Equalities Original rule: l7 -> l0 : _^0'=_^post9, a_128^0'=a_128^post9, a_243^0'=a_243^post9, c_15^0'=c_15^post9, elem_16^0'=elem_16^post9, head_9^0'=head_9^post4, i_8^0'=1+i_8^1, k_296^0'=k_296^post9, len_246^0'=len_246^post9, len_48^0'=i_8^1, length_7^0'=17, lt_18^0'=lt_18^post9, lt_19^0'=lt_19^post9, lt_20^0'=lt_20^post9, lt_21^0'=lt_21^post9, prev_17^0'=prev_17^post9, result_6^0'=result_6^post9, x_13^0'=x_23^post9, x_23^0'=x_23^post9, y_110^0'=y_110^post9, y_14^0'=y_14^post9, y_158^0'=y_158^post9, y_259^0'=y_259^post9, y_309^0'=y_309^post9, y_80^0'=y_80^post9, (0 == 0 /\ result_6^0-result_6^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ len_48^0-len_48^post9 == 0 /\ -_^post9+_^0 == 0 /\ y_110^0-y_110^post9 == 0 /\ -head_9^post9+head_9^0 == 0 /\ x_13^1 == 0 /\ prev_17^0-prev_17^post9 == 0 /\ -length_7^post9+length_7^0 == 0 /\ len_246^0-len_246^post9 == 0 /\ lt_19^0-lt_19^post9 == 0 /\ -elem_16^post9+elem_16^0 == 0 /\ -k_296^post9+k_296^0 == 0 /\ -y_309^post9+y_309^0 == 0 /\ -16+i_8^1 <= 0 /\ -y_80^post9+y_80^0 == 0 /\ i_8^0-i_8^post9 == 0 /\ head_9^1 == 0 /\ -x_23^post9+x_23^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ -a_128^post9+a_128^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -y_259^post9+y_259^0 == 0 /\ i_8^1 == 0 /\ -c_15^post9+c_15^0 == 0 /\ y_158^0-y_158^post9 == 0 /\ -lt_20^post9+lt_20^0 == 0 /\ a_243^0-a_243^post9 == 0 /\ -lt_18^post9+lt_18^0 == 0), cost: 1 New rule: l7 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post4, i_8^0'=1, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=0, length_7^0'=17, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_23^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -16 <= 0), cost: 1 propagated equality result_6^post9 = result_6^0 propagated equality lt_21^post9 = lt_21^0 propagated equality len_48^post9 = len_48^0 propagated equality _^post9 = _^0 propagated equality y_110^post9 = y_110^0 propagated equality head_9^post9 = head_9^0 propagated equality x_13^1 = 0 propagated equality prev_17^post9 = prev_17^0 propagated equality length_7^post9 = length_7^0 propagated equality len_246^post9 = len_246^0 propagated equality lt_19^post9 = lt_19^0 propagated equality elem_16^post9 = elem_16^0 propagated equality k_296^post9 = k_296^0 propagated equality y_309^post9 = y_309^0 propagated equality y_80^post9 = y_80^0 propagated equality i_8^post9 = i_8^0 propagated equality head_9^1 = 0 propagated equality x_23^post9 = x_23^0 propagated equality y_14^post9 = y_14^0 propagated equality a_128^post9 = a_128^0 propagated equality x_13^post9 = x_13^0 propagated equality y_259^post9 = y_259^0 propagated equality i_8^1 = 0 propagated equality c_15^post9 = c_15^0 propagated equality y_158^post9 = y_158^0 propagated equality lt_20^post9 = lt_20^0 propagated equality a_243^post9 = a_243^0 propagated equality lt_18^post9 = lt_18^0 Simplified Guard Original rule: l7 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post4, i_8^0'=1, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=0, length_7^0'=17, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_23^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -16 <= 0), cost: 1 New rule: l7 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post4, i_8^0'=1, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=0, length_7^0'=17, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_23^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post4, i_8^0'=1, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=0, length_7^0'=17, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_23^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, T, cost: 1 New rule: l7 -> l0 : head_9^0'=head_9^post4, i_8^0'=1, len_48^0'=0, length_7^0'=17, x_13^0'=x_23^0, T, cost: 1 Propagated Equalities Original rule: l0 -> l0 : _^0'=_^post3, a_128^0'=a_128^post3, a_243^0'=a_243^post3, c_15^0'=c_15^post3, elem_16^0'=elem_16^post3, head_9^0'=head_9^post3, i_8^0'=i_8^post3, k_296^0'=k_296^post3, len_246^0'=len_246^post3, len_48^0'=len_48^post3, length_7^0'=length_7^post3, lt_18^0'=lt_18^post3, lt_19^0'=lt_19^post3, lt_20^0'=lt_20^post3, lt_21^0'=lt_21^post3, prev_17^0'=prev_17^post3, result_6^0'=result_6^post3, x_13^0'=x_13^post3, x_23^0'=x_23^post3, y_110^0'=y_110^post3, y_14^0'=y_14^post3, y_158^0'=y_158^post3, y_259^0'=y_259^post3, y_309^0'=y_309^post3, y_80^0'=y_80^post3, (0 == 0 /\ prev_17^post2-prev_17^post3 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ head_9^post2-head_9^post3 == 0 /\ -c_15^post3+c_15^post2 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ y_309^post2-y_309^post3 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ lt_21^post2-lt_21^post3 == 0 /\ y_80^post2-y_80^post3 == 0 /\ a_243^0-a_243^post2 == 0 /\ result_6^post2-result_6^post3 == 0 /\ y_158^post2-y_158^post3 == 0 /\ -len_48^0 <= 0 /\ length_7^post2-length_7^post3 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ lt_19^post2-lt_19^post3 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ k_296^post2-k_296^post3 == 0 /\ -elem_16^post3+elem_16^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ x_23^post2-x_23^post3 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_18^post3+lt_18^post2 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ len_48^post2-len_48^post3 == 0 /\ -len_246^post3+len_246^post2 == 0 /\ -y_110^post2+y_110^0 == 0 /\ y_110^post2-y_110^post3 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ lt_20^post2-lt_20^post3 == 0 /\ -a_128^post3+a_128^post2 == 0 /\ y_14^post2-y_14^post3 == 0 /\ i_8^post2-i_8^post3 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ a_243^post2-a_243^post3 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ -_^post3+_^post2 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ x_13^post2-x_13^post3 == 0 /\ y_259^post2-y_259^post3 == 0 /\ result_6^0-result_6^post2 == 0), cost: 1 New rule: l0 -> l0 : _^0'=_^post2, a_128^0'=a_128^post2, a_243^0'=a_243^post2, c_15^0'=c_15^post2, elem_16^0'=elem_16^post2, head_9^0'=head_9^post2, i_8^0'=i_8^post2, k_296^0'=k_296^post2, len_246^0'=len_246^post2, len_48^0'=len_48^post2, length_7^0'=length_7^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, prev_17^0'=prev_17^post2, result_6^0'=result_6^post2, x_13^0'=x_13^post2, x_23^0'=x_23^post2, y_110^0'=y_110^post2, y_14^0'=y_14^post2, y_158^0'=y_158^post2, y_259^0'=y_259^post2, y_309^0'=y_309^post2, y_80^0'=y_80^post2, (0 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ a_243^0-a_243^post2 == 0 /\ -len_48^0 <= 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ result_6^0-result_6^post2 == 0), cost: 1 propagated equality prev_17^post3 = prev_17^post2 propagated equality head_9^post3 = head_9^post2 propagated equality c_15^post3 = c_15^post2 propagated equality y_309^post3 = y_309^post2 propagated equality lt_21^post3 = lt_21^post2 propagated equality y_80^post3 = y_80^post2 propagated equality result_6^post3 = result_6^post2 propagated equality y_158^post3 = y_158^post2 propagated equality length_7^post3 = length_7^post2 propagated equality lt_19^post3 = lt_19^post2 propagated equality k_296^post3 = k_296^post2 propagated equality elem_16^post3 = elem_16^post2 propagated equality x_23^post3 = x_23^post2 propagated equality lt_18^post3 = lt_18^post2 propagated equality len_48^post3 = len_48^post2 propagated equality len_246^post3 = len_246^post2 propagated equality y_110^post3 = y_110^post2 propagated equality lt_20^post3 = lt_20^post2 propagated equality a_128^post3 = a_128^post2 propagated equality y_14^post3 = y_14^post2 propagated equality i_8^post3 = i_8^post2 propagated equality a_243^post3 = a_243^post2 propagated equality _^post3 = _^post2 propagated equality x_13^post3 = x_13^post2 propagated equality y_259^post3 = y_259^post2 Propagated Equalities Original rule: l0 -> l0 : _^0'=_^post2, a_128^0'=a_128^post2, a_243^0'=a_243^post2, c_15^0'=c_15^post2, elem_16^0'=elem_16^post2, head_9^0'=head_9^post2, i_8^0'=i_8^post2, k_296^0'=k_296^post2, len_246^0'=len_246^post2, len_48^0'=len_48^post2, length_7^0'=length_7^post2, lt_18^0'=lt_18^post2, lt_19^0'=lt_19^post2, lt_20^0'=lt_20^post2, lt_21^0'=lt_21^post2, prev_17^0'=prev_17^post2, result_6^0'=result_6^post2, x_13^0'=x_13^post2, x_23^0'=x_23^post2, y_110^0'=y_110^post2, y_14^0'=y_14^post2, y_158^0'=y_158^post2, y_259^0'=y_259^post2, y_309^0'=y_309^post2, y_80^0'=y_80^post2, (0 == 0 /\ -1+i_8^post2-i_8^0 == 0 /\ -lt_20^post2+lt_20^0 == 0 /\ -y_259^post2+y_259^0 == 0 /\ -elem_16^post2+elem_16^0 == 0 /\ a_128^0-a_128^post2 == 0 /\ -y_158^post2+y_158^0 == 0 /\ a_243^0-a_243^post2 == 0 /\ -len_48^0 <= 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ length_7^0-length_7^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -x_23^post2+x_23^0 == 0 /\ _^0-_^post2 == 0 /\ len_246^0-len_246^post2 == 0 /\ -y_80^post2+y_80^0 == 0 /\ -lt_18^post2+lt_18^0 == 0 /\ -lt_19^post2+lt_19^0 == 0 /\ -y_110^post2+y_110^0 == 0 /\ -prev_17^post2+prev_17^0 == 0 /\ c_15^0-c_15^post2 == 0 /\ -1+len_48^post2-len_48^0 == 0 /\ y_309^0-y_309^post2 == 0 /\ -k_296^post2+k_296^0 == 0 /\ 1-length_7^0+i_8^0 <= 0 /\ result_6^0-result_6^post2 == 0), cost: 1 New rule: l0 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post2, i_8^0'=1+i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=1+len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 propagated equality i_8^post2 = 1+i_8^0 propagated equality lt_20^post2 = lt_20^0 propagated equality y_259^post2 = y_259^0 propagated equality elem_16^post2 = elem_16^0 propagated equality a_128^post2 = a_128^0 propagated equality y_158^post2 = y_158^0 propagated equality a_243^post2 = a_243^0 propagated equality lt_21^post2 = lt_21^0 propagated equality y_14^post2 = y_14^0 propagated equality length_7^post2 = length_7^0 propagated equality x_13^post2 = x_13^0 propagated equality x_23^post2 = x_23^0 propagated equality _^post2 = _^0 propagated equality len_246^post2 = len_246^0 propagated equality y_80^post2 = y_80^0 propagated equality lt_18^post2 = lt_18^0 propagated equality lt_19^post2 = lt_19^0 propagated equality y_110^post2 = y_110^0 propagated equality prev_17^post2 = prev_17^0 propagated equality c_15^post2 = c_15^0 propagated equality len_48^post2 = 1+len_48^0 propagated equality y_309^post2 = y_309^0 propagated equality k_296^post2 = k_296^0 propagated equality result_6^post2 = result_6^0 Simplified Guard Original rule: l0 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post2, i_8^0'=1+i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=1+len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (0 == 0 /\ -len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 New rule: l0 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post2, i_8^0'=1+i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=1+len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l0 : _^0'=_^0, a_128^0'=a_128^0, a_243^0'=a_243^0, c_15^0'=c_15^0, elem_16^0'=elem_16^0, head_9^0'=head_9^post2, i_8^0'=1+i_8^0, k_296^0'=k_296^0, len_246^0'=len_246^0, len_48^0'=1+len_48^0, length_7^0'=length_7^0, lt_18^0'=lt_18^0, lt_19^0'=lt_19^0, lt_20^0'=lt_20^0, lt_21^0'=lt_21^0, prev_17^0'=prev_17^0, result_6^0'=result_6^0, x_13^0'=x_13^0, x_23^0'=x_23^0, y_110^0'=y_110^0, y_14^0'=y_14^0, y_158^0'=y_158^0, y_259^0'=y_259^0, y_309^0'=y_309^0, y_80^0'=y_80^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 New rule: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=1+i_8^0, len_48^0'=1+len_48^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 Step with 16 Trace 16[T] Blocked [{}, {}] Step with 17 Trace 16[T], 17[(-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0)] Blocked [{}, {11[T]}, {}] Accelerate Start location: l7 Program variables: _^0 a_128^0 a_243^0 c_15^0 elem_16^0 head_9^0 i_8^0 k_296^0 len_246^0 len_48^0 length_7^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 prev_17^0 result_6^0 x_13^0 x_23^0 y_110^0 y_14^0 y_158^0 y_259^0 y_309^0 y_80^0 11: l0 -> l1 : a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, len_246^0'=1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, y_14^0'=y_110^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 17: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=1+i_8^0, len_48^0'=1+len_48^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 18: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=n+i_8^0, len_48^0'=n+len_48^0, (length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0), cost: 1 12: l1 -> l4 : k_296^0'=len_246^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, x_13^0'=y_14^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 13: l1 -> l5 : elem_16^0'=y_259^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, prev_17^0'=elem_16^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 14: l4 -> l6 : result_6^0'=result_6^post7, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 15: l4 -> l1 : a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, len_246^0'=1+k_296^0, lt_21^0'=lt_21^post8, prev_17^0'=0, y_14^0'=c_15^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 16: l7 -> l0 : head_9^0'=head_9^post4, i_8^0'=1, len_48^0'=0, length_7^0'=17, x_13^0'=x_23^0, T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=1+i_8^0, len_48^0'=1+len_48^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 New rule: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=n+i_8^0, len_48^0'=n+len_48^0, (length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0), cost: 1 -1+length_7^0-i_8^0 >= 0 [0]: montonic decrease yields length_7^0-n-i_8^0 >= 0 -1+length_7^0-i_8^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+length_7^0-i_8^0 >= 0) len_48^0 >= 0 [0]: monotonic increase yields len_48^0 >= 0 Replacement map: {-1+length_7^0-i_8^0 >= 0 -> length_7^0-n-i_8^0 >= 0, len_48^0 >= 0 -> len_48^0 >= 0} Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}] Step with 11 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {}] Step with 13 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 13[(-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {}, {}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}] Step with 12 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {}] Step with 14 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 14[(-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {}, {}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {14[T]}] Step with 15 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 15[(-a_243^0 <= 0 /\ -k_296^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {14[T]}, {}] Accelerate Start location: l7 Program variables: _^0 a_128^0 a_243^0 c_15^0 elem_16^0 head_9^0 i_8^0 k_296^0 len_246^0 len_48^0 length_7^0 lt_18^0 lt_19^0 lt_20^0 lt_21^0 prev_17^0 result_6^0 x_13^0 x_23^0 y_110^0 y_14^0 y_158^0 y_259^0 y_309^0 y_80^0 11: l0 -> l1 : a_128^0'=-2+len_48^0, a_243^0'=-3+_^0+len_48^0, c_15^0'=y_158^0, elem_16^0'=y_80^0, len_246^0'=1, lt_19^0'=lt_19^post1, lt_20^0'=lt_20^post1, lt_21^0'=lt_21^post1, prev_17^0'=0, result_6^0'=head_9^0, x_13^0'=y_80^0, y_14^0'=y_110^0, (2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0), cost: 1 17: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=1+i_8^0, len_48^0'=1+len_48^0, (-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0), cost: 1 18: l0 -> l0 : head_9^0'=head_9^post2, i_8^0'=n+i_8^0, len_48^0'=n+len_48^0, (length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0), cost: 1 12: l1 -> l4 : k_296^0'=len_246^0, lt_19^0'=lt_19^post5, lt_20^0'=lt_20^post5, x_13^0'=y_14^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 13: l1 -> l5 : elem_16^0'=y_259^0, lt_18^0'=lt_18^post6, lt_19^0'=lt_19^post6, lt_20^0'=lt_20^post6, prev_17^0'=elem_16^0, (-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0), cost: 1 19: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0), cost: 1 14: l4 -> l6 : result_6^0'=result_6^post7, (-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0), cost: 1 15: l4 -> l1 : a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=x_13^0, len_246^0'=1+k_296^0, lt_21^0'=lt_21^post8, prev_17^0'=0, y_14^0'=c_15^0, (-a_243^0 <= 0 /\ -k_296^0 <= 0), cost: 1 16: l7 -> l0 : head_9^0'=head_9^post4, i_8^0'=1, len_48^0'=0, length_7^0'=17, x_13^0'=x_23^0, T, cost: 1 unrolling Original rule: l1 -> l1 : a_243^0'=-1+a_243^0, c_15^0'=y_309^0, elem_16^0'=y_14^0, k_296^0'=len_246^0, len_246^0'=1+len_246^0, lt_19^0'=lt_19^post51, lt_20^0'=lt_20^post51, lt_21^0'=lt_21^post8, prev_17^0'=0, x_13^0'=y_14^0, y_14^0'=c_15^0, (-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0), cost: 1 New rule: l1 -> l1 : a_243^0'=-3+a_243^0, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=2+len_246^0, len_246^0'=3+len_246^0, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 <= 0 /\ 0 == 0 /\ 1-a_243^0 <= 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ -1-len_246^0 <= 0 /\ 2-a_243^0 <= 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -2-len_246^0 <= 0), cost: 1 Loop Acceleration Original rule: l1 -> l1 : a_243^0'=-3+a_243^0, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=2+len_246^0, len_246^0'=3+len_246^0, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 <= 0 /\ 0 == 0 /\ 1-a_243^0 <= 0 /\ -a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ -1-len_246^0 <= 0 /\ 2-a_243^0 <= 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0 /\ -2-len_246^0 <= 0), cost: 1 New rule: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 >= 0 /\ -prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ -1+n2 >= 0), cost: 1 0 >= 0 [0]: monotonic increase yields 0 >= 0 a_243^0 >= 0 [0]: montonic decrease yields 3+a_243^0-3*n2 >= 0, dependencies: -1+a_243^0 >= 0 a_243^0 >= 0 [1]: eventual decrease yields (a_243^0 >= 0 /\ 3+a_243^0-3*n2 >= 0) a_243^0 >= 0 [2]: eventual increase yields (a_243^0 >= 0 /\ 3 <= 0) -1+a_243^0 >= 0 [0]: montonic decrease yields 2+a_243^0-3*n2 >= 0 -1+a_243^0 >= 0 [1]: eventual increase yields (-1+a_243^0 >= 0 /\ 3 <= 0) -prev_17^0 >= 0 [0]: monotonic increase yields -prev_17^0 >= 0 2+len_246^0 >= 0 [0]: monotonic increase yields 2+len_246^0 >= 0 1+len_246^0 >= 0 [0]: monotonic increase yields 1+len_246^0 >= 0, dependencies: 2+len_246^0 >= 0 len_246^0 >= 0 [0]: monotonic increase yields len_246^0 >= 0, dependencies: 2+len_246^0 >= 0 prev_17^0 >= 0 [0]: monotonic increase yields prev_17^0 >= 0 -2+a_243^0 >= 0 [0]: montonic decrease yields 1+a_243^0-3*n2 >= 0 -2+a_243^0 >= 0 [1]: eventual increase yields (3 <= 0 /\ -2+a_243^0 >= 0) Replacement map: {0 >= 0 -> 0 >= 0, a_243^0 >= 0 -> 3+a_243^0-3*n2 >= 0, -1+a_243^0 >= 0 -> 2+a_243^0-3*n2 >= 0, -prev_17^0 >= 0 -> -prev_17^0 >= 0, 2+len_246^0 >= 0 -> 2+len_246^0 >= 0, 1+len_246^0 >= 0 -> 1+len_246^0 >= 0, len_246^0 >= 0 -> len_246^0 >= 0, prev_17^0 >= 0 -> prev_17^0 >= 0, -2+a_243^0 >= 0 -> 1+a_243^0-3*n2 >= 0} made implied equalities explicit Original rule: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 >= 0 /\ -prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ -1+n2 >= 0), cost: 1 New rule: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 >= 0 /\ -prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0), cost: 1 Simplified Guard Original rule: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (0 >= 0 /\ -prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0), cost: 1 New rule: l1 -> l1 : a_243^0'=a_243^0-3*n2, c_15^0'=y_309^0, elem_16^0'=y_309^0, k_296^0'=-1+len_246^0+3*n2, len_246^0'=len_246^0+3*n2, lt_19^0'=lt_19^post512, lt_20^0'=lt_20^post512, lt_21^0'=lt_21^post83, prev_17^0'=0, x_13^0'=y_309^0, y_14^0'=y_309^0, (-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0), cost: 1 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {19[T]}] Step with 13 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 13[(-a_243^0 <= 0 /\ 1-len_246^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {19[T]}, {}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}] Step with 12 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}, {}] Step with 15 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 15[(-a_243^0 <= 0 /\ -k_296^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}, {}, {}] Covered Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}, {15[T]}] Step with 14 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 14[(-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}, {15[T]}, {}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {13[T], 19[T]}, {14[T], 15[T]}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 19[(-prev_17^0 >= 0 /\ 2+a_243^0-3*n2 >= 0 /\ 2+len_246^0 >= 0 /\ 3+a_243^0-3*n2 >= 0 /\ 1+len_246^0 >= 0 /\ len_246^0 >= 0 /\ 1+a_243^0-3*n2 >= 0 /\ prev_17^0 >= 0 /\ prev_17^0 == 0 /\ -1+n2 >= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T]}, {12[T], 13[T], 19[T]}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}] Step with 12 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}, {}] Step with 14 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 14[(-a_243^0 <= 0 /\ -k_296^0 <= 0 /\ c_15^0 <= 0 /\ c_15^0 == 0 /\ -c_15^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}, {}, {}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}, {14[T]}] Step with 15 Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)], 15[(-a_243^0 <= 0 /\ -k_296^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}, {14[T]}, {}] Covered Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)], 12[(-a_243^0 <= 0 /\ -prev_17^0 <= 0 /\ -prev_17^0 == 0 /\ prev_17^0 <= 0 /\ -len_246^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {13[T], 19[T]}, {14[T], 15[T]}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)], 11[(2-len_48^0 <= 0 /\ 1-len_48^0 <= 0 /\ -len_48^0 <= 0 /\ length_7^0-i_8^0 <= 0)] Blocked [{}, {11[T]}, {17[T], 18[T]}, {12[T], 13[T], 19[T]}] Backtrack Trace 16[T], 18[(length_7^0-n-i_8^0 >= 0 /\ -1+n >= 0 /\ len_48^0 >= 0)] Blocked [{}, {11[T]}, {11[T], 17[T], 18[T]}] Backtrack Trace 16[T] Blocked [{}, {11[T], 18[T]}] Step with 17 Trace 16[T], 17[(-len_48^0 <= 0 /\ 1-length_7^0+i_8^0 <= 0)] Blocked [{}, {11[T], 18[T]}, {}] Covered Trace 16[T] Blocked [{}, {11[T], 17[T], 18[T]}] Backtrack Trace Blocked [{16[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b