Termination

A proof segment used in Program Correctness $\text{precondition }⟹\text{ termination}$