WORST_CASE(Omega(0),?) Initial ITS Start location: l9 0: l0 -> l1 : b^0'=b^post0, a^0'=a^post0, b5^0'=b5^post0, a4^0'=a4^post0, ret_complex6^0'=ret_complex6^post0, answer^0'=answer^post0, (a^0-a^post0 == 0 /\ -b5^post0+b5^0 == 0 /\ -a4^post0+a4^0 == 0 /\ 30-a4^0 <= 0 /\ -1+ret_complex6^post0 == 0 /\ b^0-b^post0 == 0 /\ answer^post0-ret_complex6^post0 == 0), cost: 1 1: l0 -> l2 : b^0'=b^post1, a^0'=a^post1, b5^0'=b5^post1, a4^0'=a4^post1, ret_complex6^0'=ret_complex6^post1, answer^0'=answer^post1, (-29+a4^0 <= 0 /\ -ret_complex6^post1+ret_complex6^0 == 0 /\ -a4^post1+a4^0 == 0 /\ -answer^post1+answer^0 == 0 /\ b^0-b^post1 == 0 /\ b5^0-b5^post1 == 0 /\ a^0-a^post1 == 0), cost: 1 3: l2 -> l4 : b^0'=b^post3, a^0'=a^post3, b5^0'=b5^post3, a4^0'=a4^post3, ret_complex6^0'=ret_complex6^post3, answer^0'=answer^post3, (a4^0-a4^post3 == 0 /\ -answer^post3+answer^0 == 0 /\ b5^0-b5^post3 == 0 /\ a^0-a^post3 == 0 /\ b^0-b^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0), cost: 1 2: l3 -> l0 : b^0'=b^post2, a^0'=a^post2, b5^0'=b5^post2, a4^0'=a4^post2, ret_complex6^0'=ret_complex6^post2, answer^0'=answer^post2, (-answer^post2+answer^0 == 0 /\ a4^0-a4^post2 == 0 /\ a^0-a^post2 == 0 /\ b^0-b^post2 == 0 /\ b5^0-b5^post2 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0), cost: 1 10: l4 -> l3 : b^0'=b^post10, a^0'=a^post10, b5^0'=b5^post10, a4^0'=a4^post10, ret_complex6^0'=ret_complex6^post10, answer^0'=answer^post10, (-2-a4^0+a4^post10 == 0 /\ b^0-b^post10 == 0 /\ -a^post10+a^0 == 0 /\ -answer^post10+answer^0 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -b5^0+a4^0 <= 0 /\ 10-b5^0+b5^post10 == 0), cost: 1 11: l4 -> l7 : b^0'=b^post11, a^0'=a^post11, b5^0'=b5^post11, a4^0'=a4^post11, ret_complex6^0'=ret_complex6^post11, answer^0'=answer^post11, (1+b5^0-a4^0 <= 0 /\ a4^0-a4^post11 == 0 /\ -answer^post11+answer^0 == 0 /\ b^0-b^post11 == 0 /\ b5^0-b5^post11 == 0 /\ a^0-a^post11 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0), cost: 1 4: l5 -> l2 : b^0'=b^post4, a^0'=a^post4, b5^0'=b5^post4, a4^0'=a4^post4, ret_complex6^0'=ret_complex6^post4, answer^0'=answer^post4, (b5^0-b5^post4 == 0 /\ 13-b5^0 <= 0 /\ -a^post4+a^0 == 0 /\ -1-a4^0+a4^post4 == 0 /\ b^0-b^post4 == 0 /\ -answer^post4+answer^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0), cost: 1 5: l5 -> l2 : b^0'=b^post5, a^0'=a^post5, b5^0'=b5^post5, a4^0'=a4^post5, ret_complex6^0'=ret_complex6^post5, answer^0'=answer^post5, (-10-a4^0+a4^post5 == 0 /\ -12+b5^0 <= 0 /\ -answer^post5+answer^0 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ a^0-a^post5 == 0), cost: 1 6: l6 -> l2 : b^0'=b^post6, a^0'=a^post6, b5^0'=b5^post6, a4^0'=a4^post6, ret_complex6^0'=ret_complex6^post6, answer^0'=answer^post6, (b^0-b^post6 == 0 /\ -answer^post6+answer^0 == 0 /\ -b5^post6+b5^0 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ a^0-a^post6 == 0 /\ -9+b5^0 <= 0 /\ -1+a4^post6-a4^0 == 0), cost: 1 7: l6 -> l5 : b^0'=b^post7, a^0'=a^post7, b5^0'=b5^post7, a4^0'=a4^post7, ret_complex6^0'=ret_complex6^post7, answer^0'=answer^post7, (answer^0-answer^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ b^0-b^post7 == 0 /\ b5^0-b5^post7 == 0 /\ a^0-a^post7 == 0 /\ 10-b5^0 <= 0 /\ -a4^post7+a4^0 == 0), cost: 1 8: l7 -> l6 : b^0'=b^post8, a^0'=a^post8, b5^0'=b5^post8, a4^0'=a4^post8, ret_complex6^0'=ret_complex6^post8, answer^0'=answer^post8, (-ret_complex6^post8+ret_complex6^0 == 0 /\ -5+b5^0 <= 0 /\ -answer^post8+answer^0 == 0 /\ -a4^post8+a4^0 == 0 /\ -2-b5^0+b5^post8 == 0 /\ a^0-a^post8 == 0 /\ b^0-b^post8 == 0), cost: 1 9: l7 -> l6 : b^0'=b^post9, a^0'=a^post9, b5^0'=b5^post9, a4^0'=a4^post9, ret_complex6^0'=ret_complex6^post9, answer^0'=answer^post9, (0 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ -a4^post9+a4^0 == 0 /\ a^0-a^post9 == 0 /\ -answer^post9+answer^0 == 0 /\ 6-b5^0 <= 0 /\ -b^post9+b^0 == 0), cost: 1 12: l8 -> l3 : b^0'=b^post12, a^0'=a^post12, b5^0'=b5^post12, a4^0'=a4^post12, ret_complex6^0'=ret_complex6^post12, answer^0'=answer^post12, (-1+b^post12 == 0 /\ answer^post12 == 0 /\ a4^post12-a^post12 == 0 /\ -1+a^post12 == 0 /\ b5^post12-b^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0), cost: 1 13: l9 -> l8 : b^0'=b^post13, a^0'=a^post13, b5^0'=b5^post13, a4^0'=a4^post13, ret_complex6^0'=ret_complex6^post13, answer^0'=answer^post13, (b^0-b^post13 == 0 /\ a^0-a^post13 == 0 /\ -b5^post13+b5^0 == 0 /\ -answer^post13+answer^0 == 0 /\ -a4^post13+a4^0 == 0 /\ ret_complex6^0-ret_complex6^post13 == 0), cost: 1 Removed unreachable rules and leafs Start location: l9 1: l0 -> l2 : b^0'=b^post1, a^0'=a^post1, b5^0'=b5^post1, a4^0'=a4^post1, ret_complex6^0'=ret_complex6^post1, answer^0'=answer^post1, (-29+a4^0 <= 0 /\ -ret_complex6^post1+ret_complex6^0 == 0 /\ -a4^post1+a4^0 == 0 /\ -answer^post1+answer^0 == 0 /\ b^0-b^post1 == 0 /\ b5^0-b5^post1 == 0 /\ a^0-a^post1 == 0), cost: 1 3: l2 -> l4 : b^0'=b^post3, a^0'=a^post3, b5^0'=b5^post3, a4^0'=a4^post3, ret_complex6^0'=ret_complex6^post3, answer^0'=answer^post3, (a4^0-a4^post3 == 0 /\ -answer^post3+answer^0 == 0 /\ b5^0-b5^post3 == 0 /\ a^0-a^post3 == 0 /\ b^0-b^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0), cost: 1 2: l3 -> l0 : b^0'=b^post2, a^0'=a^post2, b5^0'=b5^post2, a4^0'=a4^post2, ret_complex6^0'=ret_complex6^post2, answer^0'=answer^post2, (-answer^post2+answer^0 == 0 /\ a4^0-a4^post2 == 0 /\ a^0-a^post2 == 0 /\ b^0-b^post2 == 0 /\ b5^0-b5^post2 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0), cost: 1 10: l4 -> l3 : b^0'=b^post10, a^0'=a^post10, b5^0'=b5^post10, a4^0'=a4^post10, ret_complex6^0'=ret_complex6^post10, answer^0'=answer^post10, (-2-a4^0+a4^post10 == 0 /\ b^0-b^post10 == 0 /\ -a^post10+a^0 == 0 /\ -answer^post10+answer^0 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -b5^0+a4^0 <= 0 /\ 10-b5^0+b5^post10 == 0), cost: 1 11: l4 -> l7 : b^0'=b^post11, a^0'=a^post11, b5^0'=b5^post11, a4^0'=a4^post11, ret_complex6^0'=ret_complex6^post11, answer^0'=answer^post11, (1+b5^0-a4^0 <= 0 /\ a4^0-a4^post11 == 0 /\ -answer^post11+answer^0 == 0 /\ b^0-b^post11 == 0 /\ b5^0-b5^post11 == 0 /\ a^0-a^post11 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0), cost: 1 4: l5 -> l2 : b^0'=b^post4, a^0'=a^post4, b5^0'=b5^post4, a4^0'=a4^post4, ret_complex6^0'=ret_complex6^post4, answer^0'=answer^post4, (b5^0-b5^post4 == 0 /\ 13-b5^0 <= 0 /\ -a^post4+a^0 == 0 /\ -1-a4^0+a4^post4 == 0 /\ b^0-b^post4 == 0 /\ -answer^post4+answer^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0), cost: 1 5: l5 -> l2 : b^0'=b^post5, a^0'=a^post5, b5^0'=b5^post5, a4^0'=a4^post5, ret_complex6^0'=ret_complex6^post5, answer^0'=answer^post5, (-10-a4^0+a4^post5 == 0 /\ -12+b5^0 <= 0 /\ -answer^post5+answer^0 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ a^0-a^post5 == 0), cost: 1 6: l6 -> l2 : b^0'=b^post6, a^0'=a^post6, b5^0'=b5^post6, a4^0'=a4^post6, ret_complex6^0'=ret_complex6^post6, answer^0'=answer^post6, (b^0-b^post6 == 0 /\ -answer^post6+answer^0 == 0 /\ -b5^post6+b5^0 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ a^0-a^post6 == 0 /\ -9+b5^0 <= 0 /\ -1+a4^post6-a4^0 == 0), cost: 1 7: l6 -> l5 : b^0'=b^post7, a^0'=a^post7, b5^0'=b5^post7, a4^0'=a4^post7, ret_complex6^0'=ret_complex6^post7, answer^0'=answer^post7, (answer^0-answer^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ b^0-b^post7 == 0 /\ b5^0-b5^post7 == 0 /\ a^0-a^post7 == 0 /\ 10-b5^0 <= 0 /\ -a4^post7+a4^0 == 0), cost: 1 8: l7 -> l6 : b^0'=b^post8, a^0'=a^post8, b5^0'=b5^post8, a4^0'=a4^post8, ret_complex6^0'=ret_complex6^post8, answer^0'=answer^post8, (-ret_complex6^post8+ret_complex6^0 == 0 /\ -5+b5^0 <= 0 /\ -answer^post8+answer^0 == 0 /\ -a4^post8+a4^0 == 0 /\ -2-b5^0+b5^post8 == 0 /\ a^0-a^post8 == 0 /\ b^0-b^post8 == 0), cost: 1 9: l7 -> l6 : b^0'=b^post9, a^0'=a^post9, b5^0'=b5^post9, a4^0'=a4^post9, ret_complex6^0'=ret_complex6^post9, answer^0'=answer^post9, (0 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ -a4^post9+a4^0 == 0 /\ a^0-a^post9 == 0 /\ -answer^post9+answer^0 == 0 /\ 6-b5^0 <= 0 /\ -b^post9+b^0 == 0), cost: 1 12: l8 -> l3 : b^0'=b^post12, a^0'=a^post12, b5^0'=b5^post12, a4^0'=a4^post12, ret_complex6^0'=ret_complex6^post12, answer^0'=answer^post12, (-1+b^post12 == 0 /\ answer^post12 == 0 /\ a4^post12-a^post12 == 0 /\ -1+a^post12 == 0 /\ b5^post12-b^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0), cost: 1 13: l9 -> l8 : b^0'=b^post13, a^0'=a^post13, b5^0'=b5^post13, a4^0'=a4^post13, ret_complex6^0'=ret_complex6^post13, answer^0'=answer^post13, (b^0-b^post13 == 0 /\ a^0-a^post13 == 0 /\ -b5^post13+b5^0 == 0 /\ -answer^post13+answer^0 == 0 /\ -a4^post13+a4^0 == 0 /\ ret_complex6^0-ret_complex6^post13 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l2 : b^0'=b^post1, a^0'=a^post1, b5^0'=b5^post1, a4^0'=a4^post1, ret_complex6^0'=ret_complex6^post1, answer^0'=answer^post1, (-29+a4^0 <= 0 /\ -ret_complex6^post1+ret_complex6^0 == 0 /\ -a4^post1+a4^0 == 0 /\ -answer^post1+answer^0 == 0 /\ b^0-b^post1 == 0 /\ b5^0-b5^post1 == 0 /\ a^0-a^post1 == 0), cost: 1 New rule: l0 -> l2 : -29+a4^0 <= 0, cost: 1 Applied preprocessing Original rule: l3 -> l0 : b^0'=b^post2, a^0'=a^post2, b5^0'=b5^post2, a4^0'=a4^post2, ret_complex6^0'=ret_complex6^post2, answer^0'=answer^post2, (-answer^post2+answer^0 == 0 /\ a4^0-a4^post2 == 0 /\ a^0-a^post2 == 0 /\ b^0-b^post2 == 0 /\ b5^0-b5^post2 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0), cost: 1 New rule: l3 -> l0 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l4 : b^0'=b^post3, a^0'=a^post3, b5^0'=b5^post3, a4^0'=a4^post3, ret_complex6^0'=ret_complex6^post3, answer^0'=answer^post3, (a4^0-a4^post3 == 0 /\ -answer^post3+answer^0 == 0 /\ b5^0-b5^post3 == 0 /\ a^0-a^post3 == 0 /\ b^0-b^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0), cost: 1 New rule: l2 -> l4 : TRUE, cost: 1 Applied preprocessing Original rule: l5 -> l2 : b^0'=b^post4, a^0'=a^post4, b5^0'=b5^post4, a4^0'=a4^post4, ret_complex6^0'=ret_complex6^post4, answer^0'=answer^post4, (b5^0-b5^post4 == 0 /\ 13-b5^0 <= 0 /\ -a^post4+a^0 == 0 /\ -1-a4^0+a4^post4 == 0 /\ b^0-b^post4 == 0 /\ -answer^post4+answer^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0), cost: 1 New rule: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 Applied preprocessing Original rule: l5 -> l2 : b^0'=b^post5, a^0'=a^post5, b5^0'=b5^post5, a4^0'=a4^post5, ret_complex6^0'=ret_complex6^post5, answer^0'=answer^post5, (-10-a4^0+a4^post5 == 0 /\ -12+b5^0 <= 0 /\ -answer^post5+answer^0 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ a^0-a^post5 == 0), cost: 1 New rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l2 : b^0'=b^post6, a^0'=a^post6, b5^0'=b5^post6, a4^0'=a4^post6, ret_complex6^0'=ret_complex6^post6, answer^0'=answer^post6, (b^0-b^post6 == 0 /\ -answer^post6+answer^0 == 0 /\ -b5^post6+b5^0 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ a^0-a^post6 == 0 /\ -9+b5^0 <= 0 /\ -1+a4^post6-a4^0 == 0), cost: 1 New rule: l6 -> l2 : a4^0'=1+a4^0, -9+b5^0 <= 0, cost: 1 Applied preprocessing Original rule: l6 -> l5 : b^0'=b^post7, a^0'=a^post7, b5^0'=b5^post7, a4^0'=a4^post7, ret_complex6^0'=ret_complex6^post7, answer^0'=answer^post7, (answer^0-answer^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ b^0-b^post7 == 0 /\ b5^0-b5^post7 == 0 /\ a^0-a^post7 == 0 /\ 10-b5^0 <= 0 /\ -a4^post7+a4^0 == 0), cost: 1 New rule: l6 -> l5 : -10+b5^0 >= 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : b^0'=b^post8, a^0'=a^post8, b5^0'=b5^post8, a4^0'=a4^post8, ret_complex6^0'=ret_complex6^post8, answer^0'=answer^post8, (-ret_complex6^post8+ret_complex6^0 == 0 /\ -5+b5^0 <= 0 /\ -answer^post8+answer^0 == 0 /\ -a4^post8+a4^0 == 0 /\ -2-b5^0+b5^post8 == 0 /\ a^0-a^post8 == 0 /\ b^0-b^post8 == 0), cost: 1 New rule: l7 -> l6 : b5^0'=2+b5^0, -5+b5^0 <= 0, cost: 1 Applied preprocessing Original rule: l7 -> l6 : b^0'=b^post9, a^0'=a^post9, b5^0'=b5^post9, a4^0'=a4^post9, ret_complex6^0'=ret_complex6^post9, answer^0'=answer^post9, (0 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ -a4^post9+a4^0 == 0 /\ a^0-a^post9 == 0 /\ -answer^post9+answer^0 == 0 /\ 6-b5^0 <= 0 /\ -b^post9+b^0 == 0), cost: 1 New rule: l7 -> l6 : b5^0'=b5^post9, -6+b5^0 >= 0, cost: 1 Applied preprocessing Original rule: l4 -> l3 : b^0'=b^post10, a^0'=a^post10, b5^0'=b5^post10, a4^0'=a4^post10, ret_complex6^0'=ret_complex6^post10, answer^0'=answer^post10, (-2-a4^0+a4^post10 == 0 /\ b^0-b^post10 == 0 /\ -a^post10+a^0 == 0 /\ -answer^post10+answer^0 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -b5^0+a4^0 <= 0 /\ 10-b5^0+b5^post10 == 0), cost: 1 New rule: l4 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 1 Applied preprocessing Original rule: l4 -> l7 : b^0'=b^post11, a^0'=a^post11, b5^0'=b5^post11, a4^0'=a4^post11, ret_complex6^0'=ret_complex6^post11, answer^0'=answer^post11, (1+b5^0-a4^0 <= 0 /\ a4^0-a4^post11 == 0 /\ -answer^post11+answer^0 == 0 /\ b^0-b^post11 == 0 /\ b5^0-b5^post11 == 0 /\ a^0-a^post11 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0), cost: 1 New rule: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l3 : b^0'=b^post12, a^0'=a^post12, b5^0'=b5^post12, a4^0'=a4^post12, ret_complex6^0'=ret_complex6^post12, answer^0'=answer^post12, (-1+b^post12 == 0 /\ answer^post12 == 0 /\ a4^post12-a^post12 == 0 /\ -1+a^post12 == 0 /\ b5^post12-b^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0), cost: 1 New rule: l8 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 1 Applied preprocessing Original rule: l9 -> l8 : b^0'=b^post13, a^0'=a^post13, b5^0'=b5^post13, a4^0'=a4^post13, ret_complex6^0'=ret_complex6^post13, answer^0'=answer^post13, (b^0-b^post13 == 0 /\ a^0-a^post13 == 0 /\ -b5^post13+b5^0 == 0 /\ -answer^post13+answer^0 == 0 /\ -a4^post13+a4^0 == 0 /\ ret_complex6^0-ret_complex6^post13 == 0), cost: 1 New rule: l9 -> l8 : TRUE, cost: 1 Simplified rules Start location: l9 14: l0 -> l2 : -29+a4^0 <= 0, cost: 1 16: l2 -> l4 : TRUE, cost: 1 15: l3 -> l0 : TRUE, cost: 1 23: l4 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 1 24: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 19: l6 -> l2 : a4^0'=1+a4^0, -9+b5^0 <= 0, cost: 1 20: l6 -> l5 : -10+b5^0 >= 0, cost: 1 21: l7 -> l6 : b5^0'=2+b5^0, -5+b5^0 <= 0, cost: 1 22: l7 -> l6 : b5^0'=b5^post9, -6+b5^0 >= 0, cost: 1 25: l8 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 1 26: l9 -> l8 : TRUE, cost: 1 Eliminating location l8 by chaining: Applied chaining First rule: l9 -> l8 : TRUE, cost: 1 Second rule: l8 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 1 New rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied deletion Removed the following rules: 25 26 Eliminating location l0 by chaining: Applied chaining First rule: l3 -> l0 : TRUE, cost: 1 Second rule: l0 -> l2 : -29+a4^0 <= 0, cost: 1 New rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Applied deletion Removed the following rules: 14 15 Eliminated locations on linear paths Start location: l9 16: l2 -> l4 : TRUE, cost: 1 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 23: l4 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 1 24: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 19: l6 -> l2 : a4^0'=1+a4^0, -9+b5^0 <= 0, cost: 1 20: l6 -> l5 : -10+b5^0 >= 0, cost: 1 21: l7 -> l6 : b5^0'=2+b5^0, -5+b5^0 <= 0, cost: 1 22: l7 -> l6 : b5^0'=b5^post9, -6+b5^0 >= 0, cost: 1 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Eliminating location l4 by chaining: Applied chaining First rule: l2 -> l4 : TRUE, cost: 1 Second rule: l4 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 1 New rule: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 Applied chaining First rule: l2 -> l4 : TRUE, cost: 1 Second rule: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 New rule: l2 -> l7 : 1+b5^0-a4^0 <= 0, cost: 2 Applied deletion Removed the following rules: 16 23 24 Eliminating location l6 by chaining: Applied chaining First rule: l7 -> l6 : b5^0'=2+b5^0, -5+b5^0 <= 0, cost: 1 Second rule: l6 -> l2 : a4^0'=1+a4^0, -9+b5^0 <= 0, cost: 1 New rule: l7 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (-5+b5^0 <= 0 /\ -7+b5^0 <= 0), cost: 2 Applied simplification Original rule: l7 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (-5+b5^0 <= 0 /\ -7+b5^0 <= 0), cost: 2 New rule: l7 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, -5+b5^0 <= 0, cost: 2 Applied chaining First rule: l7 -> l6 : b5^0'=b5^post9, -6+b5^0 >= 0, cost: 1 Second rule: l6 -> l2 : a4^0'=1+a4^0, -9+b5^0 <= 0, cost: 1 New rule: l7 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (-9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 2 Applied chaining First rule: l7 -> l6 : b5^0'=b5^post9, -6+b5^0 >= 0, cost: 1 Second rule: l6 -> l5 : -10+b5^0 >= 0, cost: 1 New rule: l7 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ -6+b5^0 >= 0), cost: 2 Applied deletion Removed the following rules: 19 20 21 22 Eliminated locations on tree-shaped paths Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 30: l2 -> l7 : 1+b5^0-a4^0 <= 0, cost: 2 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 31: l7 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, -5+b5^0 <= 0, cost: 2 32: l7 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (-9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 2 33: l7 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ -6+b5^0 >= 0), cost: 2 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Eliminating location l7 by chaining: Applied chaining First rule: l2 -> l7 : 1+b5^0-a4^0 <= 0, cost: 2 Second rule: l7 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, -5+b5^0 <= 0, cost: 2 New rule: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 Applied chaining First rule: l2 -> l7 : 1+b5^0-a4^0 <= 0, cost: 2 Second rule: l7 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (-9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 2 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 Applied chaining First rule: l2 -> l7 : 1+b5^0-a4^0 <= 0, cost: 2 Second rule: l7 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ -6+b5^0 >= 0), cost: 2 New rule: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 Applied deletion Removed the following rules: 30 31 32 33 Eliminated locations on tree-shaped paths Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 34: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 35: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 36: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied acceleration Original rule: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 New rule: l2 -> l2 : b5^0'=2*n+b5^0, a4^0'=n+a4^0, (n >= 0 /\ 7-2*n-b5^0 >= 0 /\ -n-b5^0+a4^0 >= 0), cost: 4*n Sub-proof via acceration calculus written to file:///tmp/tmpnam_gdfpLA.txt Applied instantiation Original rule: l2 -> l2 : b5^0'=2*n+b5^0, a4^0'=n+a4^0, (n >= 0 /\ 7-2*n-b5^0 >= 0 /\ -n-b5^0+a4^0 >= 0), cost: 4*n New rule: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (0 >= 0 /\ 7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 Applied acceleration Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (9-b5^post9 >= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 Sub-proof via acceration calculus written to file:///tmp/tmpnam_KkMCec.txt Applied nonterm Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 New rule: l2 -> [10] : (9-b5^post9 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_KKkBeP.txt Applied chaining First rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 New rule: l2 -> l2 : b5^0'=2+b5^post9, a4^0'=2+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0), cost: 8 Applied acceleration Original rule: l2 -> l2 : b5^0'=2+b5^post9, a4^0'=2+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0), cost: 8 New rule: l2 -> l2 : b5^0'=2+b5^post9, a4^0'=a4^0+2*n1, (-1+n1 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0 /\ -4+b5^post9 >= 0), cost: 8*n1 Sub-proof via acceration calculus written to file:///tmp/tmpnam_hOFJNC.txt Applied nonterm Original rule: l2 -> l2 : b5^0'=2+b5^post9, a4^0'=2+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0), cost: 8 New rule: l2 -> [10] : (-2+b5^0-b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_OeaChj.txt Applied chaining First rule: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 Second rule: l2 -> [10] : (-2+b5^0-b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM Applied chaining First rule: l2 -> l2 : b5^0'=2+b5^0, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -5+b5^0 <= 0), cost: 4 Second rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=2+a4^0, (2+b5^0-a4^0 <= 0 /\ -4+b5^0 >= 0 /\ -9+b5^post9 <= 0 /\ -5+b5^0 <= 0), cost: 8 Applied acceleration Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=2+a4^0, (2+b5^0-a4^0 <= 0 /\ -4+b5^0 >= 0 /\ -9+b5^post9 <= 0 /\ -5+b5^0 <= 0), cost: 8 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=a4^0+2*n2, (9-b5^post9 >= 0 /\ -1+n2 >= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ 5-b5^post9 >= 0 /\ -2-b5^0+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: 8*n2 Sub-proof via acceration calculus written to file:///tmp/tmpnam_hNoaFe.txt Applied nonterm Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=2+a4^0, (2+b5^0-a4^0 <= 0 /\ -4+b5^0 >= 0 /\ -9+b5^post9 <= 0 /\ -5+b5^0 <= 0), cost: 8 New rule: l2 -> [10] : (9-b5^post9 >= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -2-b5^0+b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_CpOCHf.txt Applied chaining First rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l2 -> [10] : (9-b5^post9 >= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -2-b5^0+b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM New rule: l2 -> [10] : (0 <= 0 /\ 9-b5^post9 >= 0 /\ -2 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0 /\ -4+b5^post9 >= 0 /\ -1+a4^0-b5^post9 >= 0), cost: NONTERM Applied simplification Original rule: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (0 >= 0 /\ 7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 New rule: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 Applied simplification Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (9-b5^post9 >= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 Applied simplification Original rule: l2 -> [10] : (9-b5^post9 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM New rule: l2 -> [10] : (-1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM Applied simplification Original rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM Applied simplification Original rule: l2 -> [10] : (9-b5^post9 >= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -2-b5^0+b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM New rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM Applied simplification Original rule: l2 -> [10] : (0 <= 0 /\ 9-b5^post9 >= 0 /\ -2 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0 /\ -4+b5^post9 >= 0 /\ -1+a4^0-b5^post9 >= 0), cost: NONTERM New rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: NONTERM Applied deletion Removed the following rules: 34 35 Accelerated simple loops Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 36: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 40: l2 -> [10] : (-2+b5^0-b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0), cost: NONTERM 44: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 45: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 46: l2 -> [10] : (-1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM 47: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM 48: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM 49: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: NONTERM 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> [10] : (-2+b5^0-b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l5 -> [10] : (9-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (-2+b5^0-b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 New rule: l5 -> l2 : b5^0'=20-b5^0+2*a4^0, a4^0'=20-b5^0+2*a4^0, (10-b5^0+a4^0 >= 0 /\ -13+b5^0-2*a4^0 >= 0), cost: 41-4*b5^0+4*a4^0 Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: -4*b5^0+4*a4^0 New rule: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 Applied chaining First rule: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 Second rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 New rule: l5 -> l2 : b5^0'=b5^post9, a4^0'=1+n0+a4^0, (-1+n0 >= 0 /\ -b5^0+a4^0 >= 0 /\ -9+b5^post9 <= 0 /\ -13+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 1+4*n0 Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 New rule: l5 -> l2 : b5^0'=b5^post9, a4^0'=10+n0+a4^0, (9-b5^0+a4^0 >= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -12+b5^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 1+4*n0 Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 4*n0 New rule: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> [10] : (-1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM New rule: l5 -> [10] : (9-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (-1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ b5^0-b5^post9 <= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l5 -> [10] : (8-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ 5-b5^post9 >= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM New rule: l5 -> [10] : (8-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (-2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0 /\ b5^0-b5^post9 <= 0 /\ -b5^0+b5^post9 <= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM Applied chaining First rule: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 Second rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: NONTERM New rule: l5 -> [10] : (b5^0-a4^0 <= 0 /\ -13+b5^0 >= 0), cost: NONTERM Applied chaining First rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 Second rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: NONTERM New rule: l5 -> [10] : (-9+b5^0-a4^0 <= 0 /\ -12+b5^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -5+b5^post9 <= 0 /\ -4+b5^post9 >= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 40 44 45 46 47 48 49 Chained accelerated rules with incoming rules Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 36: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 53: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 56: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 17: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 18: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 50: l5 -> [10] : (9-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 52: l5 -> l2 : b5^0'=20-b5^0+2*a4^0, a4^0'=20-b5^0+2*a4^0, (10-b5^0+a4^0 >= 0 /\ -13+b5^0-2*a4^0 >= 0), cost: 41-4*b5^0+4*a4^0 54: l5 -> l2 : b5^0'=b5^post9, a4^0'=1+n0+a4^0, (-1+n0 >= 0 /\ -b5^0+a4^0 >= 0 /\ -9+b5^post9 <= 0 /\ -13+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 1+4*n0 55: l5 -> l2 : b5^0'=b5^post9, a4^0'=10+n0+a4^0, (9-b5^0+a4^0 >= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -12+b5^0 <= 0 /\ -9+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 1+4*n0 57: l5 -> [10] : (9-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 59: l5 -> [10] : (8-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 61: l5 -> [10] : (8-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 63: l5 -> [10] : (b5^0-a4^0 <= 0 /\ -13+b5^0 >= 0), cost: NONTERM 64: l5 -> [10] : (-9+b5^0-a4^0 <= 0 /\ -12+b5^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Eliminating location l5 by chaining: Applied chaining First rule: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l5 -> l2 : a4^0'=1+a4^0, -13+b5^0 >= 0, cost: 1 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: 5 Applied simplification Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: 5 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: 5 Applied chaining First rule: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l5 -> l2 : a4^0'=10+a4^0, -12+b5^0 <= 0, cost: 1 New rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=10+a4^0, (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 5 Applied chaining First rule: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l5 -> [10] : (b5^0-a4^0 <= 0 /\ -13+b5^0 >= 0), cost: NONTERM New rule: l2 -> [10] : (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM Applied simplification Original rule: l2 -> [10] : (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM New rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM Applied chaining First rule: l2 -> l5 : b5^0'=b5^post9, (-10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 4 Second rule: l5 -> [10] : (-9+b5^0-a4^0 <= 0 /\ -12+b5^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM New rule: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -9-a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: NONTERM Applied simplification Original rule: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -9-a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: NONTERM New rule: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 17 18 36 50 52 54 55 57 59 61 63 64 Eliminated locations on tree-shaped paths Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 66: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: 5 67: l2 -> l2 : b5^0'=b5^post9, a4^0'=10+a4^0, (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 5 68: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 69: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 53: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 56: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied nonterm Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=1+a4^0, (1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: 5 New rule: l2 -> [11] : (-1-b5^0+b5^post9 <= 0 /\ -1+n4 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_mFMlib.txt Applied nonterm Original rule: l2 -> l2 : b5^0'=b5^post9, a4^0'=10+a4^0, (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: 5 New rule: l2 -> [11] : (-10+b5^post9 >= 0 /\ 12-b5^post9 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_leLKdK.txt Applied simplification Original rule: l2 -> [11] : (-1-b5^0+b5^post9 <= 0 /\ -1+n4 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM New rule: l2 -> [11] : (-1-b5^0+b5^post9 <= 0 /\ -1+n4 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM Applied simplification Original rule: l2 -> [11] : (-10+b5^post9 >= 0 /\ 12-b5^post9 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l2 -> [11] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM Applied deletion Removed the following rules: 66 67 Accelerated simple loops Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 68: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 69: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 72: l2 -> [11] : (-1-b5^0+b5^post9 <= 0 /\ -1+n4 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 73: l2 -> [11] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 53: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 56: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [11] : (-1-b5^0+b5^post9 <= 0 /\ -1+n4 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM New rule: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [11] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -1+n5 >= 0), cost: NONTERM New rule: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM Applied deletion Removed the following rules: 72 73 Chained accelerated rules with incoming rules Start location: l9 29: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 68: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 69: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 28: l3 -> l2 : -29+a4^0 <= 0, cost: 2 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 53: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 56: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 74: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM 75: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Eliminating location l2 by chaining: Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 New rule: l3 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, (-29+a4^0 <= 0 /\ -b5^0+a4^0 <= 0), cost: 4 Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM New rule: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : -29+a4^0 <= 0, cost: 2 Second rule: l2 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM New rule: l3 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM Applied chaining First rule: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 Second rule: l2 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, -b5^0+a4^0 <= 0, cost: 2 New rule: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (0 <= 0 /\ 7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 Applied simplification Original rule: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (0 <= 0 /\ 7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 New rule: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 Applied partial deletion Original rule: l3 -> l2 : b5^0'=-b5^0+2*a4^0, a4^0'=-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 New rule: l3 -> [12] : (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 Applied partial deletion Original rule: l3 -> l2 : b5^0'=b5^post9, a4^0'=n0+a4^0, (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 New rule: l3 -> [12] : (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 Applied deletion Removed the following rules: 28 29 53 56 68 69 Eliminated locations on tree-shaped paths Start location: l9 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 74: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM 75: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM 76: l3 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, (-29+a4^0 <= 0 /\ -b5^0+a4^0 <= 0), cost: 4 77: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 78: l3 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 79: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 80: l3 -> [12] : (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 2-4*b5^0+4*a4^0 81: l3 -> [12] : (-29+a4^0 <= 0 /\ -1+n0 >= 0 /\ -1-b5^0+b5^post9 <= 0 /\ -9+b5^post9 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -6+b5^post9 >= 0), cost: 2+4*n0 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied pruning (of leafs and parallel rules): Start location: l9 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 74: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM 75: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM 76: l3 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, (-29+a4^0 <= 0 /\ -b5^0+a4^0 <= 0), cost: 4 77: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 78: l3 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 79: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied acceleration Original rule: l3 -> l3 : b5^0'=-10+b5^0, a4^0'=2+a4^0, (-29+a4^0 <= 0 /\ -b5^0+a4^0 <= 0), cost: 4 New rule: l3 -> l3 : b5^0'=-10*n6+b5^0, a4^0'=2*n6+a4^0, (12-12*n6+b5^0-a4^0 >= 0 /\ n6 >= 0 /\ 31-2*n6-a4^0 >= 0), cost: 4*n6 Sub-proof via acceration calculus written to file:///tmp/tmpnam_dKaaBH.txt Applied deletion Removed the following rules: 76 Accelerated simple loops Start location: l9 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 74: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM 75: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM 77: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 78: l3 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 79: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 82: l3 -> l3 : b5^0'=-10*n6+b5^0, a4^0'=2*n6+a4^0, (12-12*n6+b5^0-a4^0 >= 0 /\ n6 >= 0 /\ 31-2*n6-a4^0 >= 0), cost: 4*n6 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Applied chaining First rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Second rule: l3 -> l3 : b5^0'=-10-b5^0+2*a4^0, a4^0'=2-b5^0+2*a4^0, (7+b5^0-2*a4^0 >= 0 /\ -b5^0+a4^0 >= 0), cost: 4-4*b5^0+4*a4^0 New rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=-9, a4^0'=3, answer^0'=0, (0 >= 0 /\ 6 >= 0), cost: 6 Applied chaining First rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 Second rule: l3 -> l3 : b5^0'=-10*n6+b5^0, a4^0'=2*n6+a4^0, (12-12*n6+b5^0-a4^0 >= 0 /\ n6 >= 0 /\ 31-2*n6-a4^0 >= 0), cost: 4*n6 New rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1-10*n6, a4^0'=1+2*n6, answer^0'=0, (n6 >= 0 /\ -1+n6 <= 0), cost: 2+4*n6 Applied deletion Removed the following rules: 79 82 Chained accelerated rules with incoming rules Start location: l9 51: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -7+b5^0 <= 0), cost: NONTERM 58: l3 -> [10] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0 /\ -9+b5^0 <= 0), cost: NONTERM 60: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ -5+b5^0 <= 0), cost: NONTERM 62: l3 -> [10] : (-29+a4^0 <= 0 /\ -2-b5^0+a4^0 >= 0 /\ -4+b5^0 >= 0 /\ 5-b5^0 >= 0), cost: NONTERM 65: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 74: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ 12-b5^0 <= 0), cost: NONTERM 75: l3 -> [11] : (-29+a4^0 <= 0 /\ -1-b5^0+a4^0 >= 0 /\ -6+b5^0 >= 0), cost: NONTERM 77: l3 -> [10] : (-29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -a4^0+b5^post9 <= 0 /\ -6+b5^0 >= 0 /\ -13+b5^post9 >= 0), cost: NONTERM 78: l3 -> [10] : (-12+b5^post9 <= 0 /\ -10+b5^post9 >= 0 /\ -29+a4^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -6+b5^0 >= 0), cost: NONTERM 27: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1, a4^0'=1, answer^0'=0, TRUE, cost: 2 83: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=-9, a4^0'=3, answer^0'=0, (0 >= 0 /\ 6 >= 0), cost: 6 84: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1-10*n6, a4^0'=1+2*n6, answer^0'=0, (n6 >= 0 /\ -1+n6 <= 0), cost: 2+4*n6 Eliminating location l3 by chaining: Applied partial deletion Original rule: l9 -> l3 : b^0'=1, a^0'=1, b5^0'=1-10*n6, a4^0'=1+2*n6, answer^0'=0, (n6 >= 0 /\ -1+n6 <= 0), cost: 2+4*n6 New rule: l9 -> [14] : (n6 >= 0 /\ -1+n6 <= 0), cost: 2+4*n6 Applied deletion Removed the following rules: 27 51 58 60 62 65 74 75 77 78 83 84 Eliminated locations on tree-shaped paths Start location: l9 85: l9 -> [14] : (n6 >= 0 /\ -1+n6 <= 0), cost: 2+4*n6 Computing asymptotic complexity Proved the following lower bound Complexity: Unknown Cpx degree: ? Solved cost: 0 Rule cost: 0