int_rules_9_3 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 9.3*Piecewise*linear*functions =#
    @apply_utils Antiderivative((~u) ^ ~(m'), ~x) => With([c = Simplify(D(~u, ~x))], (1 / c) * Subst(Antiderivative((~x) ^ ~m, ~x), ~x, ~u)) <-- FreeQ(~m, ~x) && PiecewiseLinearQ(~u, ~x)
    @apply_utils Antiderivative(~v / ~u, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (b * ~x) / a - ((b * ~u - a * ~v) / a) * Antiderivative(1 / ~u, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative((~v) ^ ~n / ~u, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (~v) ^ ~n / (a * ~n) - ((b * ~u - a * ~v) / a) * Antiderivative((~v) ^ (~n - 1) / ~u, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (GtQ(~n, 0) && NeQ(~n, 1))
    @apply_utils Antiderivative(1 / (~u * ~v), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (b / (b * ~u - a * ~v)) * Antiderivative(1 / ~v, ~x) - (a / (b * ~u - a * ~v)) * Antiderivative(1 / ~u, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative(1 / (~u * sqrt(~v)), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (2 * atan(sqrt(~v) / Rt((b * ~u - a * ~v) / a, 2))) / (a * Rt((b * ~u - a * ~v) / a, 2)) <-- NeQ(b * ~u - a * ~v, 0) && PosQ((b * ~u - a * ~v) / a)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative(1 / (~u * sqrt(~v)), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (-2 * atanh(sqrt(~v) / Rt(-((b * ~u - a * ~v)) / a, 2))) / (a * Rt(-((b * ~u - a * ~v)) / a, 2)) <-- NeQ(b * ~u - a * ~v, 0) && NegQ((b * ~u - a * ~v) / a)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative((~v) ^ ~n / ~u, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (~v) ^ (~n + 1) / ((~n + 1) * (b * ~u - a * ~v)) - ((a * (~n + 1)) / ((~n + 1) * (b * ~u - a * ~v))) * Antiderivative((~v) ^ (~n + 1) / ~u, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && LtQ(~n, -1)
    @apply_utils Antiderivative((~v) ^ ~n / ~u, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], ((~v) ^ (~n + 1) / ((~n + 1) * (b * ~u - a * ~v))) * HypergeometricFunctions._₂F₁(1, ~n + 1, ~n + 2, (-a * ~v) / (b * ~u - a * ~v)) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && Not(IntegerQ(~n))
    @apply_utils Antiderivative(1 / (sqrt(~u) * sqrt(~v)), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (2 / Rt(a * b, 2)) * atanh((Rt(a * b, 2) * sqrt(~u)) / (a * sqrt(~v))) <-- NeQ(b * ~u - a * ~v, 0) && PosQ(a * b)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative(1 / (sqrt(~u) * sqrt(~v)), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (2 / Rt(-a * b, 2)) * atan((Rt(-a * b, 2) * sqrt(~u)) / (a * sqrt(~v))) <-- NeQ(b * ~u - a * ~v, 0) && NegQ(a * b)) <-- PiecewiseLinearQ(~u, ~v, ~x)
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~n, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (-((~u) ^ (~m + 1)) * (~v) ^ (~n + 1)) / ((~m + 1) * (b * ~u - a * ~v)) <-- NeQ(b * ~u - a * ~v, 0)) <-- FreeQ([~m, ~n], ~x) && (PiecewiseLinearQ(~u, ~v, ~x) && (EqQ(~m + ~n + 2, 0) && NeQ(~m, -1)))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~(n'), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], ((~u) ^ (~m + 1) * (~v) ^ ~n) / (a * (~m + 1)) - ((b * ~n) / (a * (~m + 1))) * Antiderivative((~u) ^ (~m + 1) * (~v) ^ (~n - 1), ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- FreeQ([~m, ~n], ~x) && (PiecewiseLinearQ(~u, ~v, ~x) && (NeQ(~m, -1) && (LtQ(~m, -1) && (GtQ(~n, 0) && Not(ILtQ(~m + ~n, -2) && (FractionQ(~m) || GeQ(2 * ~n + ~m + 1, 0)))) || (IGtQ(~n, 0) && (IGtQ(~m, 0) && LeQ(~n, ~m)) || (IGtQ(~n, 0) && Not(IntegerQ(~m)) || ILtQ(~m, 0) && Not(IntegerQ(~n)))))))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~(n'), ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], ((~u) ^ (~m + 1) * (~v) ^ ~n) / (a * (~m + ~n + 1)) - ((~n * (b * ~u - a * ~v)) / (a * (~m + ~n + 1))) * Antiderivative((~u) ^ ~m * (~v) ^ (~n - 1), ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (NeQ(~m + ~n + 2, 0) && (GtQ(~n, 0) && (NeQ(~m + ~n + 1, 0) && (Not(IGtQ(~m, 0) && (Not(IntegerQ(~n)) || LtQ(0, ~m, ~n))) && Not(ILtQ(~m + ~n, -2))))))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~n, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], ((~u) ^ (~m + 1) * (~v) ^ ~n) / (a * (~m + ~n + 1)) - ((~n * (b * ~u - a * ~v)) / (a * (~m + ~n + 1))) * Antiderivative((~u) ^ ~m * (~v) ^ Simplify(~n - 1), ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (NeQ(~m + ~n + 1, 0) && (Not(RationalQ(~n)) && SumSimplerQ(~n, -1)))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~n, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (-((~u) ^ (~m + 1)) * (~v) ^ (~n + 1)) / ((~m + 1) * (b * ~u - a * ~v)) + ((b * (~m + ~n + 2)) / ((~m + 1) * (b * ~u - a * ~v))) * Antiderivative((~u) ^ (~m + 1) * (~v) ^ ~n, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (NeQ(~m + ~n + 2, 0) && LtQ(~m, -1))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~n, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (-((~u) ^ (~m + 1)) * (~v) ^ (~n + 1)) / ((~m + 1) * (b * ~u - a * ~v)) + ((b * (~m + ~n + 2)) / ((~m + 1) * (b * ~u - a * ~v))) * Antiderivative((~u) ^ Simplify(~m + 1) * (~v) ^ ~n, ~x) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (Not(RationalQ(~m)) && SumSimplerQ(~m, 1))
    @apply_utils Antiderivative((~u) ^ ~m * (~v) ^ ~n, ~x) => With([a = Simplify(D(~u, ~x)), b = Simplify(D(~v, ~x))], (((~u) ^ ~m * (~v) ^ (~n + 1)) / (b * (~n + 1) * ((b * ~u) / (b * ~u - a * ~v)) ^ ~m)) * HypergeometricFunctions._₂F₁(-(~m), ~n + 1, ~n + 2, (-a * ~v) / (b * ~u - a * ~v)) <-- NeQ(b * ~u - a * ~v, 0)) <-- PiecewiseLinearQ(~u, ~v, ~x) && (Not(IntegerQ(~m)) && Not(IntegerQ(~n)))
    @apply_utils Antiderivative((~u) ^ ~(n') * log(~(a') + ~(b') * ~x), ~x) => With([c = Simplify(D(~u, ~x))], (((~u) ^ ~n * (~a + ~b * ~x) * log(~a + ~b * ~x)) / ~b - Antiderivative((~u) ^ ~n, ~x)) - ((c * ~n) / ~b) * Antiderivative((~u) ^ (~n - 1) * (~a + ~b * ~x) * log(~a + ~b * ~x), ~x)) <-- FreeQ([~a, ~b], ~x) && (PiecewiseLinearQ(~u, ~x) && (Not(LinearQ(~u, ~x)) && GtQ(~n, 0)))
    #= Antiderivative((~u)^(~n')*log((~a')+(~b')*(~x))/((~a')+(~b')*(~x)),~x) :=  With([c=Simplify(D(u,x))], u^n*log(a+b*x)^2/(2*b) - c*n/(2*b)*Antiderivative(u^(n-1)*log(a+b*x)^2,x)) <-- FreeQ([a,b],x) &&  PiecewiseLinearQ(u,x) && GtQ(n,0) =#
    @apply_utils Antiderivative((~u) ^ ~(n') * (~(a') + ~(b') * ~x) ^ ~(m') * log(~(a') + ~(b') * ~x), ~x) => With([c = Simplify(D(~u, ~x))], (((~u) ^ ~n * (~a + ~b * ~x) ^ (~m + 1) * log(~a + ~b * ~x)) / (~b * (~m + 1)) - (1 / (~m + 1)) * Antiderivative((~u) ^ ~n * (~a + ~b * ~x) ^ ~m, ~x)) - ((c * ~n) / (~b * (~m + 1))) * Antiderivative((~u) ^ (~n - 1) * (~a + ~b * ~x) ^ (~m + 1) * log(~a + ~b * ~x), ~x)) <-- FreeQ([~a, ~b, ~m], ~x) && (PiecewiseLinearQ(~u, ~x) && (Not(LinearQ(~u, ~x)) && (GtQ(~n, 0) && NeQ(~m, -1))))
end
