Verifying a Superior Integration Method for Step Functions I should note that this is an integration algorithm and therefore intermediate steps DO appear to be unjustified. The purpose of this question is to justify or reject this algorithm as always giving correct solutions.
Suppose we have some piecewise continuous function $f$ and that it can be written in the form $f(x) = G(x,\lfloor g_1(x) \rfloor,\lfloor g_2(x) \rfloor,\cdots, \lfloor g_n(x) \rfloor)$, for some functions $g_1(x), g_2(x), \cdots g_n(x)$ and $G(x,y_1,y_2,\cdots, y_n)$ such that $\lfloor g_1(x) \rfloor,\lfloor g_2(x) \rfloor,\cdots, \lfloor g_n(x) \rfloor$ are piecewise constant functions and $G$ is piecewise continuous with respect to $x$.
Now we have the algorithm to compute the general integral for $f$:
INTEGRATE-WITH-FLOOR(f)


*

*Let $H(x,y_1,y_2,\cdots, y_n) = \int G(x,y_1,y_2,\cdots, y_n) dx$ be a new function.

*Let $F(x) = H(x,\lfloor g_1(x) \rfloor,\lfloor g_2(x) \rfloor,\cdots, \lfloor g_n(x) \rfloor)$ be a new function.

*Let $C(x)$ be a new piecewise constant function such that $F(x) + C(x)$ is continuous.

*Return $F(x) + C(x)$.
Now I know this is more like an algorithm from a Computer Science class than a Math forum but I think it works and I seek verification.
Furthermore:
Does this algorithm compare to any existing methods. I was taught this method back when I was in calculus a few years ago but I have never seen it since then nor understood if it was justified or not.
Is there any way to extend this to differential equations at all or would it be too difficult?
Note: not looking for algorithms. Just general discussion of how it would be extended is just fine as well.
 A: This algorithm is not completely true or it at leaat appears so. I can only verify it for a piecewise continuous $f$ and where $\lfloor g(x) \rfloor$ in the algorithm is piecewise constant.

THE PROOF
We will prove the correctness of this algorithm by a sequence of definitions and propositions.
First we define $f^+(x) = \lim_{h \to 0^{+}} \frac {f(x+h) - \lim_{a \to x^{+}} f(a)}{h}$ and $f^-(x) = \lim_{h \to 0^{-}} \frac {f(x+h) - \lim_{a \to x^{-}} f(a)}{h}$ as shorthand for the left and right hand derivatives of some function $f$ at $x$.
Now we will define a special operator that will serve as a means of formalizing the questions algorithm.

Definition: We define the implied derivative to be an operator that takes in a function $f$ and returns a set of functions as shown by the expression $f^{\to} = \{g | \forall_{x \in R} (g(x) = f^+(x)) \lor (g(x) = f^-(x))\}$.

We will define a piecewise constant function via the following:

A piecewise constant function $g$ is any function that has a left and right hand derivative of $0$ everywhere.

We now prove the following propositions.

The implied derivative of any result of steps 1-4 is the original function $f$.

We now define an implied antiderivative of some function $f$ to be any function $F$ such that $f$ is an implied derivative of $F$.

Any two implied antiderivatives of some function $f$ known as $F$ and $F'$ differ by some unique piecewise constant function $C$.

Now we must go one step further and prove the following.

If $F$ is an implied antiderivative of $f$, then for all piecewise constant functions $C$ we have that $F + C$ is an implied antiderivative of $f$.

Because all results of the first 4 steps of the algorithm are an implied antiderivative of the imput we can state that adding a piecewise constant function to it results in another implied antiderivative. Therefore, all results of the algorithm are continuous implied antiderivatives of the input. Now we shall relate implied antiderivatives to integrals.

Suppose we have two continuous implied antiderivatives of $f$ caled $F$ and $F'$. Then there exists a unique constant $c$, such that $F = F' + c$.

Now we go one step further.

Suppose we have a continuous implied antiderivative of $f$ caled $F$. Then for all constants $c$, $F + c$ is a continuous implied antiderivative of $f$.

Now that we have done that we only have one theorem left to prove.

If $F(x) = \int_0^x f(x)$ then $F$ is a continuous implied antiderivative of $f$.

Since all integrals are continuous implied antiderivatives of the input to the algorithm we only need to show that all continuous implied antiderivatives are integrals of the input. Because all such implied antiderivatives differ by a constant, we have that they differ by some integral by a constant. Since anything that differs from an integral by a constant is also an integral we have that all continuous implied antiderivatives are integrals.
Therefore, any result of the algorithm is a valid integral of the input.

I will fill in more of the sub proofs later on. It is late and I am tired. I have to say, this whole thing quite literally took me two years to prove and finally I have pretty much done it. Hopefully nobody takes offense to me needing a minor break before proving all these subtheorems.
Citation: https://drive.google.com/file/d/1UdBHop02_AmIhLbMPmqwbnxWzDcc3eWF/view
