int_rules_5_1_2 = @theory begin

    #= ::Subsection::Closed:: =#
    #= 5.1.2*(d*x)^m*(a+b*arcsin(c*x))^n =#
    #= Antiderivative(((~a')+(~b')*asin((~c')*(~x)))^(~n')/(~x),~x) :=  1/b*Subst(Antiderivative(x^n*cot(-a/b+x/b),x),x,a+b*asin(c*x)) <--  FreeQ([a,b,c],x) && IGtQ(n,0) =#
    #= Antiderivative(((~a')+(~b')*acos((~c')*(~x)))^(~n')/(~x),~x) :=  -1/b*Subst(Antiderivative(x^n*tan(-a/b+x/b),x),x,a+b*acos(c*x)) <--  FreeQ([a,b,c],x) && IGtQ(n,0) =#
    @apply_utils Antiderivative((~(a') + ~(b') * asin(~(c') * ~x)) ^ ~(n') / ~x, ~x) => Subst(Antiderivative((~a + ~b * ~x) ^ ~n * cot(~x), ~x), ~x, asin(~c * ~x)) <-- FreeQ([~a, ~b, ~c], ~x) && IGtQ(~n, 0)
    @apply_utils Antiderivative((~(a') + ~(b') * acos(~(c') * ~x)) ^ ~(n') / ~x, ~x) => -(Subst(Antiderivative((~a + ~b * ~x) ^ ~n * tan(~x), ~x), ~x, acos(~c * ~x))) <-- FreeQ([~a, ~b, ~c], ~x) && IGtQ(~n, 0)
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~(n'), ~x) => ((~d * ~x) ^ (~m + 1) * (~a + ~b * asin(~c * ~x)) ^ ~n) / (~d * (~m + 1)) - ((~b * ~c * ~n) / (~d * (~m + 1))) * Antiderivative(((~d * ~x) ^ (~m + 1) * (~a + ~b * asin(~c * ~x)) ^ (~n - 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m], ~x) && (IGtQ(~n, 0) && NeQ(~m, -1))
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~(n'), ~x) => ((~d * ~x) ^ (~m + 1) * (~a + ~b * acos(~c * ~x)) ^ ~n) / (~d * (~m + 1)) + ((~b * ~c * ~n) / (~d * (~m + 1))) * Antiderivative(((~d * ~x) ^ (~m + 1) * (~a + ~b * acos(~c * ~x)) ^ (~n - 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m], ~x) && (IGtQ(~n, 0) && NeQ(~m, -1))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~n, ~x) => ((~x) ^ (~m + 1) * (~a + ~b * asin(~c * ~x)) ^ ~n) / (~m + 1) - ((~b * ~c * ~n) / (~m + 1)) * Antiderivative(((~x) ^ (~m + 1) * (~a + ~b * asin(~c * ~x)) ^ (~n - 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && GtQ(~n, 0))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~n, ~x) => ((~x) ^ (~m + 1) * (~a + ~b * acos(~c * ~x)) ^ ~n) / (~m + 1) + ((~b * ~c * ~n) / (~m + 1)) * Antiderivative(((~x) ^ (~m + 1) * (~a + ~b * acos(~c * ~x)) ^ (~n - 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && GtQ(~n, 0))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~n, ~x) => ((~x) ^ ~m * sqrt(1 - (~c) ^ 2 * (~x) ^ 2) * (~a + ~b * asin(~c * ~x)) ^ (~n + 1)) / (~b * ~c * (~n + 1)) - (1 / ((~b) ^ 2 * (~c) ^ (~m + 1) * (~n + 1))) * Subst(Antiderivative(ExpandTrigReduce((~x) ^ (~n + 1), sin(-(~a) / ~b + ~x / ~b) ^ (~m - 1) * (~m - (~m + 1) * sin(-(~a) / ~b + ~x / ~b) ^ 2), ~x), ~x), ~x, ~a + ~b * asin(~c * ~x)) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && (GeQ(~n, -2) && LtQ(~n, -1)))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~n, ~x) => (-((~x) ^ ~m) * sqrt(1 - (~c) ^ 2 * (~x) ^ 2) * (~a + ~b * acos(~c * ~x)) ^ (~n + 1)) / (~b * ~c * (~n + 1)) - (1 / ((~b) ^ 2 * (~c) ^ (~m + 1) * (~n + 1))) * Subst(Antiderivative(ExpandTrigReduce((~x) ^ (~n + 1), cos(-(~a) / ~b + ~x / ~b) ^ (~m - 1) * (~m - (~m + 1) * cos(-(~a) / ~b + ~x / ~b) ^ 2), ~x), ~x), ~x, ~a + ~b * acos(~c * ~x)) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && (GeQ(~n, -2) && LtQ(~n, -1)))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~n, ~x) => (((~x) ^ ~m * sqrt(1 - (~c) ^ 2 * (~x) ^ 2) * (~a + ~b * asin(~c * ~x)) ^ (~n + 1)) / (~b * ~c * (~n + 1)) - (~m / (~b * ~c * (~n + 1))) * Antiderivative(((~x) ^ (~m - 1) * (~a + ~b * asin(~c * ~x)) ^ (~n + 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x)) + ((~c * (~m + 1)) / (~b * (~n + 1))) * Antiderivative(((~x) ^ (~m + 1) * (~a + ~b * asin(~c * ~x)) ^ (~n + 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && LtQ(~n, -2))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~n, ~x) => ((-((~x) ^ ~m) * sqrt(1 - (~c) ^ 2 * (~x) ^ 2) * (~a + ~b * acos(~c * ~x)) ^ (~n + 1)) / (~b * ~c * (~n + 1)) + (~m / (~b * ~c * (~n + 1))) * Antiderivative(((~x) ^ (~m - 1) * (~a + ~b * acos(~c * ~x)) ^ (~n + 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x)) - ((~c * (~m + 1)) / (~b * (~n + 1))) * Antiderivative(((~x) ^ (~m + 1) * (~a + ~b * acos(~c * ~x)) ^ (~n + 1)) / sqrt(1 - (~c) ^ 2 * (~x) ^ 2), ~x) <-- FreeQ([~a, ~b, ~c], ~x) && (IGtQ(~m, 0) && LtQ(~n, -2))
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~n, ~x) => (1 / (~b * (~c) ^ (~m + 1))) * Subst(Antiderivative((~x) ^ ~n * sin(-(~a) / ~b + ~x / ~b) ^ ~m * cos(-(~a) / ~b + ~x / ~b), ~x), ~x, ~a + ~b * asin(~c * ~x)) <-- FreeQ([~a, ~b, ~c, ~n], ~x) && IGtQ(~m, 0)
    @apply_utils Antiderivative((~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~n, ~x) => (-1 / (~b * (~c) ^ (~m + 1))) * Subst(Antiderivative((~x) ^ ~n * cos(-(~a) / ~b + ~x / ~b) ^ ~m * sin(-(~a) / ~b + ~x / ~b), ~x), ~x, ~a + ~b * acos(~c * ~x)) <-- FreeQ([~a, ~b, ~c, ~n], ~x) && IGtQ(~m, 0)
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * (~(a') + ~(b') * asin(~(c') * ~x)) ^ ~(n'), ~x) => Unintegrable((~d * ~x) ^ ~m * (~a + ~b * asin(~c * ~x)) ^ ~n, ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x)
    @apply_utils Antiderivative((~(d') * ~x) ^ ~(m') * (~(a') + ~(b') * acos(~(c') * ~x)) ^ ~(n'), ~x) => Unintegrable((~d * ~x) ^ ~m * (~a + ~b * acos(~c * ~x)) ^ ~n, ~x) <-- FreeQ([~a, ~b, ~c, ~d, ~m, ~n], ~x)
end
