A rigorous decomposition approach is presented for mixed-integer dynamic optimization problems. The approach combines dynamic optimization with insight based targeting techniques to decompose the optimization into subproblems providing rigorous upper and lower bounds on the objective. This approach has the potential to eliminate total enumeration of the discrete space, assures termination in a finite number of iterations, and yields a rigorous bound on the distance between the solution found and the global solution.