NO Initial ITS Start location: l13 0: l0 -> l1 : tmp^0'=tmp^post0, length5^0'=length5^post0, tmp15^0'=tmp15^post0, i6^0'=i6^post0, tmp___09^0'=tmp___09^post0, s^0'=s^post0, (length5^0-length5^post0 == 0 /\ -tmp15^post0+tmp15^0 == 0 /\ -i6^post0+i6^0 == 0 /\ -s^post0+s^0 == 0 /\ tmp___09^0-tmp___09^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1 15: l1 -> l2 : tmp^0'=tmp^post15, length5^0'=length5^post15, tmp15^0'=tmp15^post15, i6^0'=i6^post15, tmp___09^0'=tmp___09^post15, s^0'=s^post15, (s^0-s^post15 == 0 /\ -i6^post15+i6^0 == 0 /\ -tmp___09^post15+tmp___09^0 == 0 /\ length5^0-length5^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ tmp15^0-tmp15^post15 == 0), cost: 1 1: l2 -> l0 : tmp^0'=tmp^post1, length5^0'=length5^post1, tmp15^0'=tmp15^post1, i6^0'=i6^post1, tmp___09^0'=tmp___09^post1, s^0'=s^post1, (-tmp___09^post1+tmp___09^0 == 0 /\ -i6^post1+i6^0 == 0 /\ -s^post1+s^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ tmp15^0-tmp15^post1 == 0 /\ length5^0-length5^post1 == 0), cost: 1 2: l2 -> l3 : tmp^0'=tmp^post2, length5^0'=length5^post2, tmp15^0'=tmp15^post2, i6^0'=i6^post2, tmp___09^0'=tmp___09^post2, s^0'=s^post2, (-s^post2+s^0 == 0 /\ i6^0-i6^post2 == 0 /\ length5^0-length5^post2 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp15^0-tmp15^post2 == 0 /\ -tmp___09^post2+tmp___09^0 == 0), cost: 1 3: l2 -> l0 : tmp^0'=tmp^post3, length5^0'=length5^post3, tmp15^0'=tmp15^post3, i6^0'=i6^post3, tmp___09^0'=tmp___09^post3, s^0'=s^post3, (i6^0-i6^post3 == 0 /\ -s^post3+s^0 == 0 /\ tmp15^0-tmp15^post3 == 0 /\ length5^0-length5^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___09^post3+tmp___09^0 == 0), cost: 1 4: l4 -> l5 : tmp^0'=tmp^post4, length5^0'=length5^post4, tmp15^0'=tmp15^post4, i6^0'=i6^post4, tmp___09^0'=tmp___09^post4, s^0'=s^post4, (tmp15^0-tmp15^post4 == 0 /\ i6^0-i6^post4 == 0 /\ -length5^post4+length5^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -s^post4+s^0 == 0 /\ -tmp___09^post4+tmp___09^0 == 0), cost: 1 16: l5 -> l9 : tmp^0'=tmp^post16, length5^0'=length5^post16, tmp15^0'=tmp15^post16, i6^0'=i6^post16, tmp___09^0'=tmp___09^post16, s^0'=s^post16, (tmp^0-tmp^post16 == 0 /\ length5^0-i6^0 <= 0 /\ tmp15^0-tmp15^post16 == 0 /\ -length5^post16+length5^0 == 0 /\ -i6^post16+i6^0 == 0 /\ -s^post16+s^0 == 0 /\ -tmp___09^post16+tmp___09^0 == 0), cost: 1 17: l5 -> l4 : tmp^0'=tmp^post17, length5^0'=length5^post17, tmp15^0'=tmp15^post17, i6^0'=i6^post17, tmp___09^0'=tmp___09^post17, s^0'=s^post17, (0 == 0 /\ -s^post17+s^0 == 0 /\ -1-i6^0+i6^post17 == 0 /\ 1-length5^0+i6^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -tmp15^post17+tmp15^0 == 0 /\ length5^0-length5^post17 == 0), cost: 1 5: l6 -> l7 : tmp^0'=tmp^post5, length5^0'=length5^post5, tmp15^0'=tmp15^post5, i6^0'=i6^post5, tmp___09^0'=tmp___09^post5, s^0'=s^post5, (-s^post5+s^0 == 0 /\ -tmp15^post5+tmp15^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ i6^0-i6^post5 == 0 /\ tmp___09^0-tmp___09^post5 == 0 /\ length5^0-length5^post5 == 0), cost: 1 10: l7 -> l8 : tmp^0'=tmp^post10, length5^0'=length5^post10, tmp15^0'=tmp15^post10, i6^0'=i6^post10, tmp___09^0'=tmp___09^post10, s^0'=s^post10, (tmp^0-tmp^post10 == 0 /\ -length5^post10+length5^0 == 0 /\ tmp15^0-tmp15^post10 == 0 /\ i6^0-i6^post10 == 0 /\ -s^post10+s^0 == 0 /\ -tmp___09^post10+tmp___09^0 == 0), cost: 1 6: l8 -> l6 : tmp^0'=tmp^post6, length5^0'=length5^post6, tmp15^0'=tmp15^post6, i6^0'=i6^post6, tmp___09^0'=tmp___09^post6, s^0'=s^post6, (tmp^0-tmp^post6 == 0 /\ -s^post6+s^0 == 0 /\ -tmp15^post6+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post6 == 0 /\ -i6^post6+i6^0 == 0 /\ length5^0-length5^post6 == 0), cost: 1 7: l8 -> l6 : tmp^0'=tmp^post7, length5^0'=length5^post7, tmp15^0'=tmp15^post7, i6^0'=i6^post7, tmp___09^0'=tmp___09^post7, s^0'=s^post7, (s^0-s^post7 == 0 /\ -tmp___09^post7+tmp___09^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp15^0-tmp15^post7 == 0 /\ length5^0-length5^post7 == 0 /\ -i6^post7+i6^0 == 0), cost: 1 8: l8 -> l1 : tmp^0'=tmp^post8, length5^0'=length5^post8, tmp15^0'=tmp15^post8, i6^0'=i6^post8, tmp___09^0'=tmp___09^post8, s^0'=s^post8, (-tmp___09^post8+tmp___09^0 == 0 /\ -s^post8+s^0 == 0 /\ -i6^post8+i6^0 == 0 /\ tmp15^0-tmp15^post8 == 0 /\ length5^0-length5^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 9: l9 -> l10 : tmp^0'=tmp^post9, length5^0'=length5^post9, tmp15^0'=tmp15^post9, i6^0'=i6^post9, tmp___09^0'=tmp___09^post9, s^0'=s^post9, (-tmp___09^post9+tmp___09^0 == 0 /\ -i6^post9+i6^0 == 0 /\ length5^0-length5^post9 == 0 /\ -s^post9+s^0 == 0 /\ tmp15^0-tmp15^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 12: l10 -> l11 : tmp^0'=tmp^post12, length5^0'=length5^post12, tmp15^0'=tmp15^post12, i6^0'=i6^post12, tmp___09^0'=tmp___09^post12, s^0'=s^post12, (tmp^0-tmp^post12 == 0 /\ tmp___09^0-tmp___09^post12 == 0 /\ length5^0-length5^post12 == 0 /\ -s^post12+s^0 == 0 /\ -tmp15^post12+tmp15^0 == 0 /\ -i6^post12+i6^0 == 0), cost: 1 13: l10 -> l7 : tmp^0'=tmp^post13, length5^0'=length5^post13, tmp15^0'=tmp15^post13, i6^0'=i6^post13, tmp___09^0'=tmp___09^post13, s^0'=s^post13, (tmp^0-tmp^post13 == 0 /\ length5^0-length5^post13 == 0 /\ -tmp15^post13+tmp15^0 == 0 /\ -s^post13+s^0 == 0 /\ -i6^post13+i6^0 == 0 /\ tmp___09^0-tmp___09^post13 == 0), cost: 1 14: l10 -> l11 : tmp^0'=tmp^post14, length5^0'=length5^post14, tmp15^0'=tmp15^post14, i6^0'=i6^post14, tmp___09^0'=tmp___09^post14, s^0'=s^post14, (length5^0-length5^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -tmp15^post14+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post14 == 0 /\ s^0-s^post14 == 0 /\ -i6^post14+i6^0 == 0), cost: 1 11: l11 -> l9 : tmp^0'=tmp^post11, length5^0'=length5^post11, tmp15^0'=tmp15^post11, i6^0'=i6^post11, tmp___09^0'=tmp___09^post11, s^0'=s^post11, (0 == 0 /\ i6^0-i6^post11 == 0 /\ -s^post11+s^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ length5^0-length5^post11 == 0 /\ tmp___09^0-tmp___09^post11 == 0), cost: 1 18: l12 -> l4 : tmp^0'=tmp^post18, length5^0'=length5^post18, tmp15^0'=tmp15^post18, i6^0'=i6^post18, tmp___09^0'=tmp___09^post18, s^0'=s^post18, (0 == 0 /\ i6^post18 == 0 /\ tmp___09^0-tmp___09^post18 == 0 /\ s^post18-tmp^post18 == 0 /\ -tmp15^post18+tmp15^0 == 0 /\ -s^post18+length5^post18 == 0), cost: 1 19: l13 -> l12 : tmp^0'=tmp^post19, length5^0'=length5^post19, tmp15^0'=tmp15^post19, i6^0'=i6^post19, tmp___09^0'=tmp___09^post19, s^0'=s^post19, (tmp^0-tmp^post19 == 0 /\ -i6^post19+i6^0 == 0 /\ -tmp15^post19+tmp15^0 == 0 /\ length5^0-length5^post19 == 0 /\ tmp___09^0-tmp___09^post19 == 0 /\ -s^post19+s^0 == 0), cost: 1 Removed unreachable rules and leafs Start location: l13 0: l0 -> l1 : tmp^0'=tmp^post0, length5^0'=length5^post0, tmp15^0'=tmp15^post0, i6^0'=i6^post0, tmp___09^0'=tmp___09^post0, s^0'=s^post0, (length5^0-length5^post0 == 0 /\ -tmp15^post0+tmp15^0 == 0 /\ -i6^post0+i6^0 == 0 /\ -s^post0+s^0 == 0 /\ tmp___09^0-tmp___09^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1 15: l1 -> l2 : tmp^0'=tmp^post15, length5^0'=length5^post15, tmp15^0'=tmp15^post15, i6^0'=i6^post15, tmp___09^0'=tmp___09^post15, s^0'=s^post15, (s^0-s^post15 == 0 /\ -i6^post15+i6^0 == 0 /\ -tmp___09^post15+tmp___09^0 == 0 /\ length5^0-length5^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ tmp15^0-tmp15^post15 == 0), cost: 1 1: l2 -> l0 : tmp^0'=tmp^post1, length5^0'=length5^post1, tmp15^0'=tmp15^post1, i6^0'=i6^post1, tmp___09^0'=tmp___09^post1, s^0'=s^post1, (-tmp___09^post1+tmp___09^0 == 0 /\ -i6^post1+i6^0 == 0 /\ -s^post1+s^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ tmp15^0-tmp15^post1 == 0 /\ length5^0-length5^post1 == 0), cost: 1 3: l2 -> l0 : tmp^0'=tmp^post3, length5^0'=length5^post3, tmp15^0'=tmp15^post3, i6^0'=i6^post3, tmp___09^0'=tmp___09^post3, s^0'=s^post3, (i6^0-i6^post3 == 0 /\ -s^post3+s^0 == 0 /\ tmp15^0-tmp15^post3 == 0 /\ length5^0-length5^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___09^post3+tmp___09^0 == 0), cost: 1 4: l4 -> l5 : tmp^0'=tmp^post4, length5^0'=length5^post4, tmp15^0'=tmp15^post4, i6^0'=i6^post4, tmp___09^0'=tmp___09^post4, s^0'=s^post4, (tmp15^0-tmp15^post4 == 0 /\ i6^0-i6^post4 == 0 /\ -length5^post4+length5^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -s^post4+s^0 == 0 /\ -tmp___09^post4+tmp___09^0 == 0), cost: 1 16: l5 -> l9 : tmp^0'=tmp^post16, length5^0'=length5^post16, tmp15^0'=tmp15^post16, i6^0'=i6^post16, tmp___09^0'=tmp___09^post16, s^0'=s^post16, (tmp^0-tmp^post16 == 0 /\ length5^0-i6^0 <= 0 /\ tmp15^0-tmp15^post16 == 0 /\ -length5^post16+length5^0 == 0 /\ -i6^post16+i6^0 == 0 /\ -s^post16+s^0 == 0 /\ -tmp___09^post16+tmp___09^0 == 0), cost: 1 17: l5 -> l4 : tmp^0'=tmp^post17, length5^0'=length5^post17, tmp15^0'=tmp15^post17, i6^0'=i6^post17, tmp___09^0'=tmp___09^post17, s^0'=s^post17, (0 == 0 /\ -s^post17+s^0 == 0 /\ -1-i6^0+i6^post17 == 0 /\ 1-length5^0+i6^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -tmp15^post17+tmp15^0 == 0 /\ length5^0-length5^post17 == 0), cost: 1 5: l6 -> l7 : tmp^0'=tmp^post5, length5^0'=length5^post5, tmp15^0'=tmp15^post5, i6^0'=i6^post5, tmp___09^0'=tmp___09^post5, s^0'=s^post5, (-s^post5+s^0 == 0 /\ -tmp15^post5+tmp15^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ i6^0-i6^post5 == 0 /\ tmp___09^0-tmp___09^post5 == 0 /\ length5^0-length5^post5 == 0), cost: 1 10: l7 -> l8 : tmp^0'=tmp^post10, length5^0'=length5^post10, tmp15^0'=tmp15^post10, i6^0'=i6^post10, tmp___09^0'=tmp___09^post10, s^0'=s^post10, (tmp^0-tmp^post10 == 0 /\ -length5^post10+length5^0 == 0 /\ tmp15^0-tmp15^post10 == 0 /\ i6^0-i6^post10 == 0 /\ -s^post10+s^0 == 0 /\ -tmp___09^post10+tmp___09^0 == 0), cost: 1 6: l8 -> l6 : tmp^0'=tmp^post6, length5^0'=length5^post6, tmp15^0'=tmp15^post6, i6^0'=i6^post6, tmp___09^0'=tmp___09^post6, s^0'=s^post6, (tmp^0-tmp^post6 == 0 /\ -s^post6+s^0 == 0 /\ -tmp15^post6+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post6 == 0 /\ -i6^post6+i6^0 == 0 /\ length5^0-length5^post6 == 0), cost: 1 7: l8 -> l6 : tmp^0'=tmp^post7, length5^0'=length5^post7, tmp15^0'=tmp15^post7, i6^0'=i6^post7, tmp___09^0'=tmp___09^post7, s^0'=s^post7, (s^0-s^post7 == 0 /\ -tmp___09^post7+tmp___09^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp15^0-tmp15^post7 == 0 /\ length5^0-length5^post7 == 0 /\ -i6^post7+i6^0 == 0), cost: 1 8: l8 -> l1 : tmp^0'=tmp^post8, length5^0'=length5^post8, tmp15^0'=tmp15^post8, i6^0'=i6^post8, tmp___09^0'=tmp___09^post8, s^0'=s^post8, (-tmp___09^post8+tmp___09^0 == 0 /\ -s^post8+s^0 == 0 /\ -i6^post8+i6^0 == 0 /\ tmp15^0-tmp15^post8 == 0 /\ length5^0-length5^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 9: l9 -> l10 : tmp^0'=tmp^post9, length5^0'=length5^post9, tmp15^0'=tmp15^post9, i6^0'=i6^post9, tmp___09^0'=tmp___09^post9, s^0'=s^post9, (-tmp___09^post9+tmp___09^0 == 0 /\ -i6^post9+i6^0 == 0 /\ length5^0-length5^post9 == 0 /\ -s^post9+s^0 == 0 /\ tmp15^0-tmp15^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 12: l10 -> l11 : tmp^0'=tmp^post12, length5^0'=length5^post12, tmp15^0'=tmp15^post12, i6^0'=i6^post12, tmp___09^0'=tmp___09^post12, s^0'=s^post12, (tmp^0-tmp^post12 == 0 /\ tmp___09^0-tmp___09^post12 == 0 /\ length5^0-length5^post12 == 0 /\ -s^post12+s^0 == 0 /\ -tmp15^post12+tmp15^0 == 0 /\ -i6^post12+i6^0 == 0), cost: 1 13: l10 -> l7 : tmp^0'=tmp^post13, length5^0'=length5^post13, tmp15^0'=tmp15^post13, i6^0'=i6^post13, tmp___09^0'=tmp___09^post13, s^0'=s^post13, (tmp^0-tmp^post13 == 0 /\ length5^0-length5^post13 == 0 /\ -tmp15^post13+tmp15^0 == 0 /\ -s^post13+s^0 == 0 /\ -i6^post13+i6^0 == 0 /\ tmp___09^0-tmp___09^post13 == 0), cost: 1 14: l10 -> l11 : tmp^0'=tmp^post14, length5^0'=length5^post14, tmp15^0'=tmp15^post14, i6^0'=i6^post14, tmp___09^0'=tmp___09^post14, s^0'=s^post14, (length5^0-length5^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -tmp15^post14+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post14 == 0 /\ s^0-s^post14 == 0 /\ -i6^post14+i6^0 == 0), cost: 1 11: l11 -> l9 : tmp^0'=tmp^post11, length5^0'=length5^post11, tmp15^0'=tmp15^post11, i6^0'=i6^post11, tmp___09^0'=tmp___09^post11, s^0'=s^post11, (0 == 0 /\ i6^0-i6^post11 == 0 /\ -s^post11+s^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ length5^0-length5^post11 == 0 /\ tmp___09^0-tmp___09^post11 == 0), cost: 1 18: l12 -> l4 : tmp^0'=tmp^post18, length5^0'=length5^post18, tmp15^0'=tmp15^post18, i6^0'=i6^post18, tmp___09^0'=tmp___09^post18, s^0'=s^post18, (0 == 0 /\ i6^post18 == 0 /\ tmp___09^0-tmp___09^post18 == 0 /\ s^post18-tmp^post18 == 0 /\ -tmp15^post18+tmp15^0 == 0 /\ -s^post18+length5^post18 == 0), cost: 1 19: l13 -> l12 : tmp^0'=tmp^post19, length5^0'=length5^post19, tmp15^0'=tmp15^post19, i6^0'=i6^post19, tmp___09^0'=tmp___09^post19, s^0'=s^post19, (tmp^0-tmp^post19 == 0 /\ -i6^post19+i6^0 == 0 /\ -tmp15^post19+tmp15^0 == 0 /\ length5^0-length5^post19 == 0 /\ tmp___09^0-tmp___09^post19 == 0 /\ -s^post19+s^0 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : tmp^0'=tmp^post0, length5^0'=length5^post0, tmp15^0'=tmp15^post0, i6^0'=i6^post0, tmp___09^0'=tmp___09^post0, s^0'=s^post0, (length5^0-length5^post0 == 0 /\ -tmp15^post0+tmp15^0 == 0 /\ -i6^post0+i6^0 == 0 /\ -s^post0+s^0 == 0 /\ tmp___09^0-tmp___09^post0 == 0 /\ tmp^0-tmp^post0 == 0), cost: 1 New rule: l0 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l0 : tmp^0'=tmp^post1, length5^0'=length5^post1, tmp15^0'=tmp15^post1, i6^0'=i6^post1, tmp___09^0'=tmp___09^post1, s^0'=s^post1, (-tmp___09^post1+tmp___09^0 == 0 /\ -i6^post1+i6^0 == 0 /\ -s^post1+s^0 == 0 /\ tmp^0-tmp^post1 == 0 /\ tmp15^0-tmp15^post1 == 0 /\ length5^0-length5^post1 == 0), cost: 1 New rule: l2 -> l0 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l0 : tmp^0'=tmp^post3, length5^0'=length5^post3, tmp15^0'=tmp15^post3, i6^0'=i6^post3, tmp___09^0'=tmp___09^post3, s^0'=s^post3, (i6^0-i6^post3 == 0 /\ -s^post3+s^0 == 0 /\ tmp15^0-tmp15^post3 == 0 /\ length5^0-length5^post3 == 0 /\ tmp^0-tmp^post3 == 0 /\ -tmp___09^post3+tmp___09^0 == 0), cost: 1 New rule: l2 -> l0 : TRUE, cost: 1 Applied preprocessing Original rule: l4 -> l5 : tmp^0'=tmp^post4, length5^0'=length5^post4, tmp15^0'=tmp15^post4, i6^0'=i6^post4, tmp___09^0'=tmp___09^post4, s^0'=s^post4, (tmp15^0-tmp15^post4 == 0 /\ i6^0-i6^post4 == 0 /\ -length5^post4+length5^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -s^post4+s^0 == 0 /\ -tmp___09^post4+tmp___09^0 == 0), cost: 1 New rule: l4 -> l5 : TRUE, cost: 1 Applied preprocessing Original rule: l6 -> l7 : tmp^0'=tmp^post5, length5^0'=length5^post5, tmp15^0'=tmp15^post5, i6^0'=i6^post5, tmp___09^0'=tmp___09^post5, s^0'=s^post5, (-s^post5+s^0 == 0 /\ -tmp15^post5+tmp15^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ i6^0-i6^post5 == 0 /\ tmp___09^0-tmp___09^post5 == 0 /\ length5^0-length5^post5 == 0), cost: 1 New rule: l6 -> l7 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l6 : tmp^0'=tmp^post6, length5^0'=length5^post6, tmp15^0'=tmp15^post6, i6^0'=i6^post6, tmp___09^0'=tmp___09^post6, s^0'=s^post6, (tmp^0-tmp^post6 == 0 /\ -s^post6+s^0 == 0 /\ -tmp15^post6+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post6 == 0 /\ -i6^post6+i6^0 == 0 /\ length5^0-length5^post6 == 0), cost: 1 New rule: l8 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l6 : tmp^0'=tmp^post7, length5^0'=length5^post7, tmp15^0'=tmp15^post7, i6^0'=i6^post7, tmp___09^0'=tmp___09^post7, s^0'=s^post7, (s^0-s^post7 == 0 /\ -tmp___09^post7+tmp___09^0 == 0 /\ tmp^0-tmp^post7 == 0 /\ tmp15^0-tmp15^post7 == 0 /\ length5^0-length5^post7 == 0 /\ -i6^post7+i6^0 == 0), cost: 1 New rule: l8 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l1 : tmp^0'=tmp^post8, length5^0'=length5^post8, tmp15^0'=tmp15^post8, i6^0'=i6^post8, tmp___09^0'=tmp___09^post8, s^0'=s^post8, (-tmp___09^post8+tmp___09^0 == 0 /\ -s^post8+s^0 == 0 /\ -i6^post8+i6^0 == 0 /\ tmp15^0-tmp15^post8 == 0 /\ length5^0-length5^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 New rule: l8 -> l1 : TRUE, cost: 1 Applied preprocessing Original rule: l9 -> l10 : tmp^0'=tmp^post9, length5^0'=length5^post9, tmp15^0'=tmp15^post9, i6^0'=i6^post9, tmp___09^0'=tmp___09^post9, s^0'=s^post9, (-tmp___09^post9+tmp___09^0 == 0 /\ -i6^post9+i6^0 == 0 /\ length5^0-length5^post9 == 0 /\ -s^post9+s^0 == 0 /\ tmp15^0-tmp15^post9 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 New rule: l9 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l8 : tmp^0'=tmp^post10, length5^0'=length5^post10, tmp15^0'=tmp15^post10, i6^0'=i6^post10, tmp___09^0'=tmp___09^post10, s^0'=s^post10, (tmp^0-tmp^post10 == 0 /\ -length5^post10+length5^0 == 0 /\ tmp15^0-tmp15^post10 == 0 /\ i6^0-i6^post10 == 0 /\ -s^post10+s^0 == 0 /\ -tmp___09^post10+tmp___09^0 == 0), cost: 1 New rule: l7 -> l8 : TRUE, cost: 1 Applied preprocessing Original rule: l11 -> l9 : tmp^0'=tmp^post11, length5^0'=length5^post11, tmp15^0'=tmp15^post11, i6^0'=i6^post11, tmp___09^0'=tmp___09^post11, s^0'=s^post11, (0 == 0 /\ i6^0-i6^post11 == 0 /\ -s^post11+s^0 == 0 /\ tmp^0-tmp^post11 == 0 /\ length5^0-length5^post11 == 0 /\ tmp___09^0-tmp___09^post11 == 0), cost: 1 New rule: l11 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 1 Applied preprocessing Original rule: l10 -> l11 : tmp^0'=tmp^post12, length5^0'=length5^post12, tmp15^0'=tmp15^post12, i6^0'=i6^post12, tmp___09^0'=tmp___09^post12, s^0'=s^post12, (tmp^0-tmp^post12 == 0 /\ tmp___09^0-tmp___09^post12 == 0 /\ length5^0-length5^post12 == 0 /\ -s^post12+s^0 == 0 /\ -tmp15^post12+tmp15^0 == 0 /\ -i6^post12+i6^0 == 0), cost: 1 New rule: l10 -> l11 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l7 : tmp^0'=tmp^post13, length5^0'=length5^post13, tmp15^0'=tmp15^post13, i6^0'=i6^post13, tmp___09^0'=tmp___09^post13, s^0'=s^post13, (tmp^0-tmp^post13 == 0 /\ length5^0-length5^post13 == 0 /\ -tmp15^post13+tmp15^0 == 0 /\ -s^post13+s^0 == 0 /\ -i6^post13+i6^0 == 0 /\ tmp___09^0-tmp___09^post13 == 0), cost: 1 New rule: l10 -> l7 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l11 : tmp^0'=tmp^post14, length5^0'=length5^post14, tmp15^0'=tmp15^post14, i6^0'=i6^post14, tmp___09^0'=tmp___09^post14, s^0'=s^post14, (length5^0-length5^post14 == 0 /\ tmp^0-tmp^post14 == 0 /\ -tmp15^post14+tmp15^0 == 0 /\ tmp___09^0-tmp___09^post14 == 0 /\ s^0-s^post14 == 0 /\ -i6^post14+i6^0 == 0), cost: 1 New rule: l10 -> l11 : TRUE, cost: 1 Applied preprocessing Original rule: l1 -> l2 : tmp^0'=tmp^post15, length5^0'=length5^post15, tmp15^0'=tmp15^post15, i6^0'=i6^post15, tmp___09^0'=tmp___09^post15, s^0'=s^post15, (s^0-s^post15 == 0 /\ -i6^post15+i6^0 == 0 /\ -tmp___09^post15+tmp___09^0 == 0 /\ length5^0-length5^post15 == 0 /\ tmp^0-tmp^post15 == 0 /\ tmp15^0-tmp15^post15 == 0), cost: 1 New rule: l1 -> l2 : TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l9 : tmp^0'=tmp^post16, length5^0'=length5^post16, tmp15^0'=tmp15^post16, i6^0'=i6^post16, tmp___09^0'=tmp___09^post16, s^0'=s^post16, (tmp^0-tmp^post16 == 0 /\ length5^0-i6^0 <= 0 /\ tmp15^0-tmp15^post16 == 0 /\ -length5^post16+length5^0 == 0 /\ -i6^post16+i6^0 == 0 /\ -s^post16+s^0 == 0 /\ -tmp___09^post16+tmp___09^0 == 0), cost: 1 New rule: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 Applied preprocessing Original rule: l5 -> l4 : tmp^0'=tmp^post17, length5^0'=length5^post17, tmp15^0'=tmp15^post17, i6^0'=i6^post17, tmp___09^0'=tmp___09^post17, s^0'=s^post17, (0 == 0 /\ -s^post17+s^0 == 0 /\ -1-i6^0+i6^post17 == 0 /\ 1-length5^0+i6^0 <= 0 /\ tmp^0-tmp^post17 == 0 /\ -tmp15^post17+tmp15^0 == 0 /\ length5^0-length5^post17 == 0), cost: 1 New rule: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 Applied preprocessing Original rule: l12 -> l4 : tmp^0'=tmp^post18, length5^0'=length5^post18, tmp15^0'=tmp15^post18, i6^0'=i6^post18, tmp___09^0'=tmp___09^post18, s^0'=s^post18, (0 == 0 /\ i6^post18 == 0 /\ tmp___09^0-tmp___09^post18 == 0 /\ s^post18-tmp^post18 == 0 /\ -tmp15^post18+tmp15^0 == 0 /\ -s^post18+length5^post18 == 0), cost: 1 New rule: l12 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 1 Applied preprocessing Original rule: l13 -> l12 : tmp^0'=tmp^post19, length5^0'=length5^post19, tmp15^0'=tmp15^post19, i6^0'=i6^post19, tmp___09^0'=tmp___09^post19, s^0'=s^post19, (tmp^0-tmp^post19 == 0 /\ -i6^post19+i6^0 == 0 /\ -tmp15^post19+tmp15^0 == 0 /\ length5^0-length5^post19 == 0 /\ tmp___09^0-tmp___09^post19 == 0 /\ -s^post19+s^0 == 0), cost: 1 New rule: l13 -> l12 : TRUE, cost: 1 Simplified rules Start location: l13 20: l0 -> l1 : TRUE, cost: 1 31: l1 -> l2 : TRUE, cost: 1 21: l2 -> l0 : TRUE, cost: 1 22: l4 -> l5 : TRUE, cost: 1 32: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 33: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 23: l6 -> l7 : TRUE, cost: 1 27: l7 -> l8 : TRUE, cost: 1 24: l8 -> l6 : TRUE, cost: 1 25: l8 -> l1 : TRUE, cost: 1 26: l9 -> l10 : TRUE, cost: 1 29: l10 -> l11 : TRUE, cost: 1 30: l10 -> l7 : TRUE, cost: 1 28: l11 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 1 34: l12 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 1 35: l13 -> l12 : TRUE, cost: 1 Eliminating location l12 by chaining: Applied chaining First rule: l13 -> l12 : TRUE, cost: 1 Second rule: l12 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 1 New rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Applied deletion Removed the following rules: 34 35 Eliminating location l11 by chaining: Applied chaining First rule: l10 -> l11 : TRUE, cost: 1 Second rule: l11 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 1 New rule: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 Applied deletion Removed the following rules: 28 29 Eliminating location l6 by chaining: Applied chaining First rule: l8 -> l6 : TRUE, cost: 1 Second rule: l6 -> l7 : TRUE, cost: 1 New rule: l8 -> l7 : TRUE, cost: 2 Applied deletion Removed the following rules: 23 24 Eliminating location l2 by chaining: Applied chaining First rule: l1 -> l2 : TRUE, cost: 1 Second rule: l2 -> l0 : TRUE, cost: 1 New rule: l1 -> l0 : TRUE, cost: 2 Applied deletion Removed the following rules: 21 31 Eliminating location l0 by chaining: Applied chaining First rule: l1 -> l0 : TRUE, cost: 2 Second rule: l0 -> l1 : TRUE, cost: 1 New rule: l1 -> l1 : TRUE, cost: 3 Applied deletion Removed the following rules: 20 39 Eliminated locations on linear paths Start location: l13 40: l1 -> l1 : TRUE, cost: 3 22: l4 -> l5 : TRUE, cost: 1 32: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 33: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 27: l7 -> l8 : TRUE, cost: 1 25: l8 -> l1 : TRUE, cost: 1 38: l8 -> l7 : TRUE, cost: 2 26: l9 -> l10 : TRUE, cost: 1 30: l10 -> l7 : TRUE, cost: 1 37: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Applied nonterm Original rule: l1 -> l1 : TRUE, cost: 3 New rule: l1 -> [14] : n >= 0, cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_FNPBEK.txt Applied deletion Removed the following rules: 40 Accelerated simple loops Start location: l13 41: l1 -> [14] : n >= 0, cost: NONTERM 22: l4 -> l5 : TRUE, cost: 1 32: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 33: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 27: l7 -> l8 : TRUE, cost: 1 25: l8 -> l1 : TRUE, cost: 1 38: l8 -> l7 : TRUE, cost: 2 26: l9 -> l10 : TRUE, cost: 1 30: l10 -> l7 : TRUE, cost: 1 37: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Applied chaining First rule: l8 -> l1 : TRUE, cost: 1 Second rule: l1 -> [14] : n >= 0, cost: NONTERM New rule: l8 -> [14] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 41 Chained accelerated rules with incoming rules Start location: l13 22: l4 -> l5 : TRUE, cost: 1 32: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 33: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 27: l7 -> l8 : TRUE, cost: 1 25: l8 -> l1 : TRUE, cost: 1 38: l8 -> l7 : TRUE, cost: 2 42: l8 -> [14] : TRUE, cost: NONTERM 26: l9 -> l10 : TRUE, cost: 1 30: l10 -> l7 : TRUE, cost: 1 37: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l13 22: l4 -> l5 : TRUE, cost: 1 32: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 33: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 27: l7 -> l8 : TRUE, cost: 1 38: l8 -> l7 : TRUE, cost: 2 42: l8 -> [14] : TRUE, cost: NONTERM 26: l9 -> l10 : TRUE, cost: 1 30: l10 -> l7 : TRUE, cost: 1 37: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Eliminating location l5 by chaining: Applied chaining First rule: l4 -> l5 : TRUE, cost: 1 Second rule: l5 -> l9 : length5^0-i6^0 <= 0, cost: 1 New rule: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 Applied chaining First rule: l4 -> l5 : TRUE, cost: 1 Second rule: l5 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 1 New rule: l4 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 2 Applied deletion Removed the following rules: 22 32 33 Eliminating location l10 by chaining: Applied chaining First rule: l9 -> l10 : TRUE, cost: 1 Second rule: l10 -> l7 : TRUE, cost: 1 New rule: l9 -> l7 : TRUE, cost: 2 Applied chaining First rule: l9 -> l10 : TRUE, cost: 1 Second rule: l10 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 2 New rule: l9 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 3 Applied deletion Removed the following rules: 26 30 37 Eliminating location l8 by chaining: Applied chaining First rule: l7 -> l8 : TRUE, cost: 1 Second rule: l8 -> l7 : TRUE, cost: 2 New rule: l7 -> l7 : TRUE, cost: 3 Applied chaining First rule: l7 -> l8 : TRUE, cost: 1 Second rule: l8 -> [14] : TRUE, cost: NONTERM New rule: l7 -> [14] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 27 38 42 Eliminated locations on tree-shaped paths Start location: l13 43: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 44: l4 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 2 47: l7 -> l7 : TRUE, cost: 3 48: l7 -> [14] : TRUE, cost: NONTERM 45: l9 -> l7 : TRUE, cost: 2 46: l9 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 3 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Applied acceleration Original rule: l4 -> l4 : i6^0'=1+i6^0, tmp___09^0'=tmp___09^post17, 1-length5^0+i6^0 <= 0, cost: 2 New rule: l4 -> l4 : i6^0'=i6^0+n0, tmp___09^0'=tmp___09^post17, (-1+n0 >= 0 /\ length5^0-i6^0-n0 >= 0), cost: 2*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_kHcGHp.txt Applied instantiation Original rule: l4 -> l4 : i6^0'=i6^0+n0, tmp___09^0'=tmp___09^post17, (-1+n0 >= 0 /\ length5^0-i6^0-n0 >= 0), cost: 2*n0 New rule: l4 -> l4 : i6^0'=length5^0, tmp___09^0'=tmp___09^post17, (0 >= 0 /\ -1+length5^0-i6^0 >= 0), cost: 2*length5^0-2*i6^0 Applied simplification Original rule: l4 -> l4 : i6^0'=length5^0, tmp___09^0'=tmp___09^post17, (0 >= 0 /\ -1+length5^0-i6^0 >= 0), cost: 2*length5^0-2*i6^0 New rule: l4 -> l4 : i6^0'=length5^0, tmp___09^0'=tmp___09^post17, -1+length5^0-i6^0 >= 0, cost: 2*length5^0-2*i6^0 Applied deletion Removed the following rules: 44 Applied nonterm Original rule: l7 -> l7 : TRUE, cost: 3 New rule: l7 -> [16] : n1 >= 0, cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_LgfmAg.txt Applied deletion Removed the following rules: 47 Applied nonterm Original rule: l9 -> l9 : tmp15^0'=tmp15^post11, 0 == 0, cost: 3 New rule: l9 -> [17] : (0 >= 0 /\ -1+n2 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_fNDGeC.txt Applied simplification Original rule: l9 -> [17] : (0 >= 0 /\ -1+n2 >= 0), cost: NONTERM New rule: l9 -> [17] : -1+n2 >= 0, cost: NONTERM Applied deletion Removed the following rules: 46 Accelerated simple loops Start location: l13 43: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 50: l4 -> l4 : i6^0'=length5^0, tmp___09^0'=tmp___09^post17, -1+length5^0-i6^0 >= 0, cost: 2*length5^0-2*i6^0 48: l7 -> [14] : TRUE, cost: NONTERM 51: l7 -> [16] : n1 >= 0, cost: NONTERM 45: l9 -> l7 : TRUE, cost: 2 53: l9 -> [17] : -1+n2 >= 0, cost: NONTERM 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Applied chaining First rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Second rule: l4 -> l4 : i6^0'=length5^0, tmp___09^0'=tmp___09^post17, -1+length5^0-i6^0 >= 0, cost: 2*length5^0-2*i6^0 New rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 2+2*length5^post18 Applied deletion Removed the following rules: 50 Applied chaining First rule: l9 -> l7 : TRUE, cost: 2 Second rule: l7 -> [16] : n1 >= 0, cost: NONTERM New rule: l9 -> [16] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 51 Applied chaining First rule: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 Second rule: l9 -> [17] : -1+n2 >= 0, cost: NONTERM New rule: l4 -> [17] : length5^0-i6^0 <= 0, cost: NONTERM Applied deletion Removed the following rules: 53 Chained accelerated rules with incoming rules Start location: l13 43: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 56: l4 -> [17] : length5^0-i6^0 <= 0, cost: NONTERM 48: l7 -> [14] : TRUE, cost: NONTERM 45: l9 -> l7 : TRUE, cost: 2 55: l9 -> [16] : TRUE, cost: NONTERM 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 54: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 2+2*length5^post18 Eliminating location l7 by chaining: Applied chaining First rule: l9 -> l7 : TRUE, cost: 2 Second rule: l7 -> [14] : TRUE, cost: NONTERM New rule: l9 -> [14] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 45 48 Eliminated locations on linear paths Start location: l13 43: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 56: l4 -> [17] : length5^0-i6^0 <= 0, cost: NONTERM 55: l9 -> [16] : TRUE, cost: NONTERM 57: l9 -> [14] : TRUE, cost: NONTERM 36: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 54: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 2+2*length5^post18 Eliminating location l4 by chaining: Applied chaining First rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Second rule: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 New rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, (0 == 0 /\ length5^post18 <= 0), cost: 4 Applied simplification Original rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, (0 == 0 /\ length5^post18 <= 0), cost: 4 New rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, length5^post18 <= 0, cost: 4 Applied chaining First rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, 0 == 0, cost: 2 Second rule: l4 -> [17] : length5^0-i6^0 <= 0, cost: NONTERM New rule: l13 -> [17] : (0 == 0 /\ length5^post18 <= 0), cost: NONTERM Applied simplification Original rule: l13 -> [17] : (0 == 0 /\ length5^post18 <= 0), cost: NONTERM New rule: l13 -> [17] : length5^post18 <= 0, cost: NONTERM Applied chaining First rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 2+2*length5^post18 Second rule: l4 -> l9 : length5^0-i6^0 <= 0, cost: 2 New rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, (0 <= 0 /\ -1+length5^post18 >= 0), cost: 4+2*length5^post18 Applied simplification Original rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, (0 <= 0 /\ -1+length5^post18 >= 0), cost: 4+2*length5^post18 New rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 4+2*length5^post18 Applied chaining First rule: l13 -> l4 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 2+2*length5^post18 Second rule: l4 -> [17] : length5^0-i6^0 <= 0, cost: NONTERM New rule: l13 -> [17] : (0 <= 0 /\ -1+length5^post18 >= 0), cost: NONTERM Applied simplification Original rule: l13 -> [17] : (0 <= 0 /\ -1+length5^post18 >= 0), cost: NONTERM New rule: l13 -> [17] : -1+length5^post18 >= 0, cost: NONTERM Applied deletion Removed the following rules: 36 43 54 56 Eliminated locations on tree-shaped paths Start location: l13 55: l9 -> [16] : TRUE, cost: NONTERM 57: l9 -> [14] : TRUE, cost: NONTERM 58: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, length5^post18 <= 0, cost: 4 59: l13 -> [17] : length5^post18 <= 0, cost: NONTERM 60: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 4+2*length5^post18 61: l13 -> [17] : -1+length5^post18 >= 0, cost: NONTERM Eliminating location l9 by chaining: Applied chaining First rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, length5^post18 <= 0, cost: 4 Second rule: l9 -> [16] : TRUE, cost: NONTERM New rule: l13 -> [16] : length5^post18 <= 0, cost: NONTERM Applied chaining First rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=0, s^0'=length5^post18, length5^post18 <= 0, cost: 4 Second rule: l9 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : length5^post18 <= 0, cost: NONTERM Applied chaining First rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 4+2*length5^post18 Second rule: l9 -> [16] : TRUE, cost: NONTERM New rule: l13 -> [16] : -1+length5^post18 >= 0, cost: NONTERM Applied chaining First rule: l13 -> l9 : tmp^0'=length5^post18, length5^0'=length5^post18, i6^0'=length5^post18, tmp___09^0'=tmp___09^post17, s^0'=length5^post18, -1+length5^post18 >= 0, cost: 4+2*length5^post18 Second rule: l9 -> [14] : TRUE, cost: NONTERM New rule: l13 -> [14] : -1+length5^post18 >= 0, cost: NONTERM Applied deletion Removed the following rules: 55 57 58 60 Eliminated locations on tree-shaped paths Start location: l13 59: l13 -> [17] : length5^post18 <= 0, cost: NONTERM 61: l13 -> [17] : -1+length5^post18 >= 0, cost: NONTERM 62: l13 -> [16] : length5^post18 <= 0, cost: NONTERM 63: l13 -> [14] : length5^post18 <= 0, cost: NONTERM 64: l13 -> [16] : -1+length5^post18 >= 0, cost: NONTERM 65: l13 -> [14] : -1+length5^post18 >= 0, cost: NONTERM Removed duplicate rules (ignoring updates) Start location: l13 63: l13 -> [14] : length5^post18 <= 0, cost: NONTERM 65: l13 -> [14] : -1+length5^post18 >= 0, cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 63 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: length5^post18 <= 0