A proof segment used in Program Correctness precondition ⟹ termination Proved by defining a Terminating Variable