using Microsoft.Z3;

class Program
{
    static void Main()
    {
        var ctx = new Context();
        var solver = ctx.MkSolver();

        var C0 = (ArithExpr)ctx.MkDiv(ctx.MkInt("63674491458"), ctx.MkInt("10000"));
        var D2 = (ArithExpr)ctx.MkDiv(ctx.MkInt("251882658"),   ctx.MkInt("100000000000"));
        var D4 = (ArithExpr)ctx.MkDiv(ctx.MkInt("370096"),      ctx.MkInt("100000000000"));
        var D6 = (ArithExpr)ctx.MkDiv(ctx.MkInt("745"),         ctx.MkInt("100000000000"));

        var sin = ctx.MkFuncDecl("sin", ctx.RealSort, ctx.RealSort);

        var u = ctx.MkRealConst("u");
        var v = ctx.MkRealConst("v");
        var zero = ctx.MkReal(0);
        var sinMax = (ArithExpr)ctx.MkDiv(ctx.MkInt("6"), ctx.MkInt("10000"));

        var sinMonotone = ctx.MkForall(
            new Expr[] { u, v },
            ctx.MkImplies(
                ctx.MkAnd(
                    ctx.MkGe(u, zero), ctx.MkLe(u, sinMax),
                    ctx.MkGe(v, zero), ctx.MkLe(v, sinMax),
                    ctx.MkLt(u, v)
                ),
                ctx.MkLt(
                    (ArithExpr)ctx.MkApp(sin, u),
                    (ArithExpr)ctx.MkApp(sin, v)
                )
            )
        );
        solver.Add(sinMonotone);

        solver.Add(ctx.MkEq(ctx.MkApp(sin, zero), zero));

        var X1 = (ArithExpr)ctx.MkRealConst("X1");
        var X2 = (ArithExpr)ctx.MkRealConst("X2");
        var Xmin = ctx.MkReal(0);
        var betaMax = (ArithExpr)ctx.MkDiv(ctx.MkInt("1"), ctx.MkInt("10000"));
        var Xmax = (ArithExpr)ctx.MkMul(C0, betaMax);

        solver.Add(ctx.MkGe(X1, Xmin), ctx.MkLe(X1, Xmax));
        solver.Add(ctx.MkGe(X2, Xmin), ctx.MkLe(X2, Xmax));
        solver.Add(ctx.MkLt(X1, X2));

        Func<ArithExpr, ArithExpr> Latitude = X =>
        {
            var beta = ctx.MkDiv(X, C0);
            var b2 = ctx.MkMul(ctx.MkReal(2), beta);
            var b4 = ctx.MkMul(ctx.MkReal(4), beta);
            var b6 = ctx.MkMul(ctx.MkReal(6), beta);

            return ctx.MkAdd(
                beta,
                ctx.MkMul(D2, (ArithExpr)ctx.MkApp(sin, b2)),
                ctx.MkMul(D4, (ArithExpr)ctx.MkApp(sin, b4)),
                ctx.MkMul(D6, (ArithExpr)ctx.MkApp(sin, b6))
            );
        };

        var B1 = Latitude(X1);
        var B2 = Latitude(X2);

        solver.Add(ctx.MkGe(B1, B2));

        var result = solver.Check();
        Console.WriteLine(result);

        if (result == Status.UNSATISFIABLE)
        {
            Console.WriteLine("Monotonicity proved: no counter-example exists.");
        }
        else if (result == Status.SATISFIABLE)
        {
            var m = solver.Model;
            Console.WriteLine("Counter-example found:");
            Console.WriteLine("  X1 = " + m.Evaluate(X1));
            Console.WriteLine("  X2 = " + m.Evaluate(X2));
            Console.WriteLine("  B1 = " + m.Evaluate(B1));
            Console.WriteLine("  B2 = " + m.Evaluate(B2));
        }
        else
        {
            Console.WriteLine("Z3 returned UNKNOWN.");
        }
    }
}

using Microsoft.Z3;

class Program
{
    static void Main()
    {
        var ctx = new Context();
        var solver = ctx.MkSolver();

        // all D2, D4, D6 : Real
        var D2 = (ArithExpr)ctx.MkDiv(ctx.MkInt("251882658"), ctx.MkInt("100000000000"));
        var D4 = (ArithExpr)ctx.MkDiv(ctx.MkInt("370096"),    ctx.MkInt("100000000000"));
        var D6 = (ArithExpr)ctx.MkDiv(ctx.MkInt("745"),       ctx.MkInt("100000000000"));

        // all c2, c4, c6 : Real :- c2 >= -1.0 /\ c2 <= 1.0
        //                      /\ c4 >= -1.0 /\ c4 <= 1.0
        //                      /\ c6 >= -1.0 /\ c6 <= 1.0
        var c2 = (ArithExpr)ctx.MkRealConst("c2");
        var c4 = (ArithExpr)ctx.MkRealConst("c4");
        var c6 = (ArithExpr)ctx.MkRealConst("c6");
        var m1 = (ArithExpr)ctx.MkUnaryMinus(ctx.MkReal(1));
        var p1 = ctx.MkReal(1);
        var zero = ctx.MkReal(0);

        solver.Add(ctx.MkGe(c2, m1), ctx.MkLe(c2, p1));
        solver.Add(ctx.MkGe(c4, m1), ctx.MkLe(c4, p1));
        solver.Add(ctx.MkGe(c6, m1), ctx.MkLe(c6, p1));

        // deriv = 1.0 + 2*D2*c2 + 4*D4*c4 + 6*D6*c6
        var term2 = ctx.MkMul(ctx.MkReal(2), ctx.MkMul(D2, c2));
        var term4 = ctx.MkMul(ctx.MkReal(4), ctx.MkMul(D4, c4));
        var term6 = ctx.MkMul(ctx.MkReal(6), ctx.MkMul(D6, c6));

        var deriv = ctx.MkAdd(p1, ctx.MkAdd(term2, ctx.MkAdd(term4, term6)));

        // exists c2, c4, c6 :- deriv <= 0.0
        solver.Add(ctx.MkLe(deriv, zero));

        var result = solver.Check();
        Console.WriteLine(result);

        if (result == Status.UNSATISFIABLE)
        {
            Console.WriteLine("Derivative > 0 proved for all cos in [-1, 1].");
            Console.WriteLine("Monotonicity proved on full meridian.");
        }
        else if (result == Status.SATISFIABLE)
        {
            var m = solver.Model;
            Console.WriteLine("Counter-example found:");
            Console.WriteLine("  c2 = " + m.Evaluate(c2));
            Console.WriteLine("  c4 = " + m.Evaluate(c4));
            Console.WriteLine("  c6 = " + m.Evaluate(c6));
            Console.WriteLine("  deriv = " + m.Evaluate(deriv));
        }
        else
        {
            Console.WriteLine("Z3 returned UNKNOWN.");
        }
    }
}