i-4[0] = max(-inf, 0) negi-4[0] = max(-inf, 0) negi-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, negi-4[0]), guard(add(min(negi-2[0], inf), min(i-2[0], inf)), 0, negi-2[0])) i-1-pre = max(-inf, guard(add(min(negi-4[0], inf), min(i-4[0], inf)), 0, i-4[0]), guard(add(min(negi-2[0], inf), min(i-2[0], inf)), 0, i-2[0])) negi-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, negi-1-pre)) i-3-pre = max(-inf, guard(add(min(negi-1-pre, inf), min(i-1-pre, 2)), 0, min(2, i-1-pre))) negi-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, min(-3, negi-1-pre))) i-0-pre = max(-inf, guard(add(min(negi-1-pre, -3), min(i-1-pre, inf)), 0, i-1-pre)) i-3[0] = max(-inf, add(1, i-3-pre)) negi-3[0] = max(-inf, add(-1, negi-3-pre)) negi-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, negi-3[0])) i-2-pre = max(-inf, guard(add(min(negi-3[0], inf), min(i-3[0], inf)), 0, i-3[0])) i-2[0] = max(-inf, add(1, i-2-pre)) negi-2[0] = max(-inf, add(-1, negi-2-pre))