Finite alphabet iterative decoders (FAIDs) proposed for LDPC codes on the binary symmetric channel are capable of surpassing the belief propagation (BP) decoder in the error floor region with lower complexity and precision, but these decoders are difficult to analyze for finite-length codes. Recently, decimation-enhanced FAIDs (DFAIDs) were proposed for column-weight-three codes. Decimation involves fixing the bit values of certain variable nodes during message-passing based on the messages they receive after some number of iterations. In this paper, we address the problem of proving the guaranteed error-correction capability of DFAIDs for column-weight-three LDPC codes. We present the methodology of the proof to derive sufficient conditions on the Tanner graph that guarantee the correction of a given error pattern in a finite number of iterations. These sufficient conditions are described as a list of forbidden graphs that must not be contained in the Tanner graph of the code. As a test case, we consider the problem of guaranteeing the correction of four errors. We illustrate the analysis for a specific 4-error pattern and provide the sufficient conditions for its correction. We also present results on the design of codes satisfying those sufficient conditions and their impact on the achievable code rate.