Abstract:With the popularization and application of formal methods, there are increasingly more cases in which the theorem prover HOL4 cannot automatically complete the termination proof in the process of formal modeling. Manual termination proof still lacks a general idea. In response, a standardized manual termination proof method is proposed. Starting from the nature of the problem, the method guarantees that the target has the necessary conditions for solving the termination problem. Then, the proof target is simplified by equivalent substitution. Finally, on the basis of the original theorem library, the lacking lemma in the proof process is found to advance the proof. The example shows that this method has a clear logic and can solve the manual termination proof problem of the HOL4 in most cases.